Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/OrdinarySingleton.lean
Pinned GitHub source · Raw UTF-8 source
Back to Finite-dimensional algebra in the unital singleton case · Back to An infinite-dimensional unital algebra has no separable singleton model
1import MathlibAnnex.Analysis.CStarAlgebra.Representation.FullImage2import MathlibAnnex.Analysis.CStarAlgebra.Representation.NonUnital34/-!5# Singleton models quantified over ordinary possibly nonunital representations67The represented algebra in this file is unital, but competitors are ordinary8star-algebra maps which are not assumed to preserve the unit. Nonzero9irreducibility forces such a competitor to preserve the unit.10-/1112set_option autoImplicit false1314open scoped ComplexOrder1516namespace MathlibAnnex.Analysis.CStarAlgebra1718universe u v w1920variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]21variable {H : Type v}22variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2324namespace NonUnitalRepresentation2526/-- Forgetting unitality preserves the explicitly nonzero irreducibility27predicate. -/28theorem isIrreducible_toNonUnitalStarAlgHom29 (pi : Representation A H) (hirr : pi.IsIrreducible) :30 IsIrreducible pi.toNonUnitalStarAlgHom := by31 exact ⟨hirr.1, hirr.2⟩3233end NonUnitalRepresentation3435namespace Representation3637/-- Raw singleton-spectrum hypothesis for a unital algebra, with every38ordinary nonzero irreducible representation included and no faithfulness39built into the definition. -/40def IsSingletonIrreducibleModelAmongNonUnital41 (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)4748/-- Quantifying over possibly nonunital competitors implies the corresponding49raw singleton statement for unital representations. -/50theorem IsSingletonIrreducibleModelAmongNonUnital.isSingletonIrreducibleModel51 {pi : Representation A H}52 (hpi : IsSingletonIrreducibleModelAmongNonUnital.{u, v, w} pi) :53 IsSingletonIrreducibleModel.{u, v, w} pi := by54 refine ⟨hpi.1, ?_⟩55 intro K _ _ _ rho hrho56 let rhoNU : NonUnitalRepresentation (A := A) (H := K) :=57 rho.toNonUnitalStarAlgHom58 have hrhoNU : rhoNU.IsIrreducible :=59 NonUnitalRepresentation.isIrreducible_toNonUnitalStarAlgHom rho hrho60 obtain ⟨U, hU⟩ := hpi.2 K rhoNU hrhoNU61 refine ⟨U, ?_⟩62 intro a x63 simpa [rhoNU] using hU a x6465/-- Conversely, a raw singleton statement for unital representations covers66all nonzero irreducible possibly nonunital competitors. -/67theorem IsSingletonIrreducibleModel.isSingletonIrreducibleModelAmongNonUnital68 {pi : Representation A H}69 (hpi : IsSingletonIrreducibleModel.{u, v, w} pi) :70 IsSingletonIrreducibleModelAmongNonUnital.{u, v, w} pi := by71 refine ⟨hpi.1, ?_⟩72 intro K _ _ _ rho hrho73 exact hpi.2 K (rho.toUnital hrho)74 (NonUnitalRepresentation.isIrreducible_toUnital rho hrho)7576/-- Unital Rosenberg conclusion with the quantifier ranging over ordinary77possibly nonunital nonzero irreducible representations. -/78theorem faithful_and_compactOperatorModel_of_singleton_amongNonUnital79 [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 pi85 hsingle.isSingletonIrreducibleModel8687/-- The representation space is finite-dimensional under the ordinary88possibly nonunital singleton quantifier. -/89theorem finiteDimensional_space_of_singleton_amongNonUnital90 [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.isSingletonIrreducibleModel9596/-- The unital algebra is finite-dimensional under the ordinary possibly97nonunital singleton quantifier. -/98theorem finiteDimensional_algebra_of_singleton_amongNonUnital99 [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.isSingletonIrreducibleModel104105/-- A nonzero infinite-dimensional unital C-star algebra cannot have a106separable nonzero irreducible representation representing its only ordinary107unitary-equivalence class. -/108theorem not_singleton_amongNonUnital_of_infiniteDimensional109 [Nontrivial A] (hA : ¬ FiniteDimensional ℂ A)110 [TopologicalSpace.SeparableSpace H]111 (pi : Representation A H) :112 ¬ IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi := by113 intro hsingle114 exact hA (finiteDimensional_algebra_of_singleton_amongNonUnital pi hsingle)115116end Representation117118end MathlibAnnex.Analysis.CStarAlgebra