Exact source: MathlibAnnex/Analysis/CStarAlgebra/NonUnital/Representation.lean
Pinned GitHub source · Raw UTF-8 source
Back to A representative of the unique irreducible class · Back to Unitary equivalence of two representations
1import Mathlib.Analysis.CStarAlgebra.Unitization2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Basic34/-!5# Representations of genuinely nonunital C-star algebras67This interface is distinct from `NonUnitalRepresentation`, which has a8unital domain and merely permits a map not known to preserve its unit.9-/1011set_option autoImplicit false1213namespace MathlibAnnex.Analysis.CStarAlgebra1415universe u v w1617variable {A : Type u} [NonUnitalCStarAlgebra A]18variable {H : Type v} {K : Type w}19variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]20variable [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]2122/-- A representation of a possibly genuinely nonunital complex C-star23algebra. -/24abbrev NonUnitalCStarRepresentation (A : Type u)25 [NonUnitalCStarAlgebra A] (H : Type v)26 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] :=27 A →⋆ₙₐ[ℂ] (H →L[ℂ] H)2829namespace NonUnitalCStarRepresentation3031def IsNonzero (pi : NonUnitalCStarRepresentation A H) : Prop :=32 ∃ a : A, pi a ≠ 03334def 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 ∈ L3940def IsIrreducible (pi : NonUnitalCStarRepresentation A H) : Prop :=41 pi.IsNonzero ∧ ∀ L : Submodule ℂ H, pi.Reduces L → L = ⊥ ∨ L = ⊤4243def 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)4647/-- Extend a representation of `A` to the minimal unitization on the same48Hilbert space. -/49noncomputable def unitization (pi : NonUnitalCStarRepresentation A H) :50 Representation (Unitization ℂ A) H :=51 Unitization.starLift pi5253@[simp]54theorem unitization_inr55 (pi : NonUnitalCStarRepresentation A H) (a : A) :56 pi.unitization (Unitization.inr a) = pi a := by57 simp [unitization]5859@[simp]60theorem unitization_inr_apply61 (pi : NonUnitalCStarRepresentation A H) (a : A) (x : H) :62 pi.unitization (Unitization.inr a) x = pi a x := by63 simp [unitization]6465theorem nontrivial_of_isNonzero66 (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsNonzero) :67 Nontrivial H := by68 rw [← not_subsingleton_iff_nontrivial]69 intro hsub70 obtain ⟨a, ha⟩ := hpi71 exact ha (Subsingleton.elim (pi a) 0)7273/-- A subspace reducing a nonunital representation also reduces its74canonical unitization extension. -/75theorem reduces_unitization_of_reduces76 (pi : NonUnitalCStarRepresentation A H) (L : Submodule ℂ H)77 (hL : pi.Reduces L) : pi.unitization.Reduces L := by78 refine ⟨hL.1, ?_⟩79 have hinv : ∀ (z : Unitization ℂ A) (x : H), x ∈ L →80 pi.unitization z x ∈ L := by81 intro z82 induction z using Unitization.ind with83 | inl_add_inr c a =>84 intro x hx85 have hax : pi a x ∈ L := (hL.2 a x hx).186 simpa [unitization] using L.add_mem (L.smul_mem c hx) hax87 intro z x hx88 refine ⟨hinv z x hx, ?_⟩89 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star]90 exact hinv (star z) x hx9192/-- Restriction of an irreducible representation of the unitization is93irreducible whenever its action on the original algebra is nonzero. -/94theorem isIrreducible_restriction_of_isIrreducible_unitization95 (rho : Representation (Unitization ℂ A) H)96 (hirr : rho.IsIrreducible)97 (hnz : IsNonzero98 (rho.toNonUnitalStarAlgHom.comp99 (Unitization.inrNonUnitalStarAlgHom ℂ A))) :100 IsIrreducible101 (rho.toNonUnitalStarAlgHom.comp102 (Unitization.inrNonUnitalStarAlgHom ℂ A)) := by103 let sigma : NonUnitalCStarRepresentation A H :=104 rho.toNonUnitalStarAlgHom.comp105 (Unitization.inrNonUnitalStarAlgHom ℂ A)106 refine ⟨hnz, ?_⟩107 intro L hL108 have heq : sigma.unitization = rho := by109 apply Unitization.starAlgHom_ext110 ext a111 simp [sigma, unitization]112 have hred : rho.Reduces L := by113 rw [← heq]114 exact reduces_unitization_of_reduces sigma L hL115 exact hirr.2 L hred116117/-- The unitization extension of a nonzero irreducible representation is118irreducible. -/119theorem isIrreducible_unitization120 (pi : NonUnitalCStarRepresentation A H) (hirr : pi.IsIrreducible) :121 pi.unitization.IsIrreducible := by122 refine ⟨?_, ?_⟩123 · obtain ⟨a, ha⟩ := hirr.1124 refine ⟨Unitization.inr a, ?_⟩125 intro hzero126 apply ha127 ext x128 have := congrArg (fun T : H →L[ℂ] H => T x) hzero129 simpa using this130 · intro L hL131 apply hirr.2 L132 refine ⟨hL.1, ?_⟩133 intro a x hx134 have hz := hL.2 (Unitization.inr a) x hx135 simpa only [unitization_inr] using hz136137/-- Unitary equivalence is preserved by canonical unitization. -/138theorem unitization_unitaryEquivalent139 {pi : NonUnitalCStarRepresentation A H}140 {rho : NonUnitalCStarRepresentation A K}141 (h : pi.UnitaryEquivalent rho) :142 pi.unitization.UnitaryEquivalent rho.unitization := by143 obtain ⟨U, hU⟩ := h144 refine ⟨U, ?_⟩145 intro z146 induction z using Unitization.ind with147 | inl_add_inr c a =>148 intro x149 simp [unitization, hU]150151end NonUnitalCStarRepresentation152153end MathlibAnnex.Analysis.CStarAlgebra