MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.Representation.surjective_of_irreducible_of_finiteDimensional

Raw UTF-8 source

theorem surjective_of_irreducible_of_finiteDimensional [Nontrivial H]
    [FiniteDimensional ℂ H]
    (pi : Representation A H) (hirr : pi.IsIrreducible) :
    Function.Surjective pi

1 import Mathlib.LinearAlgebra.Complex.Module
2 import MathlibAnnex.Analysis.CStarAlgebra.ExactInterpolation
3 import MathlibAnnex.Analysis.CStarAlgebra.Representation.FiniteDimension
4 
5 /-!
6 # Full operator image in finite dimension
7 -/
8 
9 set_option autoImplicit false
10 
11 open scoped ComplexOrder ComplexStarModule
12 
13 namespace MathlibAnnex.Analysis.CStarAlgebra
14 
15 universe u v
16 
17 variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
18 variable {H : Type v}
19 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
20 
21 namespace Representation
22 
23 /-- Exact interpolation on the whole finite-dimensional Hilbert space gives
24 an algebra preimage of every self-adjoint operator. -/
25 theorem exists_preimage_of_isSelfAdjoint [Nontrivial H]
26     [FiniteDimensional ℂ H]
27     (pi : Representation A H) (hirr : pi.IsIrreducible)
28     (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) :
29     ∃ a : A, pi a = T := by
30   obtain ⟨a, _ha, _hanorm, hexact⟩ :=
31     exists_selfAdjoint_norm_le_two_mul_and_eq_on pi
32       (isIrreducible_starAlgHom pi hirr) (⊤ : Submodule ℂ H) T hT
33   refine ⟨a, ContinuousLinearMap.ext fun x => ?_⟩
34   exact hexact x (by trivial)
35 
36 /-- An irreducible representation on a nonzero finite-dimensional Hilbert
37 space has full operator image. -/
38 theorem surjective_of_irreducible_of_finiteDimensional [Nontrivial H]
39     [FiniteDimensional ℂ H]
40     (pi : Representation A H) (hirr : pi.IsIrreducible) :
41     Function.Surjective pi := by
42   intro T
43   obtain ⟨a, ha⟩ :=
44     exists_preimage_of_isSelfAdjoint pi hirr
45       (ℜ T : H →L[ℂ] H) (ℜ T).prop
46   obtain ⟨b, hb⟩ :=
47     exists_preimage_of_isSelfAdjoint pi hirr
48       (ℑ T : H →L[ℂ] H) (ℑ T).prop
49   refine ⟨a + Complex.I • b, ?_⟩
50   calc
51     pi (a + Complex.I • b) = pi a + Complex.I • pi b := by simp
52     _ = (ℜ T : H →L[ℂ] H) + Complex.I • (ℑ T : H →L[ℂ] H) := by
53       rw [ha, hb]
54     _ = T := realPart_add_I_smul_imaginaryPart T
55 
56 /-- For a separable singleton irreducible model, the represented operators
57 are exactly the compact operators.  In fact the Hilbert space is finite-
58 dimensional and the represented image is all bounded operators. -/
59 theorem isCompactOperatorModel_of_singleton [Nontrivial A]
60     [TopologicalSpace.SeparableSpace H]
61     (pi : Representation A H)
62     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
63     IsCompactOperatorModel pi.toNonUnitalStarAlgHom := by
64   letI : Nontrivial H := nontrivial_of_isNonzero pi hsingle.1.1
65   letI : FiniteDimensional ℂ H :=
66     finiteDimensional_space_of_singleton pi hsingle
67   refine ⟨injective_of_singleton pi hsingle, ?_, ?_⟩
68   · intro a
69     change IsCompactOperator (pi a)
70     exact isCompactOperator_of_locallyCompactSpace_rng (pi a)
71   · intro T _hT
72     exact surjective_of_irreducible_of_finiteDimensional pi hsingle.1 T
73 
74 /-- The faithful/full-compact-image conclusion for a separable singleton
75 irreducible model of a nonzero unital C-star algebra. -/
76 theorem faithful_and_compactOperatorModel_of_singleton [Nontrivial A]
77     [TopologicalSpace.SeparableSpace H]
78     (pi : Representation A H)
79     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
80     Function.Injective pi ∧
81       IsCompactOperatorModel pi.toNonUnitalStarAlgHom :=
82   ⟨injective_of_singleton pi hsingle,
83     isCompactOperatorModel_of_singleton pi hsingle⟩
84 
85 end Representation
86 
87 end MathlibAnnex.Analysis.CStarAlgebra