MathlibAnnex/Analysis/Normed/GeometricStructure/SpectrumMap.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-/6module78public import MathlibAnnex.Analysis.Normed.GeometricStructure.SpectrumTransforms9public import MathlibAnnex.Topology.ClosureSpace.TransformMap1011/-!12# Transport of the concrete geometric spectra1314A homeomorphism of geometric structure spaces acts on the concrete spectra by15conjugating the generic G/P homeomorphisms with the previously constructed16comparison homeomorphisms. In particular, the primitive map is not an image17map on subsets of the underlying normed space: the given map has domain `S(E)`,18not `E`.1920The scalar fields and the universes of the normed spaces are independent.21No completeness, nontriviality, or injectivity of gamma is assumed.22-/2324@[expose] public section2526set_option autoImplicit false2728noncomputable section2930open Set3132universe u v w z3334namespace NormedSpace3536variable {𝕜 : Type v} {𝕝 : Type z} [RCLike 𝕜] [RCLike 𝕝]37variable {E : Type u} {F : Type w}38variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]39variable [NormedAddCommGroup F] [NormedSpace 𝕝 F]40variable (e : ClosureSpace.Homeomorph (geometricStructureClosure 𝕜 E)41  (geometricStructureClosure 𝕝 F))4243/-- Transport actual component sets through the generic quotient transform. -/44def geometricSpectrumHomeomorph :45    ClosureSpace.Homeomorph (geometricSpectrumClosure 𝕜 E) (geometricSpectrumClosure 𝕝 F) :=46  ((gTransformHomeomorphGeometricSpectrum 𝕜 E).symm.trans e.gHomeomorph).trans47    (gTransformHomeomorphGeometricSpectrum 𝕝 F)4849/-- Transport primitive component kernels through the closed-component transform. -/50def primitiveGeometricSpectrumHomeomorph :51    ClosureSpace.Homeomorph (primitiveGeometricSpectrumClosure 𝕜 E)52      (primitiveGeometricSpectrumClosure 𝕝 F) :=53  ((pTransformHomeomorphPrimitiveGeometricSpectrum 𝕜 E).symm.trans e.pHomeomorph).trans54    (pTransformHomeomorphPrimitiveGeometricSpectrum 𝕝 F)5556/-- Compatibility of the concrete G-map with the generic G-map. -/57theorem geometricSpectrumHomeomorph_gTransform (q : (geometricStructureClosure 𝕜 E).GPoint) :58    (geometricSpectrumHomeomorph e).toEquiv59        ((gTransformHomeomorphGeometricSpectrum 𝕜 E).toEquiv q) =60      (gTransformHomeomorphGeometricSpectrum 𝕝 F).toEquiv (e.gHomeomorph.toEquiv q) := by61  change (gTransformHomeomorphGeometricSpectrum 𝕝 F).toEquiv62    (e.gHomeomorph.toEquiv ((gTransformHomeomorphGeometricSpectrum 𝕜 E).toEquiv.symm63      ((gTransformHomeomorphGeometricSpectrum 𝕜 E).toEquiv q))) = _64  rw [Equiv.symm_apply_apply]6566/-- Compatibility of the concrete P-map with the generic P-map. -/67theorem primitiveGeometricSpectrumHomeomorph_pTransform68    (p : (geometricStructureClosure 𝕜 E).PPoint) :69    (primitiveGeometricSpectrumHomeomorph e).toEquiv70        ((pTransformHomeomorphPrimitiveGeometricSpectrum 𝕜 E).toEquiv p) =71      (pTransformHomeomorphPrimitiveGeometricSpectrum 𝕝 F).toEquiv72        (e.pHomeomorph.toEquiv p) := by73  change (pTransformHomeomorphPrimitiveGeometricSpectrum 𝕝 F).toEquiv74    (e.pHomeomorph.toEquiv ((pTransformHomeomorphPrimitiveGeometricSpectrum 𝕜 E).toEquiv.symm75      ((pTransformHomeomorphPrimitiveGeometricSpectrum 𝕜 E).toEquiv p))) = _76  rw [Equiv.symm_apply_apply]7778/-- The formula `C(I) ↦ C(e(I))`, for the actual component-set spectra. -/79@[simp]80theorem geometricSpectrumHomeomorph_toGeometricSpectrum (I : GeometricStructureSpace 𝕜 E) :81    (geometricSpectrumHomeomorph e).toEquiv (toGeometricSpectrum 𝕜 E I) =82      toGeometricSpectrum 𝕝 F (e.toEquiv I) := by83  change (gTransformHomeomorphGeometricSpectrum 𝕝 F).toEquiv84    (e.gMap ((gTransformHomeomorphGeometricSpectrum 𝕜 E).toEquiv.symm85      (toGeometricSpectrum 𝕜 E I))) = _86  rw [gTransformHomeomorphGeometricSpectrum_symm_toGeometricSpectrum,87    e.gMap_toGPoint, gTransformHomeomorphGeometricSpectrum_toGPoint]8889/-- The formula `J_C(I) ↦ J_C(e(I))`; this is not an image of a subset of `E`. -/90@[simp]91theorem primitiveGeometricSpectrumHomeomorph_toPrimitiveGeometricSpectrum92    (I : GeometricStructureSpace 𝕜 E) :93    (primitiveGeometricSpectrumHomeomorph e).toEquiv (toPrimitiveGeometricSpectrum 𝕜 E I) =94      toPrimitiveGeometricSpectrum 𝕝 F (e.toEquiv I) := by95  rw [← pTransformHomeomorphPrimitiveGeometricSpectrum_toPPoint 𝕜 E I,96    primitiveGeometricSpectrumHomeomorph_pTransform]97  change (pTransformHomeomorphPrimitiveGeometricSpectrum 𝕝 F).toEquiv98    (e.pMap ((geometricStructureClosure 𝕜 E).toPPoint I)) = _99  rw [e.pMap_toPPoint, pTransformHomeomorphPrimitiveGeometricSpectrum_toPPoint]100101/-- The inverse component map is given by the inverse geometric-structure map. -/102@[simp]103theorem geometricSpectrumHomeomorph_symm_toGeometricSpectrum104    (J : GeometricStructureSpace 𝕝 F) :105    (geometricSpectrumHomeomorph e).toEquiv.symm (toGeometricSpectrum 𝕝 F J) =106      toGeometricSpectrum 𝕜 E (e.toEquiv.symm J) := by107  apply (geometricSpectrumHomeomorph e).toEquiv.injective108  rw [Equiv.apply_symm_apply, geometricSpectrumHomeomorph_toGeometricSpectrum,109    Equiv.apply_symm_apply]110111/-- The inverse primitive map is computed on representatives, without choosing a vector map. -/112@[simp]113theorem primitiveGeometricSpectrumHomeomorph_symm_toPrimitiveGeometricSpectrum114    (J : GeometricStructureSpace 𝕝 F) :115    (primitiveGeometricSpectrumHomeomorph e).toEquiv.symm (toPrimitiveGeometricSpectrum 𝕝 F J) =116      toPrimitiveGeometricSpectrum 𝕜 E (e.toEquiv.symm J) := by117  apply (primitiveGeometricSpectrumHomeomorph e).toEquiv.injective118  rw [Equiv.apply_symm_apply,119    primitiveGeometricSpectrumHomeomorph_toPrimitiveGeometricSpectrum, Equiv.apply_symm_apply]120121/-- The inverse equivalence equals transport by the inverse homeomorphism. -/122theorem geometricSpectrumHomeomorph_symm :123    (geometricSpectrumHomeomorph e).toEquiv.symm =124      (geometricSpectrumHomeomorph e.symm).toEquiv := by125  apply Equiv.ext126  intro C127  obtain ⟨J, rfl⟩ := toGeometricSpectrum_surjective 𝕝 F C128  simp only [geometricSpectrumHomeomorph_symm_toGeometricSpectrum,129    geometricSpectrumHomeomorph_toGeometricSpectrum]130  rfl131132/-- The same inverse identity for primitive spectra. -/133theorem primitiveGeometricSpectrumHomeomorph_symm :134    (primitiveGeometricSpectrumHomeomorph e).toEquiv.symm =135      (primitiveGeometricSpectrumHomeomorph e.symm).toEquiv := by136  apply Equiv.ext137  intro J138  obtain ⟨I, rfl⟩ := toPrimitiveGeometricSpectrum_surjective 𝕝 F J139  simp only [primitiveGeometricSpectrumHomeomorph_symm_toPrimitiveGeometricSpectrum,140    primitiveGeometricSpectrumHomeomorph_toPrimitiveGeometricSpectrum]141  rfl142143/-- On component subsets the forward G-map is the actual image under `e : S(E) → S(F)`. -/144theorem geometricSpectrumHomeomorph_val (C : GeometricSpectrum 𝕜 E) :145    ((geometricSpectrumHomeomorph e).toEquiv C).val = e.toEquiv '' C.val := by146  obtain ⟨I, rfl⟩ := toGeometricSpectrum_surjective 𝕜 E C147  rw [geometricSpectrumHomeomorph_toGeometricSpectrum]148  exact (e.toFiniteHomeomorph.image_component I).symm149150/-- On primitive points the correct formula is the intersection of a transported hull in `S(F)`. -/151theorem primitiveGeometricSpectrumHomeomorph_val (J : PrimitiveGeometricSpectrum 𝕜 E) :152    ((primitiveGeometricSpectrumHomeomorph e).toEquiv J).val =153      ClosureSpace.HullKernel.kernel (geometricStructureFamily 𝕝 F)154        (e.toEquiv '' {I : GeometricStructureSpace 𝕜 E | J.val ⊆ I.val}) := rfl155156/-- Forward preservation of the full geometric closure, including empty selections. -/157theorem image_geometricSpectrumClosure (S : Set (GeometricSpectrum 𝕜 E)) :158    (geometricSpectrumHomeomorph e).toEquiv '' (geometricSpectrumClosure 𝕜 E).closure S =159      (geometricSpectrumClosure 𝕝 F).closure ((geometricSpectrumHomeomorph e).toEquiv '' S) :=160  (geometricSpectrumHomeomorph e).image_closure S161162/-- Forward preservation of the full primitive closure. -/163theorem image_primitiveGeometricSpectrumClosure (S : Set (PrimitiveGeometricSpectrum 𝕜 E)) :164    (primitiveGeometricSpectrumHomeomorph e).toEquiv ''165        (primitiveGeometricSpectrumClosure 𝕜 E).closure S =166      (primitiveGeometricSpectrumClosure 𝕝 F).closure167        ((primitiveGeometricSpectrumHomeomorph e).toEquiv '' S) :=168  (primitiveGeometricSpectrumHomeomorph e).image_closure S169170/-- The inverse geometric map also preserves every closure. -/171theorem image_symm_geometricSpectrumClosure (S : Set (GeometricSpectrum 𝕝 F)) :172    (geometricSpectrumHomeomorph e).toEquiv.symm '' (geometricSpectrumClosure 𝕝 F).closure S =173      (geometricSpectrumClosure 𝕜 E).closure174        ((geometricSpectrumHomeomorph e).toEquiv.symm '' S) :=175  (geometricSpectrumHomeomorph e).symm.image_closure S176177/-- The inverse primitive map also preserves every closure. -/178theorem image_symm_primitiveGeometricSpectrumClosure (S : Set (PrimitiveGeometricSpectrum 𝕝 F)) :179    (primitiveGeometricSpectrumHomeomorph e).toEquiv.symm ''180        (primitiveGeometricSpectrumClosure 𝕝 F).closure S =181      (primitiveGeometricSpectrumClosure 𝕜 E).closure182        ((primitiveGeometricSpectrumHomeomorph e).toEquiv.symm '' S) :=183  (primitiveGeometricSpectrumHomeomorph e).symm.image_closure S184185/-- The gamma square commutes on every concrete geometric-spectrum point. -/186theorem geometricSpectrumToPrimitive_geometricSpectrumHomeomorph (C : GeometricSpectrum 𝕜 E) :187    geometricSpectrumToPrimitive 𝕝 F ((geometricSpectrumHomeomorph e).toEquiv C) =188      (primitiveGeometricSpectrumHomeomorph e).toEquiv (geometricSpectrumToPrimitive 𝕜 E C) := by189  obtain ⟨I, rfl⟩ := toGeometricSpectrum_surjective 𝕜 E C190  rw [geometricSpectrumHomeomorph_toGeometricSpectrum,191    geometricSpectrumToPrimitive_toGeometricSpectrum,192    geometricSpectrumToPrimitive_toGeometricSpectrum,193    primitiveGeometricSpectrumHomeomorph_toPrimitiveGeometricSpectrum]194195/-- Function-level form of the commuting square in Corollary 4.17. -/196theorem geometricSpectrumToPrimitive_comp_geometricSpectrumHomeomorph :197    geometricSpectrumToPrimitive 𝕝 F ∘ (geometricSpectrumHomeomorph e).toEquiv =198      (primitiveGeometricSpectrumHomeomorph e).toEquiv ∘ geometricSpectrumToPrimitive 𝕜 E :=199  funext (geometricSpectrumToPrimitive_geometricSpectrumHomeomorph e)200201include e in202/-- Injectivity of gamma is invariant under geometric-structure homeomorphisms.203The argument uses the two constructed bijections, not just surjectivity of gamma. -/204theorem geometricSpectrumToPrimitive_injective_iff_of_homeomorph :205    Function.Injective (geometricSpectrumToPrimitive 𝕜 E) ↔206      Function.Injective (geometricSpectrumToPrimitive 𝕝 F) := by207  constructor208  · intro hE C D hCD209    apply (geometricSpectrumHomeomorph e).toEquiv.symm.injective210    apply hE211    apply (primitiveGeometricSpectrumHomeomorph e).toEquiv.injective212    rw [← geometricSpectrumToPrimitive_geometricSpectrumHomeomorph,213      ← geometricSpectrumToPrimitive_geometricSpectrumHomeomorph,214      Equiv.apply_symm_apply, Equiv.apply_symm_apply]215    exact hCD216  · intro hF C D hCD217    apply (geometricSpectrumHomeomorph e).toEquiv.injective218    apply hF219    rw [geometricSpectrumToPrimitive_geometricSpectrumHomeomorph,220      geometricSpectrumToPrimitive_geometricSpectrumHomeomorph, hCD]221222end NormedSpace