Exact source: MathlibAnnex/Analysis/CStarAlgebra/MaximalAbelian.lean
Pinned GitHub source · Raw UTF-8 source
Back to Maximal abelian $*$-subalgebras · Back to A maximal abelian subalgebra containing a self-adjoint element
1import Mathlib.Order.Zorn2import Mathlib.Algebra.Star.Subalgebra3import Mathlib.Topology.Algebra.StarSubalgebra4import Mathlib.Analysis.CStarAlgebra.Classes5import Mathlib.LinearAlgebra.Complex.Module67/-!8# Maximal abelian star subalgebras910This file constructs maximal commutative unital star subalgebras by Zorn's11lemma and records that they are norm closed in a C-star algebra.12-/1314set_option autoImplicit false1516open Set17open scoped ComplexStarModule1819namespace MathlibAnnex.Analysis.CStarAlgebra2021universe u2223variable {A : Type u} [CStarAlgebra A]2425/-- A maximal abelian unital star subalgebra, expressed without installing a26global commutative-ring instance on its subtype. -/27def IsMaximalAbelian (D : StarSubalgebra ℂ A) : Prop :=28 IsMulCommutative D ∧29 ∀ E : StarSubalgebra ℂ A, IsMulCommutative E → D ≤ E → E ≤ D3031/-- Every unital C-star algebra has a maximal abelian star subalgebra. -/32theorem exists_maximalAbelian :33 ∃ D : StarSubalgebra ℂ A, IsMaximalAbelian D := by34 let S : Set (StarSubalgebra ℂ A) := {D | IsMulCommutative D}35 have hbot : (⊥ : StarSubalgebra ℂ A) ∈ S := by36 change IsMulCommutative (⊥ : StarSubalgebra ℂ A)37 refine IsMulCommutative.of_comm fun x y => ?_38 apply Subtype.ext39 obtain ⟨r, hr⟩ := x.240 obtain ⟨s, hs⟩ := y.241 change (x : A) * (y : A) = (y : A) * (x : A)42 rw [← hr, ← hs]43 exact Algebra.commutes r (algebraMap ℂ A s)44 obtain ⟨D, _hbotD, hD, hmax⟩ :=45 zorn_le_nonempty₀ S (fun c hcS hc y hy => by46 letI : Nonempty c := ⟨⟨y, hy⟩⟩47 let F : c → StarSubalgebra ℂ A := fun d => d.148 have hdir : Directed (· ≤ ·) F := by49 intro i j50 by_cases hij' : i = j51 · subst j52 exact ⟨i, le_rfl, le_rfl⟩53 have hcoe : (i.1 : StarSubalgebra ℂ A) ≠ j.1 :=54 fun h => hij' (Subtype.ext h)55 rcases hc i.2 j.2 hcoe with hij | hji56 · exact ⟨j, hij, le_rfl⟩57 · exact ⟨i, le_rfl, hji⟩58 letI (d : c) : IsMulCommutative (F d) := hcS d.259 refine ⟨⨆ d : c, F d, ?_, ?_⟩60 · change IsMulCommutative (↥(⨆ d : c, F d))61 exact StarSubalgebra.isMulCommutative_iSup hdir62 · intro z hz63 exact le_iSup F ⟨z, hz⟩)64 (⊥ : StarSubalgebra ℂ A) hbot65 exact ⟨D, hD, fun E hE hDE => hmax hE hDE⟩6667/-- Maximal abelian star subalgebras of a C-star algebra are norm closed. -/68theorem IsMaximalAbelian.isClosed {D : StarSubalgebra ℂ A}69 (hD : IsMaximalAbelian D) : IsClosed (D : Set A) := by70 let E : StarSubalgebra ℂ A := D.topologicalClosure71 have hE : IsMulCommutative E := by72 letI : IsMulCommutative D := hD.173 letI : CommRing E :=74 StarSubalgebra.commRingTopologicalClosure D (fun x y => mul_comm' x y)75 infer_instance76 have hED : E ≤ D := hD.2 E hE (StarSubalgebra.le_topologicalClosure D)77 have heq : E = D := le_antisymm hED (StarSubalgebra.le_topologicalClosure D)78 rw [← heq]79 exact StarSubalgebra.isClosed_topologicalClosure D8081/-- A self-adjoint element commuting with a maximal abelian star subalgebra82belongs to that subalgebra. -/83theorem IsMaximalAbelian.mem_of_isSelfAdjoint_of_commute84 {D : StarSubalgebra ℂ A} (hD : IsMaximalAbelian D)85 {x : A} (hx : IsSelfAdjoint x)86 (hcomm : ∀ d : D, x * (d : A) = (d : A) * x) : x ∈ D := by87 let S : Set A := insert x (D : Set A)88 have hpair : ∀ y ∈ S, ∀ z ∈ S, y * z = z * y := by89 intro y hy z hz90 change y = x ∨ y ∈ D at hy91 change z = x ∨ z ∈ D at hz92 rcases hy with rfl | hy <;> rcases hz with rfl | hz93 · rfl94 · exact hcomm ⟨z, hz⟩95 · exact (hcomm ⟨y, hy⟩).symm96 · letI : IsMulCommutative D := hD.197 exact congrArg Subtype.val (mul_comm' (⟨y, hy⟩ : D) (⟨z, hz⟩ : D))98 have hstarS : ∀ y ∈ S, star y ∈ S := by99 intro y hy100 change y = x ∨ y ∈ D at hy101 change star y = x ∨ star y ∈ D102 rcases hy with rfl | hy103 · exact Or.inl hx.star_eq104 · exact Or.inr (star_mem hy)105 let E : StarSubalgebra ℂ A := StarAlgebra.adjoin ℂ S106 have hE : IsMulCommutative E :=107 StarAlgebra.isMulCommutative_adjoin ℂ hpair108 (fun y hy z hz => hpair y hy (star z) (hstarS z hz))109 have hDE : D ≤ E := by110 intro d hd111 exact StarAlgebra.subset_adjoin ℂ S (show (d : A) ∈ S from Or.inr hd)112 have hED : E ≤ D := hD.2 E hE hDE113 exact hED (StarAlgebra.subset_adjoin ℂ S (show x ∈ S from Or.inl rfl))114115/-- A maximal abelian star subalgebra equals its commutant: no116self-adjointness assumption on the commuting element is needed. -/117theorem IsMaximalAbelian.mem_of_commute118 {D : StarSubalgebra ℂ A} (hD : IsMaximalAbelian D)119 {x : A} (hcomm : ∀ d : D, x * (d : A) = (d : A) * x) : x ∈ D := by120 have hxcomm (d : D) : Commute x (d : A) := hcomm d121 have hstarcomm (d : D) : Commute (star x) (d : A) := by122 have h := hxcomm (star d)123 change Commute x (star (d : A)) at h124 exact h.star_left125 have hrcomm (d : D) : (ℜ x : A) * (d : A) = (d : A) * (ℜ x : A) := by126 rw [realPart_apply_coe]127 exact ((hxcomm d).add_left (hstarcomm d)).smul_left (2 : ℝ)⁻¹128 have hicomm (d : D) : (ℑ x : A) * (d : A) = (d : A) * (ℑ x : A) := by129 rw [imaginaryPart_apply_coe]130 exact (((hxcomm d).sub_left (hstarcomm d)).smul_left (2 : ℝ)⁻¹).smul_left (-Complex.I)131 have hr : (ℜ x : A) ∈ D :=132 hD.mem_of_isSelfAdjoint_of_commute (ℜ x).property hrcomm133 have hi : (ℑ x : A) ∈ D :=134 hD.mem_of_isSelfAdjoint_of_commute (ℑ x).property hicomm135 rw [← realPart_add_I_smul_imaginaryPart x]136 exact D.add_mem hr (D.smul_mem hi Complex.I)137138end MathlibAnnex.Analysis.CStarAlgebra