Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/MinimalProjection.lean
Pinned GitHub source · Raw UTF-8 source
Back to A unital singleton model acts in finite dimension
1import Mathlib.Topology.Baire.LocallyCompactRegular2import MathlibAnnex.Topology.CountableBaire3import MathlibAnnex.Analysis.CStarAlgebra.IsolatedCharacter4import MathlibAnnex.Analysis.CStarAlgebra.MaximalAbelian5import MathlibAnnex.Analysis.CStarAlgebra.Representation.CharacterCountable67/-!8# A minimal projection from a separable singleton model9-/1011set_option autoImplicit false1213open Set14open scoped ComplexOrder IsMulCommutative1516namespace MathlibAnnex.Analysis.CStarAlgebra1718universe u v1920variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]21variable {H : Type v}22variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2324/-- The projection belonging to an isolated character of a maximal abelian25subalgebra has a one-dimensional corner in the ambient algebra. -/26theorem corner_eq_smul_of_maximalAbelian27 (D : StarSubalgebra ℂ A) (hD : IsMaximalAbelian D)28 (chi : WeakDual.characterSpace ℂ D) (p : D)29 (hp : IsStarProjection p)30 (hpd : ∀ d : D, p * d = chi d • p) :31 ∀ a : A, ∃ c : ℂ, (p : A) * a * (p : A) = c • (p : A) := by32 letI : IsMulCommutative D := hD.133 intro a34 let x : A := (p : A) * a * (p : A)35 have hpda (d : D) : (p : A) * (d : A) = chi d • (p : A) :=36 congrArg Subtype.val (hpd d)37 have hdpa (d : D) : (d : A) * (p : A) = chi d • (p : A) := by38 calc39 (d : A) * (p : A) = ((d * p : D) : A) := rfl40 _ = ((p * d : D) : A) := congrArg Subtype.val (mul_comm' d p)41 _ = chi d • (p : A) := hpda d42 have hxcomm (d : D) : x * (d : A) = (d : A) * x := by43 calc44 x * (d : A) = (p : A) * a * ((p : A) * (d : A)) := by simp [x, mul_assoc]45 _ = (p : A) * a * (chi d • (p : A)) := by rw [hpda d]46 _ = chi d • x := by simp [x, mul_assoc]47 _ = (chi d • (p : A)) * a * (p : A) := by simp [x, mul_assoc]48 _ = ((d : A) * (p : A)) * a * (p : A) := by rw [hdpa d]49 _ = (d : A) * x := by simp [x, mul_assoc]50 have hxmem : x ∈ D := hD.mem_of_commute hxcomm51 let xd : D := ⟨x, hxmem⟩52 have hcorner := congrArg Subtype.val (hpd xd)53 change (p : A) * x = chi xd • (p : A) at hcorner54 have hpidem : (p : A) * (p : A) = (p : A) :=55 congrArg Subtype.val hp.isIdempotentElem.eq56 have hpx : (p : A) * x = x := by57 calc58 (p : A) * x = ((p : A) * (p : A)) * a * (p : A) := by59 simp [x, mul_assoc]60 _ = x := by rw [hpidem]61 refine ⟨chi xd, ?_⟩62 change x = chi xd • (p : A)63 exact hpx.symm.trans hcorner6465namespace Representation6667/-- A separable singleton irreducible model forces the ambient unital68C-star algebra to contain a nonzero projection with scalar corner. -/69theorem exists_nonzero_projection_scalar_corner [Nontrivial A]70 [TopologicalSpace.SeparableSpace H]71 (pi : Representation A H)72 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :73 ∃ p : A, IsStarProjection p ∧ p ≠ 0 ∧74 ∀ a : A, ∃ c : ℂ, p * a * p = c • p := by75 obtain ⟨D, hD⟩ := exists_maximalAbelian (A := A)76 letI : IsClosed (D : Set A) := hD.isClosed77 letI : IsMulCommutative D := hD.178 letI : CommCStarAlgebra D := {}79 have hcount := countable_characterSpace_of_singleton pi hsingle D80 letI : Countable (WeakDual.characterSpace ℂ D) := hcount81 obtain ⟨chi, hchi⟩ :=82 MathlibAnnex.Topology.exists_isOpen_singleton83 (X := WeakDual.characterSpace ℂ D)84 obtain ⟨p, hp, hpne, hpd⟩ :=85 exists_projection_mul_eq_smul_of_isOpen_singleton chi hchi86 refine ⟨(p : A), hp.map D.subtype, ?_,87 corner_eq_smul_of_maximalAbelian D hD chi p hp hpd⟩88 intro hzero89 apply hpne90 apply Subtype.ext91 exact hzero9293end Representation9495end MathlibAnnex.Analysis.CStarAlgebra