Exact source: MathlibAnnex/Analysis/CStarAlgebra/IsolatedCharacter.lean
Pinned GitHub source · Raw UTF-8 source
Back to A nonzero projection with scalar corner
1import Mathlib.Analysis.CStarAlgebra.GelfandDuality2import Mathlib.Topology.Algebra.Indicator34/-!5# Projections from isolated characters67Under the Gelfand transform, the characteristic function of an isolated8character is a nonzero projection. Its principal ideal inside the9commutative algebra is one-dimensional.10-/1112set_option autoImplicit false1314open Set1516namespace MathlibAnnex.Analysis.CStarAlgebra1718universe u1920variable {D : Type u} [CommCStarAlgebra D] [Nontrivial D]2122/-- An isolated character produces a nonzero projection `p` satisfying23`p * d = chi d • p` for every `d`. -/24theorem exists_projection_mul_eq_smul_of_isOpen_singleton25 (chi : WeakDual.characterSpace ℂ D)26 (hopen : IsOpen ({chi} : Set (WeakDual.characterSpace ℂ D))) :27 ∃ p : D, IsStarProjection p ∧ p ≠ 0 ∧28 ∀ d : D, p * d = chi d • p := by29 have hclopen : IsClopen ({chi} : Set (WeakDual.characterSpace ℂ D)) :=30 ⟨isClosed_singleton, hopen⟩31 let e : WeakDual.characterSpace ℂ D → ℂ :=32 Set.indicator ({chi} : Set (WeakDual.characterSpace ℂ D)) (fun _ => 1)33 have he : Continuous e := hclopen.continuous_indicator continuous_const34 let F : C(WeakDual.characterSpace ℂ D, ℂ) := ⟨e, he⟩35 have hF : IsStarProjection F := by36 rw [isStarProjection_iff']37 constructor38 · ext psi39 by_cases hpsi : psi = chi40 · simp [F, e, hpsi]41 · simp [F, e, hpsi]42 · ext psi43 by_cases hpsi : psi = chi44 · simp [F, e, hpsi]45 · simp [F, e, hpsi]46 let p : D := (gelfandStarTransform D).symm F47 have hp : IsStarProjection p := hF.map (gelfandStarTransform D).symm48 have hptransform : gelfandStarTransform D p = F :=49 (gelfandStarTransform D).apply_symm_apply F50 have hpvalue : chi p = 1 := by51 change (gelfandStarTransform D p) chi = 152 rw [hptransform]53 simp [F, e]54 have hpne : p ≠ 0 := by55 intro hzero56 rw [hzero, map_zero] at hpvalue57 exact zero_ne_one hpvalue58 refine ⟨p, hp, hpne, ?_⟩59 intro d60 apply (gelfandStarTransform D).injective61 ext psi62 change psi (p * d) = psi (chi d • p)63 by_cases hpsi : psi = chi64 · subst psi65 simp [hpvalue]66 · have hpzero : psi p = 0 := by67 change (gelfandStarTransform D p) psi = 068 rw [hptransform]69 simp [F, e, hpsi]70 simp [hpzero]7172end MathlibAnnex.Analysis.CStarAlgebra