Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_algebra_of_singleton_amongNonUnital
MathlibAnnex/Analysis/CStarAlgebra/Representation/OrdinarySingleton.lean · lines 96–103
1import MathlibAnnex.Analysis.CStarAlgebra.Representation.FullImage 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.NonUnital 3 4/-! 5# Singleton models quantified over ordinary possibly nonunital representations 6 7The represented algebra in this file is unital, but competitors are ordinary 8star-algebra maps which are not assumed to preserve the unit. Nonzero 9irreducibility forces such a competitor to preserve the unit. 10-/ 11 12set_option autoImplicit false 13 14open scoped ComplexOrder 15 16namespace MathlibAnnex.Analysis.CStarAlgebra 17 18universe u v w 19 20variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 21variable {H : Type v} 22variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 23 24namespace NonUnitalRepresentation 25 26/-- Forgetting unitality preserves the explicitly nonzero irreducibility 27predicate. -/ 28theorem isIrreducible_toNonUnitalStarAlgHom 29 (pi : Representation A H) (hirr : pi.IsIrreducible) : 30 IsIrreducible pi.toNonUnitalStarAlgHom := by 31 exact ⟨hirr.1, hirr.2⟩ 32 33end NonUnitalRepresentation 34 35namespace Representation 36 37/-- Raw singleton-spectrum hypothesis for a unital algebra, with every 38ordinary nonzero irreducible representation included and no faithfulness 39built into the definition. -/ 40def IsSingletonIrreducibleModelAmongNonUnital 41 (pi : Representation A H) : Prop := 42 pi.IsIrreducible ∧ 43 ∀ (K : Type w) [NormedAddCommGroup K] [InnerProductSpace ℂ K] 44 [CompleteSpace K] (rho : NonUnitalRepresentation (A := A) (H := K)), 45 ∀ hrho : rho.IsIrreducible, 46 pi.UnitaryEquivalent (rho.toUnital hrho) 47 48/-- Quantifying over possibly nonunital competitors implies the corresponding 49raw singleton statement for unital representations. -/ 50theorem IsSingletonIrreducibleModelAmongNonUnital.isSingletonIrreducibleModel 51 {pi : Representation A H} 52 (hpi : IsSingletonIrreducibleModelAmongNonUnital.{u, v, w} pi) : 53 IsSingletonIrreducibleModel.{u, v, w} pi := by 54 refine ⟨hpi.1, ?_⟩ 55 intro K _ _ _ rho hrho 56 let rhoNU : NonUnitalRepresentation (A := A) (H := K) := 57 rho.toNonUnitalStarAlgHom 58 have hrhoNU : rhoNU.IsIrreducible := 59 NonUnitalRepresentation.isIrreducible_toNonUnitalStarAlgHom rho hrho 60 obtain ⟨U, hU⟩ := hpi.2 K rhoNU hrhoNU 61 refine ⟨U, ?_⟩ 62 intro a x 63 simpa [rhoNU] using hU a x 64 65/-- Conversely, a raw singleton statement for unital representations covers 66all nonzero irreducible possibly nonunital competitors. -/ 67theorem IsSingletonIrreducibleModel.isSingletonIrreducibleModelAmongNonUnital 68 {pi : Representation A H} 69 (hpi : IsSingletonIrreducibleModel.{u, v, w} pi) : 70 IsSingletonIrreducibleModelAmongNonUnital.{u, v, w} pi := by 71 refine ⟨hpi.1, ?_⟩ 72 intro K _ _ _ rho hrho 73 exact hpi.2 K (rho.toUnital hrho) 74 (NonUnitalRepresentation.isIrreducible_toUnital rho hrho) 75 76/-- Unital Rosenberg conclusion with the quantifier ranging over ordinary 77possibly nonunital nonzero irreducible representations. -/ 78theorem faithful_and_compactOperatorModel_of_singleton_amongNonUnital 79 [Nontrivial A] [TopologicalSpace.SeparableSpace H] 80 (pi : Representation A H) 81 (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi) : 82 Function.Injective pi ∧ 83 IsCompactOperatorModel pi.toNonUnitalStarAlgHom := 84 faithful_and_compactOperatorModel_of_singleton pi 85 hsingle.isSingletonIrreducibleModel 86 87/-- The representation space is finite-dimensional under the ordinary 88possibly nonunital singleton quantifier. -/ 89theorem finiteDimensional_space_of_singleton_amongNonUnital 90 [Nontrivial A] [TopologicalSpace.SeparableSpace H] 91 (pi : Representation A H) 92 (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi) : 93 FiniteDimensional ℂ H := 94 finiteDimensional_space_of_singleton pi hsingle.isSingletonIrreducibleModel 95 96/-- The unital algebra is finite-dimensional under the ordinary possibly 97nonunital singleton quantifier. -/ 98theorem finiteDimensional_algebra_of_singleton_amongNonUnital 99 [Nontrivial A] [TopologicalSpace.SeparableSpace H] 100 (pi : Representation A H) 101 (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi) : 102 FiniteDimensional ℂ A := 103 finiteDimensional_algebra_of_singleton pi hsingle.isSingletonIrreducibleModel 104 105/-- A nonzero infinite-dimensional unital C-star algebra cannot have a 106separable nonzero irreducible representation representing its only ordinary 107unitary-equivalence class. -/ 108theorem not_singleton_amongNonUnital_of_infiniteDimensional 109 [Nontrivial A] (hA : ¬ FiniteDimensional ℂ A) 110 [TopologicalSpace.SeparableSpace H] 111 (pi : Representation A H) : 112 ¬ IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi := by 113 intro hsingle 114 exact hA (finiteDimensional_algebra_of_singleton_amongNonUnital pi hsingle) 115 116end Representation 117 118end MathlibAnnex.Analysis.CStarAlgebra