Exact source: MathlibAnnex/Analysis/CStarAlgebra/MaximalAbelianContaining.lean
Pinned GitHub source · Raw UTF-8 source
Back to A nonzero projection with scalar corner · Back to Every operator in a singleton image is compact · Back to A maximal abelian subalgebra containing a self-adjoint element
1import MathlibAnnex.Analysis.CStarAlgebra.MaximalAbelian23/-!4# Maximal abelian subalgebras containing a prescribed normal element5-/67set_option autoImplicit false89open Set1011namespace MathlibAnnex.Analysis.CStarAlgebra1213universe u1415variable {A : Type u} [CStarAlgebra A]1617/-- Every star-normal element of a unital C-star algebra belongs to a maximal18abelian star subalgebra. -/19theorem exists_maximalAbelian_containing (x : A) [IsStarNormal x] :20 ∃ D : StarSubalgebra ℂ A, IsMaximalAbelian D ∧ x ∈ D := by21 let E : StarSubalgebra ℂ A := StarAlgebra.elemental ℂ x22 let S : Set (StarSubalgebra ℂ A) :=23 {D | IsMulCommutative D ∧ E ≤ D}24 have hE : E ∈ S := by25 refine ⟨inferInstance, le_rfl⟩26 obtain ⟨D, _hED, hD, hmax⟩ :=27 zorn_le_nonempty₀ S (fun c hcS hc y hy => by28 letI : Nonempty c := ⟨⟨y, hy⟩⟩29 let F : c → StarSubalgebra ℂ A := fun d => d.130 have hdir : Directed (· ≤ ·) F := by31 intro i j32 by_cases hij' : i = j33 · subst j34 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 | hji38 · exact ⟨j, hij, le_rfl⟩39 · exact ⟨i, le_rfl, hji⟩40 letI (d : c) : IsMulCommutative (F d) := (hcS d.2).141 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 hz45 exact le_iSup F ⟨z, hz⟩)46 E hE47 refine ⟨D, ?_, ?_⟩48 · refine ⟨hD.1, ?_⟩49 intro F hF hDF50 exact hmax ⟨hF, hD.2.trans hDF⟩ hDF51 · exact hD.2 (StarAlgebra.elemental.self_mem ℂ x)5253/-- Self-adjoint elements satisfy the normality hypothesis of54`exists_maximalAbelian_containing`. -/55theorem exists_maximalAbelian_containing_isSelfAdjoint56 (x : A) (hx : IsSelfAdjoint x) :57 ∃ D : StarSubalgebra ℂ A, IsMaximalAbelian D ∧ x ∈ D := by58 letI : IsStarNormal x := hx.isStarNormal59 exact exists_maximalAbelian_containing x6061end MathlibAnnex.Analysis.CStarAlgebra