Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/FullImage.lean
Pinned GitHub source · Raw UTF-8 source
Back to Compact-operator conclusion for the unital singleton condition · Back to Full operator image in finite dimension
1import Mathlib.LinearAlgebra.Complex.Module2import MathlibAnnex.Analysis.CStarAlgebra.ExactInterpolation3import MathlibAnnex.Analysis.CStarAlgebra.Representation.FiniteDimension45/-!6# Full operator image in finite dimension7-/89set_option autoImplicit false1011open scoped ComplexOrder ComplexStarModule1213namespace MathlibAnnex.Analysis.CStarAlgebra1415universe u v1617variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]18variable {H : Type v}19variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2021namespace Representation2223/-- Exact interpolation on the whole finite-dimensional Hilbert space gives24an algebra preimage of every self-adjoint operator. -/25theorem 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 := by30 obtain ⟨a, _ha, _hanorm, hexact⟩ :=31 exists_selfAdjoint_norm_le_two_mul_and_eq_on pi32 (isIrreducible_starAlgHom pi hirr) (⊤ : Submodule ℂ H) T hT33 refine ⟨a, ContinuousLinearMap.ext fun x => ?_⟩34 exact hexact x (by trivial)3536/-- An irreducible representation on a nonzero finite-dimensional Hilbert37space has full operator image. -/38theorem surjective_of_irreducible_of_finiteDimensional [Nontrivial H]39 [FiniteDimensional ℂ H]40 (pi : Representation A H) (hirr : pi.IsIrreducible) :41 Function.Surjective pi := by42 intro T43 obtain ⟨a, ha⟩ :=44 exists_preimage_of_isSelfAdjoint pi hirr45 (ℜ T : H →L[ℂ] H) (ℜ T).prop46 obtain ⟨b, hb⟩ :=47 exists_preimage_of_isSelfAdjoint pi hirr48 (ℑ T : H →L[ℂ] H) (ℑ T).prop49 refine ⟨a + Complex.I • b, ?_⟩50 calc51 pi (a + Complex.I • b) = pi a + Complex.I • pi b := by simp52 _ = (ℜ T : H →L[ℂ] H) + Complex.I • (ℑ T : H →L[ℂ] H) := by53 rw [ha, hb]54 _ = T := realPart_add_I_smul_imaginaryPart T5556/-- For a separable singleton irreducible model, the represented operators57are exactly the compact operators. In fact the Hilbert space is finite-58dimensional and the represented image is all bounded operators. -/59theorem 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 := by64 letI : Nontrivial H := nontrivial_of_isNonzero pi hsingle.1.165 letI : FiniteDimensional ℂ H :=66 finiteDimensional_space_of_singleton pi hsingle67 refine ⟨injective_of_singleton pi hsingle, ?_, ?_⟩68 · intro a69 change IsCompactOperator (pi a)70 exact isCompactOperator_of_locallyCompactSpace_rng (pi a)71 · intro T _hT72 exact surjective_of_irreducible_of_finiteDimensional pi hsingle.1 T7374/-- The faithful/full-compact-image conclusion for a separable singleton75irreducible model of a nonzero unital C-star algebra. -/76theorem 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⟩8485end Representation8687end MathlibAnnex.Analysis.CStarAlgebra