MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.Representation.not_singleton_amongNonUnital_of_infiniteDimensional

Raw UTF-8 source

theorem not_singleton_amongNonUnital_of_infiniteDimensional
    [Nontrivial A] (hA : ¬ FiniteDimensional ℂ A)
    [TopologicalSpace.SeparableSpace H]
    (pi : Representation A H) :
    ¬ IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi

1 import MathlibAnnex.Analysis.CStarAlgebra.Representation.FullImage
2 import MathlibAnnex.Analysis.CStarAlgebra.Representation.NonUnital
3 
4 /-!
5 # Singleton models quantified over ordinary possibly nonunital representations
6 
7 The represented algebra in this file is unital, but competitors are ordinary
8 star-algebra maps which are not assumed to preserve the unit.  Nonzero
9 irreducibility forces such a competitor to preserve the unit.
10 -/
11 
12 set_option autoImplicit false
13 
14 open scoped ComplexOrder
15 
16 namespace MathlibAnnex.Analysis.CStarAlgebra
17 
18 universe u v w
19 
20 variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
21 variable {H : Type v}
22 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
23 
24 namespace NonUnitalRepresentation
25 
26 /-- Forgetting unitality preserves the explicitly nonzero irreducibility
27 predicate. -/
28 theorem isIrreducible_toNonUnitalStarAlgHom
29     (pi : Representation A H) (hirr : pi.IsIrreducible) :
30     IsIrreducible pi.toNonUnitalStarAlgHom := by
31   exact ⟨hirr.1, hirr.2⟩
32 
33 end NonUnitalRepresentation
34 
35 namespace Representation
36 
37 /-- Raw singleton-spectrum hypothesis for a unital algebra, with every
38 ordinary nonzero irreducible representation included and no faithfulness
39 built into the definition. -/
40 def 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
49 raw singleton statement for unital representations. -/
50 theorem 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
66 all nonzero irreducible possibly nonunital competitors. -/
67 theorem 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
77 possibly nonunital nonzero irreducible representations. -/
78 theorem 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
88 possibly nonunital singleton quantifier. -/
89 theorem 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
97 nonunital singleton quantifier. -/
98 theorem 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
106 separable nonzero irreducible representation representing its only ordinary
107 unitary-equivalence class. -/
108 theorem 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 
116 end Representation
117 
118 end MathlibAnnex.Analysis.CStarAlgebra