Exact source: MathlibAnnex/Analysis/CStarAlgebra/NonUnital/Singleton.lean
Pinned GitHub source · Raw UTF-8 source
Back to A projection represented by a rank-one operator · Back to A singleton model is faithful and exactly compact-valued · Back to Faithfulness from a unique irreducible class · Back to Every operator in a singleton image is compact
1import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.Representation2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Faithful34/-!5# Singleton irreducible models of genuinely nonunital C-star algebras6-/78set_option autoImplicit false910open scoped ComplexOrder InnerProduct1112namespace MathlibAnnex.Analysis.CStarAlgebra1314universe u v w1516variable {A : Type u} [NonUnitalCStarAlgebra A]17 [PartialOrder A] [StarOrderedRing A]18variable {H : Type v}19variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2021namespace NonUnitalCStarRepresentation2223/-- A displayed nonzero irreducible representation representing every24nonzero irreducible representation of a genuinely nonunital C-star algebra.25Faithfulness is deliberately not part of this predicate. -/26def IsSingletonIrreducibleModel27 (pi : NonUnitalCStarRepresentation A H) : Prop :=28 pi.IsIrreducible ∧29 ∀ (K : Type w) [NormedAddCommGroup K] [InnerProductSpace ℂ K]30 [CompleteSpace K] (rho : NonUnitalCStarRepresentation A K),31 rho.IsIrreducible → pi.UnitaryEquivalent rho3233/-- Pure-state separation in the minimal unitization proves faithfulness of a34singleton irreducible model without assuming that the original algebra has a35unit. -/36theorem injective_of_singleton [Nontrivial A]37 (pi : NonUnitalCStarRepresentation A H)38 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :39 Function.Injective pi := by40 intro x y hxy41 let a : A := x - y42 have hpia : pi a = 0 := by43 simp only [a, map_sub, hxy, sub_self]44 have hazero : a = 0 := by45 by_contra hane46 let ainr : Unitization ℂ A := Unitization.inr a47 have hainr : ainr ≠ 0 := by48 intro hzero49 apply hane50 apply Unitization.inr_injective (R := ℂ)51 simpa [ainr] using hzero52 obtain ⟨phi, hphi, hpure, hdetect⟩ :=53 exists_pureState_nonzero_on_star_mul_self (A := Unitization ℂ A) hainr54 let f : Unitization ℂ A →ₚ[ℂ] ℂ :=55 positiveLinearMapOfMemStateSpace phi hphi56 let rhoU : Representation (Unitization ℂ A) f.GNS := f.gnsStarAlgHom57 let rho : NonUnitalCStarRepresentation A f.GNS :=58 rhoU.toNonUnitalStarAlgHom.comp59 (Unitization.inrNonUnitalStarAlgHom ℂ A)60 have hrhoa : rho a ≠ 0 := by61 intro hzero62 have hrhoUa : rhoU ainr = 0 := by63 simpa [rho, rhoU, ainr] using hzero64 apply hdetect65 calc66 phi (star ainr * ainr) = f (star ainr * ainr) := rfl67 _ = inner ℂ f.gnsCyclicVector68 (rhoU (star ainr * ainr) f.gnsCyclicVector) :=69 (PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f _).symm70 _ = 0 := by rw [map_mul, map_star, hrhoUa]; simp71 have hxi : ‖f.gnsCyclicVector‖ = 1 :=72 PositiveLinearMap.norm_gnsCyclicVector f73 (positiveLinearMapOfMemStateSpace_one phi hphi)74 have hxi_ne : f.gnsCyclicVector ≠ 0 := by75 intro hzero76 simp [hzero] at hxi77 letI : Nontrivial f.GNS :=78 nontrivial_of_ne f.gnsCyclicVector 0 hxi_ne79 have hirrU : rhoU.IsIrreducible :=80 (Representation.isIrreducible_iff_starAlgHom rhoU).281 (isIrreducible_pureState_gnsStarAlgHom phi hphi hpure)82 have hirr : rho.IsIrreducible :=83 isIrreducible_restriction_of_isIrreducible_unitization rhoU hirrU84 ⟨a, hrhoa⟩85 obtain ⟨U, hU⟩ := hsingle.2 f.GNS rho hirr86 have hrhozero : rho a = 0 := by87 apply ContinuousLinearMap.ext88 intro z89 obtain ⟨q, rfl⟩ := U.surjective z90 calc91 rho a (U q) = U (pi a q) := (hU a q).symm92 _ = 0 := by rw [hpia]; simp93 exact hrhoa hrhozero94 exact sub_eq_zero.mp hazero9596end NonUnitalCStarRepresentation9798end MathlibAnnex.Analysis.CStarAlgebra