MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_space_of_singleton

Raw UTF-8 source

theorem finiteDimensional_space_of_singleton [Nontrivial A]
    [TopologicalSpace.SeparableSpace H]
    (pi : Representation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    FiniteDimensional ℂ H

1 import MathlibAnnex.Analysis.CStarAlgebra.CompactPreimage
2 import MathlibAnnex.Analysis.CStarAlgebra.Representation.Faithful
3 import MathlibAnnex.Analysis.CStarAlgebra.Representation.RankOneProjection
4 
5 /-!
6 # Finite dimension forced by a separable singleton irreducible model
7 -/
8 
9 set_option autoImplicit false
10 
11 open Set
12 open scoped ComplexOrder
13 
14 namespace MathlibAnnex.Analysis.CStarAlgebra
15 
16 universe u v
17 
18 variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
19 variable {H : Type v}
20 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
21 
22 namespace Representation
23 
24 /-- The Hilbert space of a separable singleton irreducible model of a
25 nonzero unital C-star algebra is finite-dimensional. -/
26 theorem finiteDimensional_space_of_singleton [Nontrivial A]
27     [TopologicalSpace.SeparableSpace H]
28     (pi : Representation A H)
29     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
30     FiniteDimensional ℂ H := by
31   have hinj : Function.Injective pi := injective_of_singleton pi hsingle
32   have hsimple : IsSimpleCStarAlgebra A :=
33     isSimpleCStarAlgebra_of_singleton_of_injective pi hsingle hinj
34   obtain ⟨p, hp, hpne, hcorner⟩ :=
35     exists_nonzero_projection_scalar_corner pi hsingle
36   have hpmap : pi p ≠ 0 := by
37     intro hzero
38     apply hpne
39     apply hinj
40     simpa using hzero
41   have hpcompact : IsCompactOperator (pi p) :=
42     isCompactOperator_map_of_scalar_corner pi hsingle.1 hp hpmap hcorner
43   let piNU : A →⋆ₙₐ H →L[ℂ] H := pi.toNonUnitalStarAlgHom
44   let I : TwoSidedIdeal A := MathlibAnnex.CStarAlgebra.compactPreimageIdeal piNU
45   have hpI : p ∈ I :=
46     (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal piNU p).2 hpcompact
47   have hIne : I ≠ ⊥ := by
48     intro hbot
49     have hpzero : p = 0 := by
50       rw [hbot] at hpI
51       simpa using hpI
52     exact hpne hpzero
53   have hItop : I = ⊤ :=
54     (hsimple.2 I
55       (MathlibAnnex.CStarAlgebra.isClosed_compactPreimageIdeal piNU)).resolve_left hIne
56   have honeI : (1 : A) ∈ I := by
57     rw [hItop]
58     trivial
59   have honeCompact : IsCompactOperator (pi (1 : A)) :=
60     (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal piNU 1).1 honeI
61   have hcompactOne :
62       IsCompactOperator ((1 : H →L[ℂ] H) : H → H) := by
63     simpa only [map_one, one_apply_eq_self] using honeCompact
64   apply FiniteDimensional.of_isCompactOperator_id
65   change IsCompactOperator (fun x : H => x)
66   exact hcompactOne
67 
68 /-- The algebra itself is finite-dimensional once its singleton model is
69 faithful and its separable representation space is finite-dimensional. -/
70 theorem finiteDimensional_algebra_of_singleton [Nontrivial A]
71     [TopologicalSpace.SeparableSpace H]
72     (pi : Representation A H)
73     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
74     FiniteDimensional ℂ A := by
75   letI : FiniteDimensional ℂ H :=
76     finiteDimensional_space_of_singleton pi hsingle
77   letI : FiniteDimensional ℂ (H →L[ℂ] H) :=
78     ContinuousLinearMap.finiteDimensional
79   exact FiniteDimensional.of_injective
80     (LinearMapClass.linearMap pi) (injective_of_singleton pi hsingle)
81 
82 end Representation
83 
84 end MathlibAnnex.Analysis.CStarAlgebra