MathlibAnnex/Analysis/CStarAlgebra/Representation/FiniteDimensionalCompact.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/67import MathlibAnnex.Analysis.CStarAlgebra.Spectrum.CompactRepresentationCharacterization8import MathlibAnnex.LinearAlgebra.FiniteDimensional.FiniteIntersection9import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension1011/-!12# Faithful finite-dimensional representations of finite-dimensional C-star algebras1314The construction uses finitely many of the already selected primitive GNS15representations. Finite-dimensionality of the algebra makes the intersection16of their linear kernels finitely determined. The full reduced atomic action17is faithful, so a finite subfamily still separates algebra elements.1819Every selected pure-state GNS space is finite-dimensional: the original20algebra's orbit of the distinguished GNS vector is the range of an explicit21surjective linear map. The genuine dependent Hilbert `lp 2` sum over the22selected finite set is finite-dimensional as well. Its representation is the23existing atomic representation of the unitization restricted to the original24algebra. The star law therefore comes from genuine Hilbert-space GNS actions,25not an unjustified inner product on a left regular representation.2627No unit, nonzero algebra, nonempty primitive spectrum, or nonempty finite28selection is assumed. All witness structures are supplied in the algebra's29own universe. Compactness is asserted for the constructed finite-dimensional30representation and then for the same canonical reduced atomic representation,31not for every preassigned faithful representation of the algebra.32-/3334@[expose] public section3536set_option autoImplicit false37noncomputable section3839open Set40open scoped Classical CStarAlgebra ENNReal lp4142attribute [local instance] _root_.CStarAlgebra.spectralOrder43  _root_.CStarAlgebra.spectralOrderedRing4445namespace MathlibAnnex.Analysis.CStarAlgebra4647open MathlibAnnex.Analysis.InnerProductSpace4849universe u50variable {A : Type u} [NonUnitalCStarAlgebra A]5152namespace NonUnitalPureState5354/-- The original-algebra orbit of the actual GNS vector is a surjective55linear image of the finite-dimensional algebra. -/56theorem finiteDimensional_gns [FiniteDimensional ℂ A] (phi : NonUnitalPureState A) :57    FiniteDimensional ℂ phi.GNS := by58  let orbit : A →ₗ[ℂ] phi.GNS :=59    { toFun := fun a => phi.gnsRepresentation a phi.gnsVector60      map_add' := by61        intro a b62        simp only [map_add, ContinuousLinearMap.add_apply]63      map_smul' := by64        intro c a65        change phi.gnsRepresentation (c • a) phi.gnsVector =66          c • (phi.gnsRepresentation a phi.gnsVector)67        simp only [map_smul, ContinuousLinearMap.smul_apply] }68  apply FiniteDimensional.of_surjective orbit69  exact NonUnitalStateGNS.representation_vector_surjective_of_isPure70    phi.val phi.property.1 phi.property7172end NonUnitalPureState7374namespace PrimitiveSpectrum7576/-- A finite set of the already selected primitive GNS actions separates77points of a finite-dimensional algebra. Empty selections are allowed. -/78theorem exists_finset_pureStateRepresentative_separates_points [FiniteDimensional ℂ A] :79    ∃ s : Finset (PrimitiveSpectrum A),80      ∀ a b : A,81        (∀ P ∈ s, P.pureStateRepresentative.gnsRepresentation a =82          P.pureStateRepresentative.gnsRepresentation b) → a = b := by83  let kernels : PrimitiveSpectrum A → Submodule ℂ A := fun P =>84    (LinearMapClass.linearMap P.pureStateRepresentative.gnsRepresentation).ker85  obtain ⟨s, hs⟩ := Submodule.exists_finset_iInf_eq_of_finiteDimensional kernels86  refine ⟨s, ?_⟩87  intro a b hab88  have hmem : a - b ∈ (⨅ P, kernels P) := by89    rw [hs]90    apply (Submodule.mem_iInf _).mpr91    intro P92    apply (Submodule.mem_iInf _).mpr93    intro hP94    change P.pureStateRepresentative.gnsRepresentation (a - b) = 095    rw [map_sub, hab P hP, sub_self]96  have hall (P : PrimitiveSpectrum A) :97      P.pureStateRepresentative.gnsRepresentation a =98        P.pureStateRepresentative.gnsRepresentation b := by99    have h := (Submodule.mem_iInf _).mp hmem P100    change P.pureStateRepresentative.gnsRepresentation (a - b) = 0 at h101    exact sub_eq_zero.mp (by simpa only [map_sub] using h)102  apply reducedAtomicRepresentation_injective103  apply ContinuousLinearMap.ext104  intro x105  apply lp.ext106  funext P107  simp only [reducedAtomicRepresentation_apply, hall P]108109/-- The genuine completed dependent Hilbert sum over a given finite selection110of primitive GNS spaces. This carrier is defined before any separation or111finite-dimensionality assumption on the algebra. -/112abbrev FiniteGNSHilbertSpace (A : Type u) [NonUnitalCStarAlgebra A]113    (s : Finset (PrimitiveSpectrum A)) :=114  HilbertSum (fun P : s => P.val.pureStateRepresentative.GNS)115116/-- The selected finite GNS actions, obtained from the existing atomic action117of the unitization and then restricted to the original algebra. -/118def finiteGNSRepresentation (s : Finset (PrimitiveSpectrum A)) :119    NonUnitalCStarRepresentation A (FiniteGNSHilbertSpace A s) :=120  (atomicRepresentation (fun P : s =>121    P.val.pureStateRepresentative.gnsRepresentation.unitization)).toNonUnitalStarAlgHom.comp122    (Unitization.inrNonUnitalStarAlgHom ℂ A)123124@[simp]125theorem finiteGNSRepresentation_apply (s : Finset (PrimitiveSpectrum A))126    (a : A) (x : FiniteGNSHilbertSpace A s) (P : s) :127    finiteGNSRepresentation s a x P =128      P.val.pureStateRepresentative.gnsRepresentation a (x P) := by129  simp [finiteGNSRepresentation, atomicRepresentation_apply,130    NonUnitalCStarRepresentation.unitization_inr]131132/-- Compression to the selected coordinate is precisely the given GNS action. -/133theorem coordinateProjection_comp_finiteGNSRepresentation_comp_coordinateEmbedding134    (s : Finset (PrimitiveSpectrum A)) (a : A) (P : s) :135    (coordinateProjection P).comp136      ((finiteGNSRepresentation s a).comp (coordinateEmbedding P)) =137        P.val.pureStateRepresentative.gnsRepresentation a := by138  apply ContinuousLinearMap.ext139  intro x140  change (finiteGNSRepresentation s a (lp.single 2 P x)) P = _141  rw [finiteGNSRepresentation_apply, lp.coeFn_single, Pi.single_eq_same]142143/-- Joint faithfulness of the chosen GNS actions implies faithfulness of144this very finite-sum representation; no summand is assumed faithful. -/145theorem finiteGNSRepresentation_injective (s : Finset (PrimitiveSpectrum A))146    (hsep : ∀ a b : A,147      (∀ P ∈ s, P.pureStateRepresentative.gnsRepresentation a =148        P.pureStateRepresentative.gnsRepresentation b) → a = b) :149    Function.Injective (finiteGNSRepresentation s) := by150  intro a b hab151  apply hsep a b152  intro P hP153  let Q : s := ⟨P, hP⟩154  have h := congrArg155    (fun T : FiniteGNSHilbertSpace A s →L[ℂ] FiniteGNSHilbertSpace A s =>156      (coordinateProjection Q).comp (T.comp (coordinateEmbedding Q))) hab157  simpa only [coordinateProjection_comp_finiteGNSRepresentation_comp_coordinateEmbedding]158    using h159160/-- Norm preservation is a property of the same concrete finite GNS action. -/161@[simp]162theorem norm_finiteGNSRepresentation (s : Finset (PrimitiveSpectrum A))163    (hsep : ∀ a b : A,164      (∀ P ∈ s, P.pureStateRepresentative.gnsRepresentation a =165        P.pureStateRepresentative.gnsRepresentation b) → a = b) (a : A) :166    ‖finiteGNSRepresentation s a‖ = ‖a‖ :=167  NonUnitalStarAlgHom.norm_map (finiteGNSRepresentation s)168    (finiteGNSRepresentation_injective s hsep) a169170theorem isometry_finiteGNSRepresentation (s : Finset (PrimitiveSpectrum A))171    (hsep : ∀ a b : A,172      (∀ P ∈ s, P.pureStateRepresentative.gnsRepresentation a =173        P.pureStateRepresentative.gnsRepresentation b) → a = b) :174    Isometry (finiteGNSRepresentation s) :=175  NonUnitalStarAlgHom.isometry (finiteGNSRepresentation s)176    (finiteGNSRepresentation_injective s hsep)177178/-- The adjoint identity is inherited from the actual GNS star representations. -/179theorem adjoint_finiteGNSRepresentation (s : Finset (PrimitiveSpectrum A)) (a : A) :180    ContinuousLinearMap.adjoint (finiteGNSRepresentation s a) =181      finiteGNSRepresentation s (star a) := by182  simpa only [ContinuousLinearMap.star_eq_adjoint] using183    (map_star (finiteGNSRepresentation s) a).symm184185/-- A finite dependent Hilbert sum of the finite-dimensional GNS fibers is186finite-dimensional. Injecting into the ordinary finite product is sufficient;187no equality between the product norm and the Hilbert norm is asserted. -/188theorem finiteDimensional_finiteGNSHilbertSpace [FiniteDimensional ℂ A]189    (s : Finset (PrimitiveSpectrum A)) :190    FiniteDimensional ℂ (FiniteGNSHilbertSpace A s) := by191  letI : ∀ P : s, FiniteDimensional ℂ P.val.pureStateRepresentative.GNS :=192    fun P => P.val.pureStateRepresentative.finiteDimensional_gns193  let coordinates : FiniteGNSHilbertSpace A s →ₗ[ℂ]194      (∀ P : s, P.val.pureStateRepresentative.GNS) :=195    { toFun := fun x P => x P196      map_add' := by intros; rfl197      map_smul' := by intros; rfl }198  apply FiniteDimensional.of_injective coordinates199  intro x y hxy200  apply lp.ext201  exact hxy202203/-- All values of the selected finite GNS action are compact because its204actual Hilbert space, not merely the source algebra, is finite-dimensional. -/205theorem isCompactOperator_finiteGNSRepresentation [FiniteDimensional ℂ A]206    (s : Finset (PrimitiveSpectrum A)) (a : A) :207    IsCompactOperator (finiteGNSRepresentation s a) := by208  letI : FiniteDimensional ℂ (FiniteGNSHilbertSpace A s) :=209    finiteDimensional_finiteGNSHilbertSpace s210  have hid : IsCompactOperator (id : FiniteGNSHilbertSpace A s →211      FiniteGNSHilbertSpace A s) :=212    (isCompactOperator_id_iff_finiteDimensional (𝕜 := ℂ)).mpr inferInstance213  exact hid.comp_clm (finiteGNSRepresentation s a)214215/-- A finite separating selection yields an actual faithful compact action. -/216theorem isCompactlyRepresented_finiteGNSRepresentation [FiniteDimensional ℂ A]217    (s : Finset (PrimitiveSpectrum A))218    (hsep : ∀ a b : A,219      (∀ P ∈ s, P.pureStateRepresentative.gnsRepresentation a =220        P.pureStateRepresentative.gnsRepresentation b) → a = b) :221    (finiteGNSRepresentation s).IsCompactlyRepresented :=222  ⟨finiteGNSRepresentation_injective s hsep,223    isCompactOperator_finiteGNSRepresentation s⟩224225/-- The separating set is proved to exist, rather than supplied as a boundary226hypothesis of the finite-dimensional existence theorem. -/227theorem exists_finset_isCompactlyRepresented_finiteGNSRepresentation228    [FiniteDimensional ℂ A] :229    ∃ s : Finset (PrimitiveSpectrum A),230      (finiteGNSRepresentation s).IsCompactlyRepresented := by231  obtain ⟨s, hs⟩ := exists_finset_pureStateRepresentative_separates_points (A := A)232  exact ⟨s, isCompactlyRepresented_finiteGNSRepresentation s hs⟩233234/-- Finite-dimensionality alone makes the same canonical reduced atomic map235faithfully compact. The supplied intermediate witness is the finite GNS sum,236not an arbitrary preassigned faithful representation. -/237theorem isCompactlyRepresented_reducedAtomicRepresentation_of_finiteDimensional238    [FiniteDimensional ℂ A] :239    (reducedAtomicRepresentation (A := A)).IsCompactlyRepresented := by240  obtain ⟨s, hs⟩ := exists_finset_isCompactlyRepresented_finiteGNSRepresentation (A := A)241  exact isCompactlyRepresented_reducedAtomicRepresentation_of_isCompactlyRepresented242    (finiteGNSRepresentation s) hs243244end PrimitiveSpectrum245246namespace NonUnitalCStarRepresentation247248/-- A finite-dimensional C-star algebra has a faithful compact-valued249representation on an explicitly supplied finite-dimensional Hilbert space in250its own universe. The normed, inner-product and completeness structures are251all supplied by the genuine finite dependent GNS Hilbert sum. -/252theorem exists_finiteDimensional_isCompactlyRepresented [FiniteDimensional ℂ A] :253    ∃ (K : Type u) (normed : NormedAddCommGroup K),254      letI : NormedAddCommGroup K := normed255      ∃ inner : InnerProductSpace ℂ K,256        letI : InnerProductSpace ℂ K := inner257        ∃ complete : CompleteSpace K,258          letI : CompleteSpace K := complete259          FiniteDimensional ℂ K ∧260            ∃ pi : NonUnitalCStarRepresentation A K, pi.IsCompactlyRepresented := by261  obtain ⟨s, hs⟩ :=262    PrimitiveSpectrum.exists_finset_isCompactlyRepresented_finiteGNSRepresentation (A := A)263  refine ⟨PrimitiveSpectrum.FiniteGNSHilbertSpace A s, inferInstance, ?_⟩264  refine ⟨inferInstance, ?_⟩265  exact ⟨inferInstance, PrimitiveSpectrum.finiteDimensional_finiteGNSHilbertSpace s,266    PrimitiveSpectrum.finiteGNSRepresentation s, hs⟩267268end NonUnitalCStarRepresentation269270end MathlibAnnex.Analysis.CStarAlgebra271272end