MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SurjectivePreimage.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.FacialStructure.AnnihilatorExtreme7import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.ExtremeKernel8import MathlibAnnex.Topology.ClosureSpace.HullKernelPreimage9import MathlibAnnex.Topology.ClosureSpace.Induced1011/-!12# Geometric structure spaces under a surjective C-star homomorphism1314The points are the existing general geometric structure spaces. The inverse15family inclusion descends an arbitrary extreme functional through the FULL16annihilator equivalence. The target is the actual subspace of kernel-containing17points, not a redefined C-star structure space.1819The elementary subfamily-to-subspace identification below is specialized to20these two C-star families. It is not a second generic subfamily construction.21-/2223set_option autoImplicit false24set_option maxHeartbeats 200000025set_option synthInstance.maxHeartbeats 20000026noncomputable section27open Set Metric28open scoped CStarAlgebra2930namespace MathlibAnnex.Analysis.CStarAlgebra3132universe u v33variable {A : Type u} {B : Type v}34variable [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B]35variable [PartialOrder A] [StarOrderedRing A]36variable [PartialOrder B] [StarOrderedRing B]37variable [Nontrivial A] [Nontrivial B]38variable (q : A →⋆ₙₐ[ℂ] B) (hq : Function.Surjective q)3940private def preimageContinuousMap (q : A →⋆ₙₐ[ℂ] B) : A →L[ℂ] B :=41  LinearMap.mkContinuous42    { toFun := q, map_add' := map_add q, map_smul' := map_smul q }43    1 (fun a => by44      change ‖q a‖ ≤ 1 * ‖a‖45      simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le q a)4647include hq in48/-- BOTH directions of the actual GSS family comparison. -/49theorem preimageFamily_geometricStructureFamily_eq :50    ClosureSpace.HullKernel.preimageFamily q (NormedSpace.geometricStructureFamily ℂ B) =51      {J : Set A | J ∈ NormedSpace.geometricStructureFamily ℂ A ∧52        ((preimageContinuousMap q).ker : Set A) ⊆ J} := by53  ext J54  constructor55  · rintro ⟨L, hL, rfl⟩56    obtain ⟨f, hf, rfl⟩ :=57      (mem_geometricStructureFamily_iff_exists_mem_extremePoints_dual_closedBall L).1 hL58    refine ⟨?_, ?_⟩59    · apply (mem_geometricStructureFamily_iff_exists_mem_extremePoints_dual_closedBall _).260      exact ⟨f.comp (preimageContinuousMap q),61        comp_mem_extremePoints_dual_closedBall_of_surjective q hq hf, rfl⟩62    · intro a ha63      change f (q a) = 064      rw [show q a = 0 from ha, map_zero]65  · rintro ⟨hJ, hK⟩66    obtain ⟨g, hg, hgJ⟩ :=67      (mem_geometricStructureFamily_iff_exists_mem_extremePoints_dual_closedBall J).1 hJ68    have hga : g ∈ (preimageContinuousMap q).ker.strongDualAnnihilator := by69      intro a ha70      have hmem := hK ha71      rw [← hgJ] at hmem72      exact hmem73    let ag : (preimageContinuousMap q).ker.strongDualAnnihilator := ⟨g, hga⟩74    let f := (surjectiveDualLinearIsometryEquiv q hq).symm ag75    have hfg : f.comp (preimageContinuousMap q) = g := by76      ext a77      exact surjectiveDualLinearIsometryEquiv_symm_apply_image q hq ag a78    have hf : f ∈ (closedBall (0 : StrongDual ℂ B) 1).extremePoints ℝ := by79      have hp : f.comp (preimageContinuousMap q) ∈80          (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ ↔81          f ∈ (closedBall (0 : StrongDual ℂ B) 1).extremePoints ℝ :=82        comp_mem_extremePoints_dual_closedBall_iff_of_surjective q hq f83      apply hp.mp84      rw [hfg]85      exact hg86    refine ⟨(f.ker : Set B), ?_, ?_⟩87    · exact (mem_geometricStructureFamily_iff_exists_mem_extremePoints_dual_closedBall _).288        ⟨f, hf, rfl⟩89    · calc90        q ⁻¹' (f.ker : Set B) = ((f.comp (preimageContinuousMap q)).ker : Set A) := rfl91        _ = (g.ker : Set A) := congrArg (fun k : StrongDual ℂ A => (k.ker : Set A)) hfg92        _ = J := hgJ9394/-- The preimage-family type is the actual kernel-containing SUBTYPE of S(A). -/95def preimageFamilyKernelHullEquiv :96    ClosureSpace.HullKernel.preimageFamily q (NormedSpace.geometricStructureFamily ℂ B) ≃97      ClosureSpace.HullKernel.hull (NormedSpace.geometricStructureFamily ℂ A)98        ((preimageContinuousMap q).ker : Set A) where99  toFun J := by100    have heq := congrArg (fun F : Set (Set A) => J.val ∈ F)101      (preimageFamily_geometricStructureFamily_eq q hq)102    have h := Eq.mp heq J.property103    exact ⟨⟨J.val, h.1⟩, h.2⟩104  invFun J := by105    refine ⟨J.val.val, ?_⟩106    rw [preimageFamily_geometricStructureFamily_eq q hq]107    exact ⟨J.val.property, J.property⟩108  left_inv J := Subtype.ext rfl109  right_inv J := by apply Subtype.ext; exact Subtype.ext rfl110111@[simp]112theorem preimageFamilyKernelHullEquiv_val113    (J : ClosureSpace.HullKernel.preimageFamily q (NormedSpace.geometricStructureFamily ℂ B)) :114    (preimageFamilyKernelHullEquiv q hq J).val.val = J.val := rfl115116/-- All-subset closure preservation into the actual subspace of S(A).117No finite-union/topologizability hypothesis is used. -/118theorem image_closure_preimageFamilyKernelHullEquiv119    (S : Set (ClosureSpace.HullKernel.preimageFamily q120      (NormedSpace.geometricStructureFamily ℂ B))) :121    preimageFamilyKernelHullEquiv q hq ''122        (ClosureSpace.HullKernel.space _123          (ClosureSpace.HullKernel.univ_notMem_preimageFamily q hq _124            (NormedSpace.univ_notMem_geometricStructureFamily ℂ B))).closure S =125      ((NormedSpace.geometricStructureClosure ℂ A).subspace126        (ClosureSpace.HullKernel.hull (NormedSpace.geometricStructureFamily ℂ A)127          ((preimageContinuousMap q).ker : Set A))).closure128            (preimageFamilyKernelHullEquiv q hq '' S) := by129  let e := preimageFamilyKernelHullEquiv q hq130  ext I131  obtain ⟨J, rfl⟩ := e.surjective I132  constructor133  · rintro ⟨J', hJ', heq⟩134    have hJJ : J' = J := e.injective heq135    subst J'136    change ClosureSpace.HullKernel.kernel _137      (Subtype.val '' (e '' S)) ⊆ (e J).val.val138    change ClosureSpace.HullKernel.kernel _ S ⊆ J.val at hJ'139    intro a ha140    apply hJ'141    intro L hL142    exact ha (e L).val ⟨e L, ⟨L, hL, rfl⟩, rfl⟩143  · intro hJ144    change ClosureSpace.HullKernel.kernel _ (Subtype.val '' (e '' S)) ⊆145      (e J).val.val at hJ146    refine ⟨J, ?_, rfl⟩147    change ClosureSpace.HullKernel.kernel _ S ⊆ J.val148    intro a ha149    apply hJ150    rintro L ⟨M, ⟨N, hN, rfl⟩, rfl⟩151    exact ha N hN152153/-- The second, subfamily-to-subspace stage of the comparison. -/154def preimageFamilyKernelHullHomeomorph :155    ClosureSpace.Homeomorph156      (ClosureSpace.HullKernel.space _157        (ClosureSpace.HullKernel.univ_notMem_preimageFamily q hq _158          (NormedSpace.univ_notMem_geometricStructureFamily ℂ B)))159      ((NormedSpace.geometricStructureClosure ℂ A).subspace160        (ClosureSpace.HullKernel.hull (NormedSpace.geometricStructureFamily ℂ A)161          ((preimageContinuousMap q).ker : Set A))) :=162  ClosureSpace.Homeomorph.ofImageClosure _ _ (preimageFamilyKernelHullEquiv q hq)163    (image_closure_preimageFamilyKernelHullEquiv q hq)164165/-- The existing MAIN preimage homeomorphism followed by the actual subspace comparison. -/166def geometricStructurePreimageHomeomorph :167    ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ B)168      ((NormedSpace.geometricStructureClosure ℂ A).subspace169        (ClosureSpace.HullKernel.hull (NormedSpace.geometricStructureFamily ℂ A)170          ((preimageContinuousMap q).ker : Set A))) :=171  (ClosureSpace.HullKernel.homeomorphPreimage q hq172    (NormedSpace.geometricStructureFamily ℂ B)173    (NormedSpace.univ_notMem_geometricStructureFamily ℂ B)).trans174      (preimageFamilyKernelHullHomeomorph q hq)175176/-- Every point is sent to its literal preimage, independently of functional choices. -/177@[simp]178theorem geometricStructurePreimageHomeomorph_val (J : NormedSpace.GeometricStructureSpace ℂ B) :179    ((geometricStructurePreimageHomeomorph q hq).toEquiv J).val.val = q ⁻¹' J.val := rfl180181/-- Inverse set recovery in the original algebra. -/182theorem geometricStructurePreimageHomeomorph_symm_val183    (I : ClosureSpace.HullKernel.hull (NormedSpace.geometricStructureFamily ℂ A)184      ((preimageContinuousMap q).ker : Set A)) :185    q ⁻¹' ((geometricStructurePreimageHomeomorph q hq).toEquiv.symm I).val = I.val.val := by186  have h := congrArg (fun J => J.val.val)187    ((geometricStructurePreimageHomeomorph q hq).toEquiv.apply_symm_apply I)188  exact h189190/-- All closures, not only finite closures, are transported forward. -/191theorem image_closure_geometricStructurePreimageHomeomorph192    (S : Set (NormedSpace.GeometricStructureSpace ℂ B)) :193    (geometricStructurePreimageHomeomorph q hq).toEquiv ''194        (NormedSpace.geometricStructureClosure ℂ B).closure S =195      ((NormedSpace.geometricStructureClosure ℂ A).subspace196        (ClosureSpace.HullKernel.hull (NormedSpace.geometricStructureFamily ℂ A)197          ((preimageContinuousMap q).ker : Set A))).closure198        ((geometricStructurePreimageHomeomorph q hq).toEquiv '' S) :=199  (geometricStructurePreimageHomeomorph q hq).image_closure S200201/-- The inverse preserves arbitrary closures in the actual target subspace. -/202theorem image_closure_geometricStructurePreimageHomeomorph_symm203    (S : Set (ClosureSpace.HullKernel.hull (NormedSpace.geometricStructureFamily ℂ A)204      ((preimageContinuousMap q).ker : Set A))) :205    (geometricStructurePreimageHomeomorph q hq).toEquiv.symm ''206        ((NormedSpace.geometricStructureClosure ℂ A).subspace207          (ClosureSpace.HullKernel.hull (NormedSpace.geometricStructureFamily ℂ A)208            ((preimageContinuousMap q).ker : Set A))).closure S =209      (NormedSpace.geometricStructureClosure ℂ B).closure210        ((geometricStructurePreimageHomeomorph q hq).toEquiv.symm '' S) :=211  (geometricStructurePreimageHomeomorph q hq).symm.image_closure S212213end MathlibAnnex.Analysis.CStarAlgebra