Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/SeparableIrreducible.lean
Pinned GitHub source · Raw UTF-8 source
Back to A separably represented C*-algebra with no separable irreducible representation · Back to No nonzero irreducible representation on a separable Hilbert space
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicCounterexample2import MathlibAnnex.Analysis.CStarAlgebra.Representation.OrdinarySingleton34/-!5# Excluding separable irreducible representations of the CAR main target67The ordinary endpoint captures a representation on any independent Hilbert8universe. Comparing two such captures through the fixed ambient inclusion9gives the raw singleton hypothesis needed by the finite-dimensionality10theorem, without assuming that an input nonunital representation preserves11the unit.12-/1314set_option autoImplicit false1516noncomputable section1718namespace MathlibAnnex.CStarAlgebra.CAR1920open MathlibAnnex.Analysis.CStarAlgebra2122universe v2324/-- The main target admits no nonzero irreducible ordinary representation on25a separable complete complex Hilbert space. The input representation is not26assumed to preserve the unit. -/27theorem not_isIrreducible_of_separable28 {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H]29 [CompleteSpace H] [TopologicalSpace.SeparableSpace H]30 (rho : NonUnitalRepresentation (A := AtomicCounterexampleAlgebra) (H := H)) :31 ¬ rho.IsIrreducible := by32 intro hrho33 let pi : Representation AtomicCounterexampleAlgebra H := rho.toUnital hrho34 have hpi : Representation.IsIrreducible pi :=35 NonUnitalRepresentation.isIrreducible_toUnital rho hrho36 have hambient_pi : atomicCounterexampleRepresentation.UnitaryEquivalent pi := by37 obtain ⟨U, hU⟩ := (atomicCounterexampleEndpoint.{v}).captures_nonunital H rho hrho38 refine ⟨U, ?_⟩39 intro a x40 simpa [atomicCounterexampleRepresentation, pi] using hU a x41 have hsingleton :42 Representation.IsSingletonIrreducibleModelAmongNonUnital.{0, v, 0} pi := by43 refine ⟨hpi, ?_⟩44 intro K _ _ _ sigma hsigma45 have hambient_sigma :46 atomicCounterexampleRepresentation.UnitaryEquivalent (sigma.toUnital hsigma) := by47 obtain ⟨U, hU⟩ := (atomicCounterexampleEndpoint.{0}).captures_nonunital K sigma hsigma48 refine ⟨U, ?_⟩49 intro a x50 change U (atomicCounterexampleRepresentation a x) = sigma a (U x)51 simpa [atomicCounterexampleRepresentation] using hU a x52 exact Representation.unitaryEquivalent_trans53 (Representation.unitaryEquivalent_symm hambient_pi) hambient_sigma54 exact (atomicCounterexampleEndpoint.{v}).not_finiteDimensional_target55 (Representation.finiteDimensional_algebra_of_singleton_amongNonUnital56 pi hsingleton)5758end MathlibAnnex.CStarAlgebra.CAR