Exact source: MathlibAnnex/Analysis/CStarAlgebra/NonUnital/MinimalProjection.lean
Pinned GitHub source · Raw UTF-8 source
Back to A projection represented by a rank-one operator · Back to A nonzero projection with scalar corner
1import Mathlib.Topology.Baire.LocallyCompactRegular2import MathlibAnnex.Topology.CountableBaire3import MathlibAnnex.Analysis.CStarAlgebra.IsolatedCharacter4import MathlibAnnex.Analysis.CStarAlgebra.MaximalAbelianContaining5import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.CharacterCountable6import MathlibAnnex.Analysis.CStarAlgebra.Representation.MinimalProjection78/-!9# A minimal projection in a non-unital singleton model1011A maximal abelian subalgebra of the unitization is chosen to contain a12nonzero element of the original algebra. Its non-scalar character space is13a nonempty open countable Baire space, so it has an isolated point away from14the scalar character. The associated Gelfand projection consequently lies15in the original algebra.16-/1718set_option autoImplicit false1920open Set21open scoped ComplexOrder IsMulCommutative2223namespace MathlibAnnex.Analysis.CStarAlgebra2425universe u v2627variable {A : Type u} [NonUnitalCStarAlgebra A]28 [PartialOrder A] [StarOrderedRing A]29variable {H : Type v}30variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]3132namespace NonUnitalCStarRepresentation3334/-- If a closed commutative subalgebra of a minimal unitization contains a35nonzero element with zero scalar coordinate, its countable character space36has an isolated character different from the scalar character. -/37theorem exists_isolated_character_ne_infinity38 (D : StarSubalgebra ℂ (Unitization ℂ A))39 [IsClosed (D : Set (Unitization ℂ A))]40 [IsMulCommutative D]41 [Countable (WeakDual.characterSpace ℂ D)]42 (d : D) (hd : d ≠ 0)43 (hdfst : (d : Unitization ℂ A).fst = 0) :44 ∃ chi : WeakDual.characterSpace ℂ D,45 chi ≠ infinityCharacterOn (A := A) D ∧46 IsOpen ({chi} : Set (WeakDual.characterSpace ℂ D)) := by47 letI : CommCStarAlgebra D := {}48 let X := WeakDual.characterSpace ℂ D49 let chiInf : X := infinityCharacterOn (A := A) D50 let U : Set X := {chiInf}ᶜ51 have hUopen : IsOpen U := isClosed_singleton.isOpen_compl52 have hchar : ∃ chi : X, chi d ≠ 0 := by53 by_contra hex54 have hall : ∀ chi : X, chi d = 0 := by55 intro chi56 by_contra hne57 exact hex ⟨chi, hne⟩58 apply hd59 apply (gelfandTransform_isometry D).injective60 ext chi61 simpa using hall chi62 have hUne : U.Nonempty := by63 obtain ⟨chi, hchi⟩ := hchar64 refine ⟨chi, ?_⟩65 change chi ≠ chiInf66 intro heq67 apply hchi68 rw [heq]69 exact hdfst70 letI : Nonempty U := hUne.to_subtype71 letI : BaireSpace U := hUopen.baireSpace72 obtain ⟨chi, hchiOpen⟩ :=73 MathlibAnnex.Topology.exists_isOpen_singleton (X := U)74 refine ⟨chi.1, chi.2, ?_⟩75 simpa using hUopen.isOpenMap_subtype_val ({chi} : Set U) hchiOpen7677/-- For the Gelfand projection attached to `chi`, every different character78vanishes on that projection. -/79theorem character_apply_eq_zero_of_projection_mul_eq_smul80 (D : StarSubalgebra ℂ (Unitization ℂ A))81 [IsClosed (D : Set (Unitization ℂ A))]82 [IsMulCommutative D]83 (chi psi : WeakDual.characterSpace ℂ D)84 (hchi : chi ≠ psi) (p : D) (hp : IsStarProjection p) (hpne : p ≠ 0)85 (hpd : ∀ d : D, p * d = chi d • p) :86 psi p = 0 := by87 have hchip : chi p = 1 := by88 apply smul_left_injective ℂ hpne89 calc90 (chi p) • p = p * p := (hpd p).symm91 _ = p := hp.isIdempotentElem.eq92 _ = (1 : ℂ) • p := (one_smul ℂ p).symm93 by_contra hpsine94 apply hchi95 apply WeakDual.CharacterSpace.ext96 intro d97 have heq := congrArg psi (hpd d)98 have heq' : psi p * psi d = psi p * chi d := by99 simpa [mul_comm (chi d) (psi p)] using heq100 exact (mul_left_cancel₀ hpsine heq').symm101102/-- A separable singleton irreducible model of a genuinely non-unital103C-star algebra forces a nonzero projection with scalar corner in that104algebra. -/105theorem exists_nonzero_projection_scalar_corner [Nontrivial A]106 [TopologicalSpace.SeparableSpace H]107 (pi : NonUnitalCStarRepresentation A H)108 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :109 ∃ p : A, IsStarProjection p ∧ p ≠ 0 ∧110 ∀ a : A, ∃ c : ℂ, p * a * p = c • p := by111 obtain ⟨a, ha⟩ : ∃ a : A, a ≠ 0 := exists_ne 0112 let b : A := star a * a113 have hbne : b ≠ 0 := CStarRing.star_mul_self_ne_zero_iff a |>.2 ha114 have hbself : IsSelfAdjoint b := IsSelfAdjoint.star_mul_self a115 have hbinrself : IsSelfAdjoint (b : Unitization ℂ A) := hbself.inr ℂ116 obtain ⟨D, hD, hbD⟩ :=117 exists_maximalAbelian_containing_isSelfAdjoint (b : Unitization ℂ A) hbinrself118 letI : IsClosed (D : Set (Unitization ℂ A)) := hD.isClosed119 letI : IsMulCommutative D := hD.1120 letI : CommCStarAlgebra D := {}121 let d : D := ⟨(b : Unitization ℂ A), hbD⟩122 have hdne : d ≠ 0 := by123 intro hzero124 apply hbne125 apply Unitization.inr_injective (R := ℂ)126 exact congrArg Subtype.val hzero127 have hdfst : (d : Unitization ℂ A).fst = 0 := rfl128 have hcount := countable_characterSpace_of_nonUnital_singleton pi hsingle D129 letI : Countable (WeakDual.characterSpace ℂ D) := hcount130 obtain ⟨chi, hchiInf, hchiOpen⟩ :=131 exists_isolated_character_ne_infinity D d hdne hdfst132 obtain ⟨p, hp, hpne, hpd⟩ :=133 exists_projection_mul_eq_smul_of_isOpen_singleton chi hchiOpen134 have hpInf : infinityCharacterOn (A := A) D p = 0 :=135 character_apply_eq_zero_of_projection_mul_eq_smul D chi136 (infinityCharacterOn (A := A) D) hchiInf p hp hpne hpd137 have hpfst : (p : Unitization ℂ A).fst = 0 := by138 simpa using hpInf139 let pA : A := (p : Unitization ℂ A).snd140 have hp_eq : (p : Unitization ℂ A) = (pA : Unitization ℂ A) := by141 ext <;> simp [pA, hpfst]142 have hpA : IsStarProjection pA := by143 apply IsStarProjection.of_inr (R := ℂ)144 rw [← hp_eq]145 exact hp.map D.subtype146 have hpAne : pA ≠ 0 := by147 intro hzero148 apply hpne149 apply Subtype.ext150 rw [hp_eq, hzero]151 rfl152 have hcornerU :=153 corner_eq_smul_of_maximalAbelian D hD chi p hp hpd154 refine ⟨pA, hpA, hpAne, ?_⟩155 intro x156 obtain ⟨c, hc⟩ := hcornerU (x : Unitization ℂ A)157 refine ⟨c, ?_⟩158 apply Unitization.inr_injective (R := ℂ)159 simpa [← hp_eq] using hc160161end NonUnitalCStarRepresentation162163end MathlibAnnex.Analysis.CStarAlgebra