MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.injective_of_singleton
theorem injective_of_singleton [Nontrivial A]
(pi : NonUnitalCStarRepresentation A H)
(hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
Function.Injective pi1 import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.Representation 2 import MathlibAnnex.Analysis.CStarAlgebra.Representation.Faithful 3 4 /-! 5 # Singleton irreducible models of genuinely nonunital C-star algebras 6 -/ 7 8 set_option autoImplicit false 9 10 open scoped ComplexOrder InnerProduct 11 12 namespace MathlibAnnex.Analysis.CStarAlgebra 13 14 universe u v w 15 16 variable {A : Type u} [NonUnitalCStarAlgebra A] 17 [PartialOrder A] [StarOrderedRing A] 18 variable {H : Type v} 19 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 20 21 namespace NonUnitalCStarRepresentation 22 23 /-- A displayed nonzero irreducible representation representing every 24 nonzero irreducible representation of a genuinely nonunital C-star algebra. 25 Faithfulness is deliberately not part of this predicate. -/ 26 def IsSingletonIrreducibleModel 27 (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 rho 32 33 /-- Pure-state separation in the minimal unitization proves faithfulness of a 34 singleton irreducible model without assuming that the original algebra has a 35 unit. -/ 36 theorem injective_of_singleton [Nontrivial A] 37 (pi : NonUnitalCStarRepresentation A H) 38 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) : 39 Function.Injective pi := by 40 intro x y hxy 41 let a : A := x - y 42 have hpia : pi a = 0 := by 43 simp only [a, map_sub, hxy, sub_self] 44 have hazero : a = 0 := by 45 by_contra hane 46 let ainr : Unitization ℂ A := Unitization.inr a 47 have hainr : ainr ≠ 0 := by 48 intro hzero 49 apply hane 50 apply Unitization.inr_injective (R := ℂ) 51 simpa [ainr] using hzero 52 obtain ⟨phi, hphi, hpure, hdetect⟩ := 53 exists_pureState_nonzero_on_star_mul_self (A := Unitization ℂ A) hainr 54 let f : Unitization ℂ A →ₚ[ℂ] ℂ := 55 positiveLinearMapOfMemStateSpace phi hphi 56 let rhoU : Representation (Unitization ℂ A) f.GNS := f.gnsStarAlgHom 57 let rho : NonUnitalCStarRepresentation A f.GNS := 58 rhoU.toNonUnitalStarAlgHom.comp 59 (Unitization.inrNonUnitalStarAlgHom ℂ A) 60 have hrhoa : rho a ≠ 0 := by 61 intro hzero 62 have hrhoUa : rhoU ainr = 0 := by 63 simpa [rho, rhoU, ainr] using hzero 64 apply hdetect 65 calc 66 phi (star ainr * ainr) = f (star ainr * ainr) := rfl 67 _ = inner ℂ f.gnsCyclicVector 68 (rhoU (star ainr * ainr) f.gnsCyclicVector) := 69 (PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f _).symm 70 _ = 0 := by rw [map_mul, map_star, hrhoUa]; simp 71 have hxi : ‖f.gnsCyclicVector‖ = 1 := 72 PositiveLinearMap.norm_gnsCyclicVector f 73 (positiveLinearMapOfMemStateSpace_one phi hphi) 74 have hxi_ne : f.gnsCyclicVector ≠ 0 := by 75 intro hzero 76 simp [hzero] at hxi 77 letI : Nontrivial f.GNS := 78 nontrivial_of_ne f.gnsCyclicVector 0 hxi_ne 79 have hirrU : rhoU.IsIrreducible := 80 (Representation.isIrreducible_iff_starAlgHom rhoU).2 81 (isIrreducible_pureState_gnsStarAlgHom phi hphi hpure) 82 have hirr : rho.IsIrreducible := 83 isIrreducible_restriction_of_isIrreducible_unitization rhoU hirrU 84 ⟨a, hrhoa⟩ 85 obtain ⟨U, hU⟩ := hsingle.2 f.GNS rho hirr 86 have hrhozero : rho a = 0 := by 87 apply ContinuousLinearMap.ext 88 intro z 89 obtain ⟨q, rfl⟩ := U.surjective z 90 calc 91 rho a (U q) = U (pi a q) := (hU a q).symm 92 _ = 0 := by rw [hpia]; simp 93 exact hrhoa hrhozero 94 exact sub_eq_zero.mp hazero 95 96 end NonUnitalCStarRepresentation 97 98 end MathlibAnnex.Analysis.CStarAlgebra