MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.exists_maximalAbelian_containing_isSelfAdjoint

Raw UTF-8 source

theorem exists_maximalAbelian_containing_isSelfAdjoint
    (x : A) (hx : IsSelfAdjoint x) :
    ∃ D : StarSubalgebra ℂ A, IsMaximalAbelian D ∧ x ∈ D

1 import MathlibAnnex.Analysis.CStarAlgebra.MaximalAbelian
2 
3 /-!
4 # Maximal abelian subalgebras containing a prescribed normal element
5 -/
6 
7 set_option autoImplicit false
8 
9 open Set
10 
11 namespace MathlibAnnex.Analysis.CStarAlgebra
12 
13 universe u
14 
15 variable {A : Type u} [CStarAlgebra A]
16 
17 /-- Every star-normal element of a unital C-star algebra belongs to a maximal
18 abelian star subalgebra. -/
19 theorem exists_maximalAbelian_containing (x : A) [IsStarNormal x] :
20     ∃ D : StarSubalgebra ℂ A, IsMaximalAbelian D ∧ x ∈ D := by
21   let E : StarSubalgebra ℂ A := StarAlgebra.elemental ℂ x
22   let S : Set (StarSubalgebra ℂ A) :=
23     {D | IsMulCommutative D ∧ E ≤ D}
24   have hE : E ∈ S := by
25     refine ⟨inferInstance, le_rfl⟩
26   obtain ⟨D, _hED, hD, hmax⟩ :=
27     zorn_le_nonempty₀ S (fun c hcS hc y hy => by
28       letI : Nonempty c := ⟨⟨y, hy⟩⟩
29       let F : c → StarSubalgebra ℂ A := fun d => d.1
30       have hdir : Directed (· ≤ ·) F := by
31         intro i j
32         by_cases hij' : i = j
33         · subst j
34           exact ⟨i, le_rfl, le_rfl⟩
35         have hcoe : (i.1 : StarSubalgebra ℂ A) ≠ j.1 :=
36           fun h => hij' (Subtype.ext h)
37         rcases hc i.2 j.2 hcoe with hij | hji
38         · exact ⟨j, hij, le_rfl⟩
39         · exact ⟨i, le_rfl, hji⟩
40       letI (d : c) : IsMulCommutative (F d) := (hcS d.2).1
41       refine ⟨⨆ d : c, F d, ?_, ?_⟩
42       · refine ⟨StarSubalgebra.isMulCommutative_iSup hdir, ?_⟩
43         exact (hcS hy).2.trans (le_iSup F ⟨y, hy⟩)
44       · intro z hz
45         exact le_iSup F ⟨z, hz⟩)
46       E hE
47   refine ⟨D, ?_, ?_⟩
48   · refine ⟨hD.1, ?_⟩
49     intro F hF hDF
50     exact hmax ⟨hF, hD.2.trans hDF⟩ hDF
51   · exact hD.2 (StarAlgebra.elemental.self_mem ℂ x)
52 
53 /-- Self-adjoint elements satisfy the normality hypothesis of
54 `exists_maximalAbelian_containing`. -/
55 theorem exists_maximalAbelian_containing_isSelfAdjoint
56     (x : A) (hx : IsSelfAdjoint x) :
57     ∃ D : StarSubalgebra ℂ A, IsMaximalAbelian D ∧ x ∈ D := by
58   letI : IsStarNormal x := hx.isStarNormal
59   exact exists_maximalAbelian_containing x
60 
61 end MathlibAnnex.Analysis.CStarAlgebra