MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.faithful_and_compactOperatorModel_of_singleton

Raw UTF-8 source

theorem faithful_and_compactOperatorModel_of_singleton [Nontrivial A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    Function.Injective pi ∧ IsCompactOperatorModel pi

1 import MathlibAnnex.Analysis.CStarAlgebra.CompactPreimage
2 import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.CompactExclusion
3 import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.CompactRange
4 import MathlibAnnex.Analysis.CStarAlgebra.State.Ideal
5 
6 /-!
7 # Compact-operator models for genuinely non-unital C-star algebras
8 
9 This file assembles the non-unital Rosenberg conclusion.  No unit is assumed
10 on the source algebra.  `NonUnital.CompactExclusion` proves directly that
11 every represented operator is compact, while `NonUnital.CompactRange` proves
12 the reverse range inclusion.  The older simplicity-based closure is retained
13 below as an independent conditional route.
14 -/
15 
16 set_option autoImplicit false
17 
18 namespace MathlibAnnex.Analysis.CStarAlgebra
19 
20 universe u v
21 
22 variable {A : Type u} [NonUnitalCStarAlgebra A]
23   [PartialOrder A] [StarOrderedRing A]
24 variable {H : Type v}
25 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
26 
27 namespace NonUnitalCStarRepresentation
28 
29 /-- A separable singleton irreducible representation of a nonzero possibly
30 non-unital complex C-star algebra is an exact model of the compact operators.
31 Neither simplicity nor faithfulness is assumed. -/
32 theorem isCompactOperatorModel_of_singleton [Nontrivial A]
33     [TopologicalSpace.SeparableSpace H]
34     (pi : NonUnitalCStarRepresentation A H)
35     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
36     IsCompactOperatorModel pi := by
37   exact ⟨injective_of_singleton pi hsingle,
38     isCompactOperator_map_of_singleton pi hsingle,
39     exists_preimage_of_compact_singleton pi hsingle⟩
40 
41 /-- Faithfulness and equality of the represented range with all compact
42 operators for a genuinely non-unital singleton model. -/
43 theorem faithful_and_compactOperatorModel_of_singleton [Nontrivial A]
44     [TopologicalSpace.SeparableSpace H]
45     (pi : NonUnitalCStarRepresentation A H)
46     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
47     Function.Injective pi ∧ IsCompactOperatorModel pi :=
48   ⟨injective_of_singleton pi hsingle,
49     isCompactOperatorModel_of_singleton pi hsingle⟩
50 
51 /-- Closed-ideal simplicity turns the one nonzero compact image supplied by
52 the singleton argument into compactness of the entire represented image. -/
53 theorem isCompactOperator_map_of_singleton_of_isSimple [Nontrivial A]
54     [TopologicalSpace.SeparableSpace H]
55     (pi : NonUnitalCStarRepresentation A H)
56     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
57     (hsimple : IsSimpleCStarAlgebra A) :
58     ∀ a : A, IsCompactOperator (pi a) := by
59   obtain ⟨p, _hp, hpne, _hrankOne, hpcompact⟩ :=
60     exists_nonzero_projection_rankOne_map pi hsingle
61   let I : TwoSidedIdeal A :=
62     MathlibAnnex.CStarAlgebra.compactPreimageIdeal pi
63   have hpI : p ∈ I :=
64     (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal pi p).2 hpcompact
65   have hIne : I ≠ ⊥ := by
66     intro hbot
67     have hpzero : p = 0 := by
68       rw [hbot] at hpI
69       simpa using hpI
70     exact hpne hpzero
71   have hItop : I = ⊤ :=
72     (hsimple.2 I
73       (MathlibAnnex.CStarAlgebra.isClosed_compactPreimageIdeal pi)).resolve_left hIne
74   intro a
75   have haI : a ∈ I := by
76     rw [hItop]
77     trivial
78   exact (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal pi a).1 haI
79 
80 /-- Conditional closure of the genuinely non-unital compact-operator model:
81 the only extra input is norm-closed two-sided simplicity of `A`. -/
82 theorem isCompactOperatorModel_of_singleton_of_isSimple [Nontrivial A]
83     [TopologicalSpace.SeparableSpace H]
84     (pi : NonUnitalCStarRepresentation A H)
85     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
86     (hsimple : IsSimpleCStarAlgebra A) :
87     IsCompactOperatorModel pi := by
88   refine ⟨injective_of_singleton pi hsingle,
89     isCompactOperator_map_of_singleton_of_isSimple pi hsingle hsimple, ?_⟩
90   exact exists_preimage_of_compact_singleton pi hsingle
91 
92 /-- Faithfulness and exact compact range, conditionally on the generic
93 non-unital simplicity bridge. -/
94 theorem faithful_and_compactOperatorModel_of_singleton_of_isSimple
95     [Nontrivial A] [TopologicalSpace.SeparableSpace H]
96     (pi : NonUnitalCStarRepresentation A H)
97     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
98     (hsimple : IsSimpleCStarAlgebra A) :
99     Function.Injective pi ∧ IsCompactOperatorModel pi :=
100   ⟨injective_of_singleton pi hsingle,
101     isCompactOperatorModel_of_singleton_of_isSimple pi hsingle hsimple⟩
102 
103 end NonUnitalCStarRepresentation
104 
105 end MathlibAnnex.Analysis.CStarAlgebra