MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/RepresentationComponents.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-/6import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.CoefficientPair7import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.CoefficientFamily8import MathlibAnnex.Analysis.Normed.GeometricStructure.Spectrum910/-!11# Actual components and irreducible representations1213Each point in a finite chain is given its own actual extreme-functional14representative and original-algebra cyclic coefficient model. The existing15`Relation.EqvGen` induction transports unitary equivalence along that chain.16Nothing is proved by identifying representation kernels with functional kernels.1718The full component, not just a subset of it, is the coefficient-kernel family.19Only after this equality is established is its intersection transported to the20received geometric spectrum and the actual map gamma.21-/2223set_option autoImplicit false24noncomputable section25open Set Metric26open scoped CStarAlgebra ComplexOrder2728namespace MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation2930universe u v w31variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]32variable [PartialOrder A] [StarOrderedRing A]33variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]34variable {K : Type w} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]3536private def componentContinuousMap (pi : NonUnitalCStarRepresentation A H) :37    A →L[ℂ] (H →L[ℂ] H) :=38  LinearMap.mkContinuous39    { toFun := pi, map_add' := map_add pi, map_smul' := map_smul pi }40    1 (fun a => by41      change ‖pi a‖ ≤ 1 * ‖a‖42      simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le pi a)4344/-- The reverse direction of the component/representation bridge. Intermediate45points in the received finite-chain relation are realized, not postulated to46have a representation attached to their labels. -/47theorem unitaryEquivalent_of_related_matrixCoefficientKernel48    (pi : NonUnitalCStarRepresentation A H) (sigma : NonUnitalCStarRepresentation A K)49    (hpi : pi.IsIrreducible) (hsigma : sigma.IsIrreducible)50    (x y : H) (z w : K) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) (hw : w ≠ 0)51    (hrel : (NormedSpace.geometricStructureClosure ℂ A).Related52      (matrixCoefficientKernel pi hpi x y hx hy) (matrixCoefficientKernel sigma hsigma z w hz hw)) :53    pi.UnitaryEquivalent sigma := by54  classical55  let c := NormedSpace.geometricStructureClosure ℂ A56  choose rho hext hker using fun I : NormedSpace.GeometricStructureSpace ℂ A =>57    (mem_geometricStructureFamily_iff_exists_mem_extremePoints_dual_closedBall I.val).1 I.property58  have hn (I : NormedSpace.GeometricStructureSpace ℂ A) : ‖rho I‖ = 1 :=59    norm_eq_one_of_mem_extremePoints_dual_closedBall (hext I)60  have h0 (I : NormedSpace.GeometricStructureSpace ℂ A) : rho I ≠ 0 :=61    norm_ne_zero_iff.mp (by rw [hn I]; exact one_ne_zero)62  let r (I : NormedSpace.GeometricStructureSpace ℂ A) :=63    NonUnitalFunctional.cyclicRepresentation (rho I) (h0 I)64  let p (I : NormedSpace.GeometricStructureSpace ℂ A) :=65    NonUnitalFunctional.cyclicSourceVector (rho I) (h0 I)66  let q (I : NormedSpace.GeometricStructureSpace ℂ A) :=67    NonUnitalFunctional.cyclicTargetVector (rho I) (h0 I)68  have hirr (I : NormedSpace.GeometricStructureSpace ℂ A) : (r I).IsIrreducible :=69    NonUnitalFunctional.isIrreducible_cyclicRepresentation (rho I) (h0 I) (hext I)70  have hp (I : NormedSpace.GeometricStructureSpace ℂ A) : p I ≠ 0 :=71    norm_ne_zero_iff.mp (by rw [NonUnitalFunctional.norm_cyclicSourceVector]; exact one_ne_zero)72  have hq (I : NormedSpace.GeometricStructureSpace ℂ A) : q I ≠ 0 :=73    norm_ne_zero_iff.mp (by rw [NonUnitalFunctional.norm_cyclicTargetVector]; exact one_ne_zero)74  have hpoint (I : NormedSpace.GeometricStructureSpace ℂ A) :75      matrixCoefficientKernel (r I) (hirr I) (p I) (q I) (hp I) (hq I) = I := by76    apply Subtype.ext77    change ((matrixCoefficient (r I) (p I) (q I)).ker : Set A) = I.val78    rw [NonUnitalFunctional.matrixCoefficient_cyclicRepresentation_of_norm_eq_one _ _ (hn I)]79    exact hker I80  have hchain {I J : NormedSpace.GeometricStructureSpace ℂ A} (h : c.Related I J) :81      (r I).UnitaryEquivalent (r J) := by82    change Relation.EqvGen c.Linked I J at h83    induction h with84    | rel I J hIJ =>85        apply unitaryEquivalent_of_linked_matrixCoefficientKernel (r I) (r J) (hirr I) (hirr J)86          (p I) (q I) (p J) (q J) (hp I) (hq I) (hp J) (hq J)87        rw [hpoint I, hpoint J]88        exact hIJ89    | refl I => exact unitaryEquivalent_refl (r I)90    | symm I J _ ih => exact ih.symm91    | trans I J L _ _ ih1 ih2 => exact ih1.trans ih292  let P := matrixCoefficientKernel pi hpi x y hx hy93  let Q := matrixCoefficientKernel sigma hsigma z w hz hw94  have hstart : pi.UnitaryEquivalent (r P) :=95    unitaryEquivalent_of_linked_matrixCoefficientKernel pi (r P) hpi (hirr P)96      x y (p P) (q P) hx hy (hp P) (hq P) (Or.inl (hpoint P).symm)97  have hend : sigma.UnitaryEquivalent (r Q) :=98    unitaryEquivalent_of_linked_matrixCoefficientKernel sigma (r Q) hsigma (hirr Q)99      z w (p Q) (q Q) hz hw (hp Q) (hq Q) (Or.inl (hpoint Q).symm)100  exact hstart.trans ((hchain hrel).trans hend.symm)101102/-- Same component is exactly unitary equivalence, for arbitrary nonzero103coefficient vectors in arbitrary nonzero irreducible representations. -/104theorem related_matrixCoefficientKernel_iff_unitaryEquivalent105    (pi : NonUnitalCStarRepresentation A H) (sigma : NonUnitalCStarRepresentation A K)106    (hpi : pi.IsIrreducible) (hsigma : sigma.IsIrreducible)107    (x y : H) (z w : K) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) (hw : w ≠ 0) :108    (NormedSpace.geometricStructureClosure ℂ A).Related109      (matrixCoefficientKernel pi hpi x y hx hy) (matrixCoefficientKernel sigma hsigma z w hz hw) ↔110        pi.UnitaryEquivalent sigma :=111  ⟨unitaryEquivalent_of_related_matrixCoefficientKernel pi sigma hpi hsigma x y z w hx hy hz hw,112    fun h => related_matrixCoefficientKernel_of_unitaryEquivalent113      pi sigma hpi hsigma h x y z w hx hy hz hw⟩114115/-- The entire component equals the coefficient-kernel family. The reverse116inclusion realizes an arbitrary component point and uses the proved converse117of the finite-chain bridge before transporting its actual coefficient vectors. -/118theorem component_matrixCoefficientKernel_eq_family119    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)120    (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) :121    (NormedSpace.geometricStructureClosure ℂ A).component122      (matrixCoefficientKernel pi hpi x y hx hy) = matrixCoefficientKernelFamily pi hpi := by123  apply Set.Subset.antisymm124  · intro I hI125    obtain ⟨rho, hext, hker⟩ :=126      (mem_geometricStructureFamily_iff_exists_mem_extremePoints_dual_closedBall I.val).1 I.property127    have hn : ‖rho‖ = 1 := norm_eq_one_of_mem_extremePoints_dual_closedBall hext128    have h0 : rho ≠ 0 := norm_ne_zero_iff.mp (by rw [hn]; exact one_ne_zero)129    let r := NonUnitalFunctional.cyclicRepresentation rho h0130    let p := NonUnitalFunctional.cyclicSourceVector rho h0131    let q := NonUnitalFunctional.cyclicTargetVector rho h0132    have hirr : r.IsIrreducible := NonUnitalFunctional.isIrreducible_cyclicRepresentation rho h0 hext133    have hp : p ≠ 0 := norm_ne_zero_iff.mp (by rw [NonUnitalFunctional.norm_cyclicSourceVector]; exact one_ne_zero)134    have hq : q ≠ 0 := norm_ne_zero_iff.mp (by rw [NonUnitalFunctional.norm_cyclicTargetVector]; exact one_ne_zero)135    have hpoint : matrixCoefficientKernel r hirr p q hp hq = I := by136      apply Subtype.ext137      change ((matrixCoefficient r p q).ker : Set A) = I.val138      rw [NonUnitalFunctional.matrixCoefficient_cyclicRepresentation_of_norm_eq_one _ _ hn]139      exact hker140    have hrel : (NormedSpace.geometricStructureClosure ℂ A).Related141        (matrixCoefficientKernel r hirr p q hp hq) (matrixCoefficientKernel pi hpi x y hx hy) := by142      rw [hpoint]143      exact (NormedSpace.geometricStructureClosure ℂ A).related_symm hI144    obtain ⟨U, hU⟩ :=145      unitaryEquivalent_of_related_matrixCoefficientKernel r pi hirr hpi p q x y hp hq hx hy hrel146    have hpU : U p ≠ 0 := fun h => hp (U.injective (h.trans (map_zero U).symm))147    have hqU : U q ≠ 0 := fun h => hq (U.injective (h.trans (map_zero U).symm))148    refine ⟨U p, U q, hpU, hqU, ?_⟩149    exact (matrixCoefficientKernel_eq_of_intertwines r pi hirr hpi U hU p q hp hq).trans hpoint150  · exact matrixCoefficientKernelFamily_subset_component pi hpi x y hx hy151152/-- Paper 5.10 on the received geometric spectrum: J_C is ker(pi) only after153identifying C with the whole coefficient-kernel family. -/154theorem geometricSpectrumKernel_toGeometricSpectrum_matrixCoefficientKernel155    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)156    (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) :157    NormedSpace.geometricSpectrumKernel ℂ A158      (NormedSpace.toGeometricSpectrum ℂ A (matrixCoefficientKernel pi hpi x y hx hy)) =159        ((componentContinuousMap pi).ker : Set A) := by160  change {a : A | ∀ I : NormedSpace.GeometricStructureSpace ℂ A,161    I ∈ (NormedSpace.geometricStructureClosure ℂ A).component162      (matrixCoefficientKernel pi hpi x y hx hy) → a ∈ I.val} = _163  rw [component_matrixCoefficientKernel_eq_family]164  exact setOf_forall_mem_matrixCoefficientKernelFamily_eq_ker pi hpi165166/-- The same kernel identity on the actual gamma map, with no new primitive167spectrum or quotient relation introduced. This is a source interface for the168separate topological comparison. -/169theorem geometricSpectrumToPrimitive_toGeometricSpectrum_matrixCoefficientKernel_val170    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)171    (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) :172    (NormedSpace.geometricSpectrumToPrimitive ℂ A173      (NormedSpace.toGeometricSpectrum ℂ A (matrixCoefficientKernel pi hpi x y hx hy))).val =174        ((componentContinuousMap pi).ker : Set A) := by175  rw [NormedSpace.geometricSpectrumToPrimitive_val]176  exact geometricSpectrumKernel_toGeometricSpectrum_matrixCoefficientKernel pi hpi x y hx hy177178end MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation