MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.Analysis.CStarAlgebra.IsMaximalAbelian
def IsMaximalAbelian (D : StarSubalgebra ℂ A) : Prop
1 import Mathlib.Order.Zorn 2 import Mathlib.Algebra.Star.Subalgebra 3 import Mathlib.Topology.Algebra.StarSubalgebra 4 import Mathlib.Analysis.CStarAlgebra.Classes 5 import Mathlib.LinearAlgebra.Complex.Module 6 7 /-! 8 # Maximal abelian star subalgebras 9 10 This file constructs maximal commutative unital star subalgebras by Zorn's 11 lemma and records that they are norm closed in a C-star algebra. 12 -/ 13 14 set_option autoImplicit false 15 16 open Set 17 open scoped ComplexStarModule 18 19 namespace MathlibAnnex.Analysis.CStarAlgebra 20 21 universe u 22 23 variable {A : Type u} [CStarAlgebra A] 24 25 /-- A maximal abelian unital star subalgebra, expressed without installing a 26 global commutative-ring instance on its subtype. -/ 27 def IsMaximalAbelian (D : StarSubalgebra ℂ A) : Prop := 28 IsMulCommutative D ∧ 29 ∀ E : StarSubalgebra ℂ A, IsMulCommutative E → D ≤ E → E ≤ D 30 31 /-- Every unital C-star algebra has a maximal abelian star subalgebra. -/ 32 theorem exists_maximalAbelian : 33 ∃ D : StarSubalgebra ℂ A, IsMaximalAbelian D := by 34 let S : Set (StarSubalgebra ℂ A) := {D | IsMulCommutative D} 35 have hbot : (⊥ : StarSubalgebra ℂ A) ∈ S := by 36 change IsMulCommutative (⊥ : StarSubalgebra ℂ A) 37 refine IsMulCommutative.of_comm fun x y => ?_ 38 apply Subtype.ext 39 obtain ⟨r, hr⟩ := x.2 40 obtain ⟨s, hs⟩ := y.2 41 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 => by 46 letI : Nonempty c := ⟨⟨y, hy⟩⟩ 47 let F : c → StarSubalgebra ℂ A := fun d => d.1 48 have hdir : Directed (· ≤ ·) F := by 49 intro i j 50 by_cases hij' : i = j 51 · subst j 52 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 | hji 56 · exact ⟨j, hij, le_rfl⟩ 57 · exact ⟨i, le_rfl, hji⟩ 58 letI (d : c) : IsMulCommutative (F d) := hcS d.2 59 refine ⟨⨆ d : c, F d, ?_, ?_⟩ 60 · change IsMulCommutative (↥(⨆ d : c, F d)) 61 exact StarSubalgebra.isMulCommutative_iSup hdir 62 · intro z hz 63 exact le_iSup F ⟨z, hz⟩) 64 (⊥ : StarSubalgebra ℂ A) hbot 65 exact ⟨D, hD, fun E hE hDE => hmax hE hDE⟩ 66 67 /-- Maximal abelian star subalgebras of a C-star algebra are norm closed. -/ 68 theorem IsMaximalAbelian.isClosed {D : StarSubalgebra ℂ A} 69 (hD : IsMaximalAbelian D) : IsClosed (D : Set A) := by 70 let E : StarSubalgebra ℂ A := D.topologicalClosure 71 have hE : IsMulCommutative E := by 72 letI : IsMulCommutative D := hD.1 73 letI : CommRing E := 74 StarSubalgebra.commRingTopologicalClosure D (fun x y => mul_comm' x y) 75 infer_instance 76 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 D 80 81 /-- A self-adjoint element commuting with a maximal abelian star subalgebra 82 belongs to that subalgebra. -/ 83 theorem IsMaximalAbelian.mem_of_isSelfAdjoint_of_commute 84 {D : StarSubalgebra ℂ A} (hD : IsMaximalAbelian D) 85 {x : A} (hx : IsSelfAdjoint x) 86 (hcomm : ∀ d : D, x * (d : A) = (d : A) * x) : x ∈ D := by 87 let S : Set A := insert x (D : Set A) 88 have hpair : ∀ y ∈ S, ∀ z ∈ S, y * z = z * y := by 89 intro y hy z hz 90 change y = x ∨ y ∈ D at hy 91 change z = x ∨ z ∈ D at hz 92 rcases hy with rfl | hy <;> rcases hz with rfl | hz 93 · rfl 94 · exact hcomm ⟨z, hz⟩ 95 · exact (hcomm ⟨y, hy⟩).symm 96 · letI : IsMulCommutative D := hD.1 97 exact congrArg Subtype.val (mul_comm' (⟨y, hy⟩ : D) (⟨z, hz⟩ : D)) 98 have hstarS : ∀ y ∈ S, star y ∈ S := by 99 intro y hy 100 change y = x ∨ y ∈ D at hy 101 change star y = x ∨ star y ∈ D 102 rcases hy with rfl | hy 103 · exact Or.inl hx.star_eq 104 · exact Or.inr (star_mem hy) 105 let E : StarSubalgebra ℂ A := StarAlgebra.adjoin ℂ S 106 have hE : IsMulCommutative E := 107 StarAlgebra.isMulCommutative_adjoin ℂ hpair 108 (fun y hy z hz => hpair y hy (star z) (hstarS z hz)) 109 have hDE : D ≤ E := by 110 intro d hd 111 exact StarAlgebra.subset_adjoin ℂ S (show (d : A) ∈ S from Or.inr hd) 112 have hED : E ≤ D := hD.2 E hE hDE 113 exact hED (StarAlgebra.subset_adjoin ℂ S (show x ∈ S from Or.inl rfl)) 114 115 /-- A maximal abelian star subalgebra equals its commutant: no 116 self-adjointness assumption on the commuting element is needed. -/ 117 theorem IsMaximalAbelian.mem_of_commute 118 {D : StarSubalgebra ℂ A} (hD : IsMaximalAbelian D) 119 {x : A} (hcomm : ∀ d : D, x * (d : A) = (d : A) * x) : x ∈ D := by 120 have hxcomm (d : D) : Commute x (d : A) := hcomm d 121 have hstarcomm (d : D) : Commute (star x) (d : A) := by 122 have h := hxcomm (star d) 123 change Commute x (star (d : A)) at h 124 exact h.star_left 125 have hrcomm (d : D) : (ℜ x : A) * (d : A) = (d : A) * (ℜ x : A) := by 126 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) := by 129 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 hrcomm 133 have hi : (ℑ x : A) ∈ D := 134 hD.mem_of_isSelfAdjoint_of_commute (ℑ x).property hicomm 135 rw [← realPart_add_I_smul_imaginaryPart x] 136 exact D.add_mem hr (D.smul_mem hi Complex.I) 137 138 end MathlibAnnex.Analysis.CStarAlgebra