MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.UnitaryEquivalent

Raw UTF-8 source

def UnitaryEquivalent (pi : NonUnitalCStarRepresentation A H)
    (rho : NonUnitalCStarRepresentation A K) : Prop

1 import Mathlib.Analysis.CStarAlgebra.Unitization
2 import MathlibAnnex.Analysis.CStarAlgebra.Representation.Basic
3 
4 /-!
5 # Representations of genuinely nonunital C-star algebras
6 
7 This interface is distinct from `NonUnitalRepresentation`, which has a
8 unital domain and merely permits a map not known to preserve its unit.
9 -/
10 
11 set_option autoImplicit false
12 
13 namespace MathlibAnnex.Analysis.CStarAlgebra
14 
15 universe u v w
16 
17 variable {A : Type u} [NonUnitalCStarAlgebra A]
18 variable {H : Type v} {K : Type w}
19 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
20 variable [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
21 
22 /-- A representation of a possibly genuinely nonunital complex C-star
23 algebra. -/
24 abbrev NonUnitalCStarRepresentation (A : Type u)
25     [NonUnitalCStarAlgebra A] (H : Type v)
26     [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] :=
27   A →⋆ₙₐ[ℂ] (H →L[ℂ] H)
28 
29 namespace NonUnitalCStarRepresentation
30 
31 def IsNonzero (pi : NonUnitalCStarRepresentation A H) : Prop :=
32   ∃ a : A, pi a ≠ 0
33 
34 def Reduces (pi : NonUnitalCStarRepresentation A H)
35     (L : Submodule ℂ H) : Prop :=
36   IsClosed (L : Set H) ∧
37     ∀ (a : A) (x : H), x ∈ L →
38       pi a x ∈ L ∧ ContinuousLinearMap.adjoint (pi a) x ∈ L
39 
40 def IsIrreducible (pi : NonUnitalCStarRepresentation A H) : Prop :=
41   pi.IsNonzero ∧ ∀ L : Submodule ℂ H, pi.Reduces L → L = ⊥ ∨ L = ⊤
42 
43 def UnitaryEquivalent (pi : NonUnitalCStarRepresentation A H)
44     (rho : NonUnitalCStarRepresentation A K) : Prop :=
45   ∃ U : H ≃ₗᵢ[ℂ] K, ∀ (a : A) (x : H), U (pi a x) = rho a (U x)
46 
47 /-- Extend a representation of `A` to the minimal unitization on the same
48 Hilbert space. -/
49 noncomputable def unitization (pi : NonUnitalCStarRepresentation A H) :
50     Representation (Unitization ℂ A) H :=
51   Unitization.starLift pi
52 
53 @[simp]
54 theorem unitization_inr
55     (pi : NonUnitalCStarRepresentation A H) (a : A) :
56     pi.unitization (Unitization.inr a) = pi a := by
57   simp [unitization]
58 
59 @[simp]
60 theorem unitization_inr_apply
61     (pi : NonUnitalCStarRepresentation A H) (a : A) (x : H) :
62     pi.unitization (Unitization.inr a) x = pi a x := by
63   simp [unitization]
64 
65 theorem nontrivial_of_isNonzero
66     (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsNonzero) :
67     Nontrivial H := by
68   rw [← not_subsingleton_iff_nontrivial]
69   intro hsub
70   obtain ⟨a, ha⟩ := hpi
71   exact ha (Subsingleton.elim (pi a) 0)
72 
73 /-- A subspace reducing a nonunital representation also reduces its
74 canonical unitization extension. -/
75 theorem reduces_unitization_of_reduces
76     (pi : NonUnitalCStarRepresentation A H) (L : Submodule ℂ H)
77     (hL : pi.Reduces L) : pi.unitization.Reduces L := by
78   refine ⟨hL.1, ?_⟩
79   have hinv : ∀ (z : Unitization ℂ A) (x : H), x ∈ L →
80       pi.unitization z x ∈ L := by
81     intro z
82     induction z using Unitization.ind with
83     | inl_add_inr c a =>
84         intro x hx
85         have hax : pi a x ∈ L := (hL.2 a x hx).1
86         simpa [unitization] using L.add_mem (L.smul_mem c hx) hax
87   intro z x hx
88   refine ⟨hinv z x hx, ?_⟩
89   rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star]
90   exact hinv (star z) x hx
91 
92 /-- Restriction of an irreducible representation of the unitization is
93 irreducible whenever its action on the original algebra is nonzero. -/
94 theorem isIrreducible_restriction_of_isIrreducible_unitization
95     (rho : Representation (Unitization ℂ A) H)
96     (hirr : rho.IsIrreducible)
97     (hnz : IsNonzero
98       (rho.toNonUnitalStarAlgHom.comp
99         (Unitization.inrNonUnitalStarAlgHom ℂ A))) :
100     IsIrreducible
101       (rho.toNonUnitalStarAlgHom.comp
102         (Unitization.inrNonUnitalStarAlgHom ℂ A)) := by
103   let sigma : NonUnitalCStarRepresentation A H :=
104     rho.toNonUnitalStarAlgHom.comp
105       (Unitization.inrNonUnitalStarAlgHom ℂ A)
106   refine ⟨hnz, ?_⟩
107   intro L hL
108   have heq : sigma.unitization = rho := by
109     apply Unitization.starAlgHom_ext
110     ext a
111     simp [sigma, unitization]
112   have hred : rho.Reduces L := by
113     rw [← heq]
114     exact reduces_unitization_of_reduces sigma L hL
115   exact hirr.2 L hred
116 
117 /-- The unitization extension of a nonzero irreducible representation is
118 irreducible. -/
119 theorem isIrreducible_unitization
120     (pi : NonUnitalCStarRepresentation A H) (hirr : pi.IsIrreducible) :
121     pi.unitization.IsIrreducible := by
122   refine ⟨?_, ?_⟩
123   · obtain ⟨a, ha⟩ := hirr.1
124     refine ⟨Unitization.inr a, ?_⟩
125     intro hzero
126     apply ha
127     ext x
128     have := congrArg (fun T : H →L[ℂ] H => T x) hzero
129     simpa using this
130   · intro L hL
131     apply hirr.2 L
132     refine ⟨hL.1, ?_⟩
133     intro a x hx
134     have hz := hL.2 (Unitization.inr a) x hx
135     simpa only [unitization_inr] using hz
136 
137 /-- Unitary equivalence is preserved by canonical unitization. -/
138 theorem unitization_unitaryEquivalent
139     {pi : NonUnitalCStarRepresentation A H}
140     {rho : NonUnitalCStarRepresentation A K}
141     (h : pi.UnitaryEquivalent rho) :
142     pi.unitization.UnitaryEquivalent rho.unitization := by
143   obtain ⟨U, hU⟩ := h
144   refine ⟨U, ?_⟩
145   intro z
146   induction z using Unitization.ind with
147   | inl_add_inr c a =>
148       intro x
149       simp [unitization, hU]
150 
151 end NonUnitalCStarRepresentation
152 
153 end MathlibAnnex.Analysis.CStarAlgebra