MathlibAnnex/Analysis/CStarAlgebra/Representation/ReducedAtomic.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.DirectSum.DiscreteCCR8import MathlibAnnex.Analysis.CStarAlgebra.Representation.CompactOperatorDiagonal910/-!11# The reduced atomic representation on the genuine Hilbert direct sum1213For a nonunital complex C-star algebra, choose the existing pure-state GNS14representative at every primitive point and form their completed dependent15Hilbert `lp 2` sum.  The corresponding atomic action is faithful because the16intersection of all primitive kernels is zero.  No countability or separability17assumption is imposed.1819Under discreteness of the primitive spectrum and the stated CCR range equality,20the repaired coordinate equivalence identifies the algebra with the actual c₀21sum of compact primitive fibres.  The c₀ diagonal representation on the Hilbert22sum is then literally the reduced atomic representation.  Consequently its23image consists of compact operators, and its literal operator range agrees with24the c₀ diagonal range, equivalently with the compact intersection of the25bounded primitive block-diagonal range.  The bounded product `lp _ ∞`, the c₀26source algebra, and the Hilbert representation space `lp _ 2` remain distinct27objects.28-/2930@[expose] public section3132set_option autoImplicit false33set_option maxHeartbeats 200000034set_option synthInstance.maxHeartbeats 20000035noncomputable section3637open Filter Set Topology38open scoped BigOperators CStarAlgebra ENNReal lp3940namespace MathlibAnnex.Analysis.CStarAlgebra4142open MathlibAnnex.Analysis.InnerProductSpace4344universe u4546namespace PrimitiveSpectrum4748variable {A : Type u} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]4950/-- The completed dependent Hilbert `lp 2` sum of the selected primitive GNS51spaces.  This is not the bounded product of compact-operator fibres. -/52abbrev ReducedAtomicHilbertSpace (A : Type u) [NonUnitalCStarAlgebra A]53    [PartialOrder A] [StarOrderedRing A] :=54  HilbertSum (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS)5556/-- The selected primitive GNS representations acting diagonally on their57genuine completed Hilbert sum. -/58def reducedAtomicRepresentation :59    NonUnitalCStarRepresentation A (ReducedAtomicHilbertSpace A) :=60  (atomicRepresentation (fun P : PrimitiveSpectrum A =>61    P.pureStateRepresentative.gnsRepresentation.unitization)).toNonUnitalStarAlgHom.comp62    (Unitization.inrNonUnitalStarAlgHom ℂ A)6364@[simp]65theorem reducedAtomicRepresentation_apply66    (a : A) (x : ReducedAtomicHilbertSpace A) (P : PrimitiveSpectrum A) :67    reducedAtomicRepresentation a x P =68      P.pureStateRepresentative.gnsRepresentation a (x P) := by69  simp [reducedAtomicRepresentation, atomicRepresentation_apply, NonUnitalCStarRepresentation.unitization_inr]7071/-- On one displayed primitive coordinate, the reduced atomic action is exactly72the selected GNS action. -/73@[simp]74theorem reducedAtomicRepresentation_coordinateEmbedding75    [DecidableEq (PrimitiveSpectrum A)] (a : A) (P : PrimitiveSpectrum A)76    (x : P.pureStateRepresentative.GNS) :77    reducedAtomicRepresentation a (coordinateEmbedding P x) =78      coordinateEmbedding P79        (P.pureStateRepresentative.gnsRepresentation a x) := by80  classical81  apply lp.ext82  funext Q83  by_cases hQP : Q = P84  · subst Q85    simp [reducedAtomicRepresentation_apply, coordinateEmbedding_apply,86      lp.coeFn_single]87  · simp [reducedAtomicRepresentation_apply, coordinateEmbedding_apply,88      lp.coeFn_single, hQP, Ne.symm hQP]8990/-- Projection to one primitive coordinate commutes with the reduced atomic91action. -/92@[simp]93theorem coordinateProjection_reducedAtomicRepresentation94    [DecidableEq (PrimitiveSpectrum A)] (a : A) (x : ReducedAtomicHilbertSpace A) (P : PrimitiveSpectrum A) :95    coordinateProjection P (reducedAtomicRepresentation a x) =96      P.pureStateRepresentative.gnsRepresentation a97        (coordinateProjection P x) := by98  classical99  simp [coordinateProjection_apply, reducedAtomicRepresentation_apply]100101/-- The reduced atomic representation is faithful: an element killed on every102selected primitive GNS space belongs to the intersection of all primitive103ideals, hence is zero. -/104theorem reducedAtomicRepresentation_injective :105    Function.Injective (reducedAtomicRepresentation (A := A)) := by106  classical107  intro a b hab108  apply sub_eq_zero.mp109  have hzero : reducedAtomicRepresentation (A := A) (a - b) = 0 := by110    rw [map_sub, hab, sub_self]111  have hall : a - b ∈ kernelIntersection112      (Set.univ : Set (PrimitiveSpectrum A)) := by113    rw [mem_kernelIntersection]114    intro P _hP115    rw [← P.coe_toTwoSidedIdeal]116    rw [← P.kernelIdeal_pureStateRepresentative]117    apply (NonUnitalCStarRepresentation.mem_kernelIdeal118      P.pureStateRepresentative.gnsRepresentation (a - b)).2119    apply ContinuousLinearMap.ext120    intro x121    have h := congrArg122      (fun T : ReducedAtomicHilbertSpace A →L[ℂ] ReducedAtomicHilbertSpace A =>123        coordinateProjection P (T (coordinateEmbedding P x))) hzero124    simpa [coordinateProjection_reducedAtomicRepresentation,125      coordinateEmbedding_apply, coordinateProjection_apply, lp.coeFn_single] using h126  rw [kernelIntersection_univ_eq_bot, TwoSidedIdeal.mem_bot] at hall127  exact hall128129/-- Faithfulness upgrades the reduced atomic representation to an isometry. -/130theorem isometry_reducedAtomicRepresentation :131    Isometry (reducedAtomicRepresentation (A := A)) :=132  NonUnitalStarAlgHom.isometry (reducedAtomicRepresentation (A := A))133    reducedAtomicRepresentation_injective134135@[simp]136theorem norm_reducedAtomicRepresentation (a : A) :137    ‖reducedAtomicRepresentation (A := A) a‖ = ‖a‖ := by138  simpa only [map_zero, dist_zero_right] using139    (isometry_reducedAtomicRepresentation (A := A)).dist_eq a 0140141/-- Restriction of the faithful reduced atomic representation to its literal142operator range is onto. -/143theorem reducedAtomicRepresentation_rangeRestrict_surjective :144    Function.Surjective145      (NonUnitalStarAlgHom.rangeRestrict (reducedAtomicRepresentation (A := A))) := by146  intro T147  obtain ⟨a, ha⟩ := (NonUnitalStarAlgHom.mem_range148    (reducedAtomicRepresentation (A := A))).1 T.property149  exact ⟨a, Subtype.ext ha⟩150151/-- The literal range restriction is bijective. -/152theorem reducedAtomicRepresentation_rangeRestrict_bijective :153    Function.Bijective154      (NonUnitalStarAlgHom.rangeRestrict (reducedAtomicRepresentation (A := A))) := by155  constructor156  · intro a b hab157    apply reducedAtomicRepresentation_injective158    exact congrArg Subtype.val hab159  · exact reducedAtomicRepresentation_rangeRestrict_surjective160161/-- Actual nonunital C-star equivalence from `A` to the literal reduced atomic162operator range. -/163def reducedAtomicEquivRange :164    A ≃⋆ₐ[ℂ] (NonUnitalStarAlgHom.range (reducedAtomicRepresentation (A := A))) :=165  { Equiv.ofBijective (NonUnitalStarAlgHom.rangeRestrict (reducedAtomicRepresentation (A := A)))166      reducedAtomicRepresentation_rangeRestrict_bijective with167    map_add' := map_add (NonUnitalStarAlgHom.rangeRestrict (reducedAtomicRepresentation (A := A)))168    map_mul' := map_mul (NonUnitalStarAlgHom.rangeRestrict (reducedAtomicRepresentation (A := A)))169    map_smul' := map_smul (NonUnitalStarAlgHom.rangeRestrict (reducedAtomicRepresentation (A := A)))170    map_star' := map_star (NonUnitalStarAlgHom.rangeRestrict (reducedAtomicRepresentation (A := A))) }171172@[simp]173theorem reducedAtomicEquivRange_apply_coe (a : A) :174    ((reducedAtomicEquivRange (A := A) a :175      (NonUnitalStarAlgHom.range (reducedAtomicRepresentation (A := A)))) :176        ReducedAtomicHilbertSpace A →L[ℂ] ReducedAtomicHilbertSpace A) =177      reducedAtomicRepresentation a := rfl178179/-- The abstract bounded-product coordinate map acts on the Hilbert `lp 2` sum180as the reduced atomic representation.  This theorem connects the two different181`lp` constructions without identifying their types. -/182theorem boundedProduct_diagonalRepresentation_coordinateMap183    (hCCR : ∀ P : PrimitiveSpectrum A,184      (NonUnitalStarAlgHom.range P.pureStateRepresentative.gnsRepresentation) =185        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ186          P.pureStateRepresentative.GNS)187    (a : A) :188    CompactOperatorBoundedProduct.diagonalRepresentation189        (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS)190        (coordinateMap hCCR a) =191      reducedAtomicRepresentation a := by192  apply ContinuousLinearMap.ext193  intro x194  apply lp.ext195  funext P196  simp only [CompactOperatorBoundedProduct.diagonalRepresentation_apply,197    coordinateMap_apply_coe, reducedAtomicRepresentation_apply]198199/-- After the repaired range theorem and `coordinateC0Equiv`, the c₀ diagonal200representation is literally the reduced atomic representation. -/201theorem c0_diagonalRepresentation_coordinateC0Equiv202    [DiscreteTopology (PrimitiveSpectrum A)]203    (hCCR : ∀ P : PrimitiveSpectrum A,204      (NonUnitalStarAlgHom.range P.pureStateRepresentative.gnsRepresentation) =205        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ206          P.pureStateRepresentative.GNS)207    (a : A) :208    CompactOperatorC0Sum.diagonalRepresentation209        (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS)210        (coordinateC0Equiv hCCR a) =211      reducedAtomicRepresentation a := by212  apply ContinuousLinearMap.ext213  intro x214  apply lp.ext215  funext P216  simp only [CompactOperatorC0Sum.diagonalRepresentation_apply,217    eval_coordinateC0Equiv_apply_coe, reducedAtomicRepresentation_apply]218219section RangeC0Proof220221private abbrev reducedAtomicC0NonUnitalCStarAlgebra : NonUnitalCStarAlgebra (CompactC0Sum A) :=222  C0DirectSum.nonUnitalCStarAlgebra _223224attribute [local instance] reducedAtomicC0NonUnitalCStarAlgebra225226private abbrev reducedAtomicC0NormedAddCommGroup : NormedAddCommGroup (CompactC0Sum A) :=227  @NonUnitalNormedRing.toNormedAddCommGroup _228    reducedAtomicC0NonUnitalCStarAlgebra.toNonUnitalNormedRing229230attribute [local instance] reducedAtomicC0NormedAddCommGroup231232private abbrev reducedAtomicC0SeminormedAddGroup : SeminormedAddGroup (CompactC0Sum A) :=233  @NormedAddGroup.toSeminormedAddGroup _234    (@NormedAddCommGroup.toNormedAddGroup _ reducedAtomicC0NormedAddCommGroup)235236attribute [local instance] reducedAtomicC0SeminormedAddGroup237238private abbrev reducedAtomicC0Ring : NonUnitalRing (CompactC0Sum A) :=239  reducedAtomicC0NonUnitalCStarAlgebra.toNonUnitalNormedRing.toNonUnitalRing240241private abbrev reducedAtomicC0NonAssocSemiring : NonUnitalNonAssocSemiring (CompactC0Sum A) :=242  reducedAtomicC0Ring.toNonUnitalNonAssocRing.toNonUnitalNonAssocSemiring243244attribute [local instance] reducedAtomicC0Ring reducedAtomicC0NonAssocSemiring245246private abbrev reducedAtomicC0AddCommMonoid : AddCommMonoid (CompactC0Sum A) :=247  reducedAtomicC0NonAssocSemiring.toAddCommMonoid248249attribute [local instance] reducedAtomicC0AddCommMonoid250251private abbrev reducedAtomicC0AddMonoid : AddMonoid (CompactC0Sum A) :=252  reducedAtomicC0AddCommMonoid.toAddMonoid253254attribute [local instance] reducedAtomicC0AddMonoid255256private abbrev reducedAtomicC0Module : Module ℂ (CompactC0Sum A) :=257  reducedAtomicC0NonUnitalCStarAlgebra.toNormedSpace.toModule258259attribute [local instance] reducedAtomicC0Module260261private abbrev reducedAtomicC0DistribMulAction : DistribMulAction ℂ (CompactC0Sum A) :=262  reducedAtomicC0NonUnitalCStarAlgebra.toNormedSpace.toModule.toDistribMulAction263264private abbrev reducedAtomicC0AddZeroClass : AddZeroClass (CompactC0Sum A) :=265  reducedAtomicC0NonAssocSemiring.toAddCommMonoid.toAddMonoid.toAddZeroClass266267attribute [local instance] reducedAtomicC0DistribMulAction reducedAtomicC0AddZeroClass268269private abbrev reducedAtomicC0Zero : Zero (CompactC0Sum A) :=270  reducedAtomicC0AddZeroClass.toZero271272attribute [local instance] reducedAtomicC0Zero273274private abbrev reducedAtomicC0Add : Add (CompactC0Sum A) :=275  reducedAtomicC0AddZeroClass.toAddZero.toAdd276277private abbrev reducedAtomicC0Mul : Mul (CompactC0Sum A) :=278  reducedAtomicC0NonAssocSemiring.toMulZeroClass.toMul279280attribute [local instance] reducedAtomicC0Add reducedAtomicC0Mul281282set_option maxHeartbeats 8000000 in283/-- The literal Hilbert-operator range of the reduced atomic representation is284exactly the literal range of the compact c₀ diagonal representation. -/285theorem reducedAtomicRepresentation_range_eq_c0_diagonalRepresentation_range286    [DiscreteTopology (PrimitiveSpectrum A)]287    (hCCR : ∀ P : PrimitiveSpectrum A,288      (NonUnitalStarAlgHom.range P.pureStateRepresentative.gnsRepresentation) =289        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ290          P.pureStateRepresentative.GNS) :291    (NonUnitalStarAlgHom.range (reducedAtomicRepresentation (A := A))) =292      (NonUnitalStarAlgHom.range (CompactOperatorC0Sum.diagonalRepresentation293        (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS))) := by294  apply SetLike.coe_injective295  change Set.range (reducedAtomicRepresentation (A := A)) =296    Set.range (CompactOperatorC0Sum.diagonalRepresentation297      (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS))298  let c : A → CompactC0Sum A := coordinateC0Equiv hCCR299  let d : CompactC0Sum A →300      (ReducedAtomicHilbertSpace A →L[ℂ] ReducedAtomicHilbertSpace A) :=301    CompactOperatorC0Sum.diagonalRepresentation302      (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS)303  have hc : Function.Surjective c := EquivLike.surjective (coordinateC0Equiv hCCR)304  have hd : d ∘ c = (reducedAtomicRepresentation (A := A)) := by305    funext a306    dsimp only [Function.comp_apply, c, d]307    exact c0_diagonalRepresentation_coordinateC0Equiv hCCR a308  change Set.range (reducedAtomicRepresentation (A := A)) = Set.range d309  rw [← hd]310  exact hc.range_comp d311312set_option maxHeartbeats 8000000 in313/-- Under discreteness and the selected CCR range equalities, the reduced314atomic operator range is exactly the compact part of the bounded primitive315block-diagonal range.  This remains a block-diagonal range statement and does316not assert surjectivity onto all compact operators on the Hilbert sum. -/317theorem reducedAtomicRepresentation_range_eq_bounded_diagonalRepresentation_range_inf_compactOperatorStarSubalgebra318    [DiscreteTopology (PrimitiveSpectrum A)]319    (hCCR : ∀ P : PrimitiveSpectrum A,320      (NonUnitalStarAlgHom.range P.pureStateRepresentative.gnsRepresentation) =321        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ322          P.pureStateRepresentative.GNS) :323    (NonUnitalStarAlgHom.range (reducedAtomicRepresentation (A := A))) =324      (NonUnitalStarAlgHom.range (CompactOperatorBoundedProduct.diagonalRepresentation325        (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS))) ⊓326        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ327          (ReducedAtomicHilbertSpace A) := by328  exact (reducedAtomicRepresentation_range_eq_c0_diagonalRepresentation_range hCCR).trans329    (CompactOperatorBoundedProduct.diagonalRepresentation_range_inf_compactOperatorStarSubalgebra330      (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS)).symm331332end RangeC0Proof333334/-- Under discreteness and the selected CCR range equalities, every reduced335atomic image operator is compact. -/336theorem isCompactOperator_reducedAtomicRepresentation337    [DiscreteTopology (PrimitiveSpectrum A)]338    (hCCR : ∀ P : PrimitiveSpectrum A,339      (NonUnitalStarAlgHom.range P.pureStateRepresentative.gnsRepresentation) =340        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ341          P.pureStateRepresentative.GNS)342    (a : A) : IsCompactOperator (reducedAtomicRepresentation a) := by343  rw [← c0_diagonalRepresentation_coordinateC0Equiv hCCR a]344  exact CompactOperatorC0Sum.isCompactOperator_diagonalRepresentation345    (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS)346      (coordinateC0Equiv hCCR a)347348/-- The reduced atomic operator range is contained in the concrete compact349operators on the completed Hilbert sum. -/350theorem reducedAtomicRepresentation_range_le_compactOperatorStarSubalgebra351    [DiscreteTopology (PrimitiveSpectrum A)]352    (hCCR : ∀ P : PrimitiveSpectrum A,353      (NonUnitalStarAlgHom.range P.pureStateRepresentative.gnsRepresentation) =354        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ355          P.pureStateRepresentative.GNS) :356    (NonUnitalStarAlgHom.range (reducedAtomicRepresentation (A := A))) ≤357      ContinuousLinearMap.compactOperatorStarSubalgebra ℂ358        (ReducedAtomicHilbertSpace A) := by359  intro T hT360  obtain ⟨a, ha⟩ := (NonUnitalStarAlgHom.mem_range361    (reducedAtomicRepresentation (A := A))).1 hT362  rw [← ha]363  exact isCompactOperator_reducedAtomicRepresentation hCCR a364365/-- The reduced atomic representation with codomain restricted to the actual366compact operators on the Hilbert sum. -/367def reducedAtomicCompactRepresentation368    [DiscreteTopology (PrimitiveSpectrum A)]369    (hCCR : ∀ P : PrimitiveSpectrum A,370      (NonUnitalStarAlgHom.range P.pureStateRepresentative.gnsRepresentation) =371        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ372          P.pureStateRepresentative.GNS) :373    A →⋆ₙₐ[ℂ] ContinuousLinearMap.compactOperatorStarSubalgebra ℂ374      (ReducedAtomicHilbertSpace A) :=375  NonUnitalStarAlgHom.codRestrict (reducedAtomicRepresentation (A := A))376    (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ377      (ReducedAtomicHilbertSpace A))378      (isCompactOperator_reducedAtomicRepresentation hCCR)379380@[simp]381theorem reducedAtomicCompactRepresentation_apply_coe382    [DiscreteTopology (PrimitiveSpectrum A)]383    (hCCR : ∀ P : PrimitiveSpectrum A,384      (NonUnitalStarAlgHom.range P.pureStateRepresentative.gnsRepresentation) =385        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ386          P.pureStateRepresentative.GNS)387    (a : A) :388    ((reducedAtomicCompactRepresentation hCCR a :389      ContinuousLinearMap.compactOperatorStarSubalgebra ℂ390        (ReducedAtomicHilbertSpace A)) :391      ReducedAtomicHilbertSpace A →L[ℂ] ReducedAtomicHilbertSpace A) =392        reducedAtomicRepresentation a := rfl393394end PrimitiveSpectrum395396end MathlibAnnex.Analysis.CStarAlgebra