MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/ImageSubspace.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.SurjectivePreimage7import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.RepresentationComponents8import MathlibAnnex.Analysis.CStarAlgebra.Quotient.ImageRepresentation9import MathlibAnnex.Analysis.CStarAlgebra.Quotient.ImageWeakDual10import MathlibAnnex.Topology.ClosureSpace.SubspaceMaps11import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic1213/-!14# The image GSS and the closure of a component1516The codomain is the actual subspace `closure (component I)`. Equality of the17component intersection with the representation kernel only identifies this18CLOSURE. It is not used to identify the components themselves. All continuity19here is for the received closure spaces; no topology on S(A) is presumed.20-/2122set_option autoImplicit false23set_option backward.isDefEq.respectTransparency false24set_option backward.whnf.reducibleClassField false25noncomputable section26open Set Metric27open scoped CStarAlgebra2829namespace MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation3031universe u v32variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]33variable [PartialOrder A] [StarOrderedRing A]34variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]35variable (pi : NonUnitalCStarRepresentation A H)3637private def imageSubspaceContinuousMap {B : Type*} [NonUnitalCStarAlgebra B]38    (q : A →⋆ₙₐ[ℂ] B) : A →L[ℂ] B :=39  LinearMap.mkContinuous40    { toFun := q, map_add' := map_add q, map_smul' := map_smul q }41    1 (fun a => by42      change ‖q a‖ ≤ 1 * ‖a‖43      simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le q a)4445attribute [local instance] HomKernelQuotient.imageCStarAlgebra4647/-- Equality of J_C with ker(pi) identifies the closure, NOT necessarily C itself. -/48theorem closure_component_eq_hull_ker49    (I : NormedSpace.GeometricStructureSpace ℂ A)50    (hI : NormedSpace.geometricSpectrumKernel ℂ A (NormedSpace.toGeometricSpectrum ℂ A I) =51      ((imageSubspaceContinuousMap pi).ker : Set A)) :52    (NormedSpace.geometricStructureClosure ℂ A).closure53        ((NormedSpace.geometricStructureClosure ℂ A).component I) =54      ClosureSpace.HullKernel.hull (NormedSpace.geometricStructureFamily ℂ A)55        ((imageSubspaceContinuousMap pi).ker : Set A) := by56  change ClosureSpace.HullKernel.hull _57    (NormedSpace.geometricSpectrumKernel ℂ A (NormedSpace.toGeometricSpectrum ℂ A I)) = _58  rw [hI]5960/-- Theorem 5.17 for the actual image. Image order and nontriviality are supplied61by proofs inside the definition; neither is an added hypothesis. -/62def imageGeometricStructureHomeomorph (hpi : pi.IsNonzero)63    (I : NormedSpace.GeometricStructureSpace ℂ A)64    (hI : NormedSpace.geometricSpectrumKernel ℂ A (NormedSpace.toGeometricSpectrum ℂ A I) =65      ((imageSubspaceContinuousMap pi).ker : Set A)) :66    ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ (NonUnitalStarAlgHom.range pi))67      ((NormedSpace.geometricStructureClosure ℂ A).subspace68        ((NormedSpace.geometricStructureClosure ℂ A).closure69          ((NormedSpace.geometricStructureClosure ℂ A).component I))) := by70  letI : Nontrivial (NonUnitalStarAlgHom.range pi) := nontrivial_image_of_isNonzero pi hpi71  letI : PartialOrder (NonUnitalStarAlgHom.range pi) := _root_.CStarAlgebra.spectralOrder (NonUnitalStarAlgHom.range pi)72  letI : StarOrderedRing (NonUnitalStarAlgHom.range pi) := _root_.CStarAlgebra.spectralOrderedRing (NonUnitalStarAlgHom.range pi)73  let q := (NonUnitalStarAlgHom.rangeRestrict pi)74  have hq : Function.Surjective q := rangeRestrict_surjective pi75  have hker : ((imageSubspaceContinuousMap q).ker : Set A) =76      ((imageSubspaceContinuousMap pi).ker : Set A) := by77    ext a78    change q a = 0 ↔ pi a = 079    constructor80    · intro h81      exact congrArg Subtype.val h82    · intro h83      apply Subtype.ext84      change pi a = 085      exact h86  have htarget : ClosureSpace.HullKernel.hull (NormedSpace.geometricStructureFamily ℂ A)87      ((imageSubspaceContinuousMap q).ker : Set A) =88        (NormedSpace.geometricStructureClosure ℂ A).closure89          ((NormedSpace.geometricStructureClosure ℂ A).component I) := by90    rw [hker, closure_component_eq_hull_ker pi I hI]91  exact (geometricStructurePreimageHomeomorph q hq).trans92    ((ClosureSpace.Homeomorph.refl (NormedSpace.geometricStructureClosure ℂ A)).subspace93      _ _ (fun J => Set.ext_iff.mp htarget J))9495/-- No choice of an extreme functional enters the action on a GSS point. -/96@[simp]97theorem imageGeometricStructureHomeomorph_val (hpi : pi.IsNonzero)98    (I : NormedSpace.GeometricStructureSpace ℂ A)99    (hI : NormedSpace.geometricSpectrumKernel ℂ A (NormedSpace.toGeometricSpectrum ℂ A I) =100      ((imageSubspaceContinuousMap pi).ker : Set A))101    (J : NormedSpace.GeometricStructureSpace ℂ (NonUnitalStarAlgHom.range pi)) :102    ((imageGeometricStructureHomeomorph pi hpi I hI).toEquiv J).val.val =103      (NonUnitalStarAlgHom.rangeRestrict pi) ⁻¹' J.val := rfl104105/-- Every point of the specified component CLOSURE is reached. -/106theorem imageGeometricStructureHomeomorph_surjective (hpi : pi.IsNonzero)107    (I : NormedSpace.GeometricStructureSpace ℂ A)108    (hI : NormedSpace.geometricSpectrumKernel ℂ A (NormedSpace.toGeometricSpectrum ℂ A I) =109      ((imageSubspaceContinuousMap pi).ker : Set A)) :110    Function.Surjective (imageGeometricStructureHomeomorph pi hpi I hI).toEquiv :=111  (imageGeometricStructureHomeomorph pi hpi I hI).toEquiv.surjective112113/-- Forward preservation of every closure in the actual subspace. -/114theorem image_closure_imageGeometricStructureHomeomorph (hpi : pi.IsNonzero)115    (I : NormedSpace.GeometricStructureSpace ℂ A)116    (hI : NormedSpace.geometricSpectrumKernel ℂ A (NormedSpace.toGeometricSpectrum ℂ A I) =117      ((imageSubspaceContinuousMap pi).ker : Set A))118    (S : Set (NormedSpace.GeometricStructureSpace ℂ (NonUnitalStarAlgHom.range pi))) :119    (imageGeometricStructureHomeomorph pi hpi I hI).toEquiv ''120      (NormedSpace.geometricStructureClosure ℂ (NonUnitalStarAlgHom.range pi)).closure S =121        ((NormedSpace.geometricStructureClosure ℂ A).subspace122          ((NormedSpace.geometricStructureClosure ℂ A).closure123            ((NormedSpace.geometricStructureClosure ℂ A).component I))).closure124          ((imageGeometricStructureHomeomorph pi hpi I hI).toEquiv '' S) :=125  (imageGeometricStructureHomeomorph pi hpi I hI).image_closure S126127/-- Reverse preservation of every closure; this is not just a continuous bijection. -/128theorem image_closure_imageGeometricStructureHomeomorph_symm (hpi : pi.IsNonzero)129    (I : NormedSpace.GeometricStructureSpace ℂ A)130    (hI : NormedSpace.geometricSpectrumKernel ℂ A (NormedSpace.toGeometricSpectrum ℂ A I) =131      ((imageSubspaceContinuousMap pi).ker : Set A))132    (S : Set ((NormedSpace.geometricStructureClosure ℂ A).closure133      ((NormedSpace.geometricStructureClosure ℂ A).component I))) :134    (imageGeometricStructureHomeomorph pi hpi I hI).toEquiv.symm ''135        ((NormedSpace.geometricStructureClosure ℂ A).subspace136          ((NormedSpace.geometricStructureClosure ℂ A).closure137            ((NormedSpace.geometricStructureClosure ℂ A).component I))).closure S =138      (NormedSpace.geometricStructureClosure ℂ (NonUnitalStarAlgHom.range pi)).closure139        ((imageGeometricStructureHomeomorph pi hpi I hI).toEquiv.symm '' S) :=140  (imageGeometricStructureHomeomorph pi hpi I hI).symm.image_closure S141142/-- The source points can be described using exactly the pulled-back extreme functionals. -/143theorem mem_geometricStructureFamily_range_iff (hpi : pi.IsNonzero) (J : Set (NonUnitalStarAlgHom.range pi)) :144    J ∈ NormedSpace.geometricStructureFamily ℂ (NonUnitalStarAlgHom.range pi) ↔145      ∃ f : StrongDual ℂ (NonUnitalStarAlgHom.range pi),146        f.comp (imageSubspaceContinuousMap (NonUnitalStarAlgHom.rangeRestrict pi)) ∈147          (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ ∧ (f.ker : Set (NonUnitalStarAlgHom.range pi)) = J := by148  letI : Nontrivial (NonUnitalStarAlgHom.range pi) := nontrivial_image_of_isNonzero pi hpi149  letI : PartialOrder (NonUnitalStarAlgHom.range pi) := _root_.CStarAlgebra.spectralOrder (NonUnitalStarAlgHom.range pi)150  letI : StarOrderedRing (NonUnitalStarAlgHom.range pi) := _root_.CStarAlgebra.spectralOrderedRing (NonUnitalStarAlgHom.range pi)151  rw [mem_geometricStructureFamily_iff_exists_mem_extremePoints_dual_closedBall]152  exact exists_congr fun f => and_congr153    (comp_mem_extremePoints_dual_closedBall_iff_of_surjective (NonUnitalStarAlgHom.rangeRestrict pi)154      (rangeRestrict_surjective pi) f).symm Iff.rfl155156/-- A coefficient seed supplies J_C = ker(pi) by the already received full component theorem. -/157def coefficientImageGeometricStructureHomeomorph (hpi : pi.IsIrreducible)158    (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) :159    ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ (NonUnitalStarAlgHom.range pi))160      ((NormedSpace.geometricStructureClosure ℂ A).subspace161        ((NormedSpace.geometricStructureClosure ℂ A).closure162          ((NormedSpace.geometricStructureClosure ℂ A).component163            (matrixCoefficientKernel pi hpi x y hx hy)))) :=164  imageGeometricStructureHomeomorph pi hpi.1 (matrixCoefficientKernel pi hpi x y hx hy)165    (geometricSpectrumKernel_toGeometricSpectrum_matrixCoefficientKernel pi hpi x y hx hy)166167end MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation