Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.CStarAlgebra.CAR.not_isIrreducible_of_separable
MathlibAnnex/Analysis/CStarAlgebra/CAR/SeparableIrreducible.lean · lines 24–56
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicCounterexample 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.OrdinarySingleton 3 4/-! 5# Excluding separable irreducible representations of the CAR main target 6 7The ordinary endpoint captures a representation on any independent Hilbert 8universe. Comparing two such captures through the fixed ambient inclusion 9gives the raw singleton hypothesis needed by the finite-dimensionality 10theorem, without assuming that an input nonunital representation preserves 11the unit. 12-/ 13 14set_option autoImplicit false 15 16noncomputable section 17 18namespace MathlibAnnex.CStarAlgebra.CAR 19 20open MathlibAnnex.Analysis.CStarAlgebra 21 22universe v 23 24/-- The main target admits no nonzero irreducible ordinary representation on 25a separable complete complex Hilbert space. The input representation is not 26assumed to preserve the unit. -/ 27theorem not_isIrreducible_of_separable 28 {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 29 [CompleteSpace H] [TopologicalSpace.SeparableSpace H] 30 (rho : NonUnitalRepresentation (A := AtomicCounterexampleAlgebra) (H := H)) : 31 ¬ rho.IsIrreducible := by 32 intro hrho 33 let pi : Representation AtomicCounterexampleAlgebra H := rho.toUnital hrho 34 have hpi : Representation.IsIrreducible pi := 35 NonUnitalRepresentation.isIrreducible_toUnital rho hrho 36 have hambient_pi : atomicCounterexampleRepresentation.UnitaryEquivalent pi := by 37 obtain ⟨U, hU⟩ := (atomicCounterexampleEndpoint.{v}).captures_nonunital H rho hrho 38 refine ⟨U, ?_⟩ 39 intro a x 40 simpa [atomicCounterexampleRepresentation, pi] using hU a x 41 have hsingleton : 42 Representation.IsSingletonIrreducibleModelAmongNonUnital.{0, v, 0} pi := by 43 refine ⟨hpi, ?_⟩ 44 intro K _ _ _ sigma hsigma 45 have hambient_sigma : 46 atomicCounterexampleRepresentation.UnitaryEquivalent (sigma.toUnital hsigma) := by 47 obtain ⟨U, hU⟩ := (atomicCounterexampleEndpoint.{0}).captures_nonunital K sigma hsigma 48 refine ⟨U, ?_⟩ 49 intro a x 50 change U (atomicCounterexampleRepresentation a x) = sigma a (U x) 51 simpa [atomicCounterexampleRepresentation] using hU a x 52 exact Representation.unitaryEquivalent_trans 53 (Representation.unitaryEquivalent_symm hambient_pi) hambient_sigma 54 exact (atomicCounterexampleEndpoint.{v}).not_finiteDimensional_target 55 (Representation.finiteDimensional_algebra_of_singleton_amongNonUnital 56 pi hsingleton) 57 58end MathlibAnnex.CStarAlgebra.CAR