MathlibAnnex/Analysis/Normed/GeometricStructure/Spectrum.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.Basic9public import MathlibAnnex.Topology.ClosureSpace.HullKernelTransforms1011/-!12# The geometric and primitive geometric spectra1314The geometric spectrum consists of actual component subsets of the geometric15structure space. The primitive geometric spectrum consists of their intersections16in the original normed space. These are different types from the quotient17`GPoint` and from the closed-component `PPoint`, respectively.1819The closure formulas below give the closures of Definition 4.6 and Theorem 4.7.20All intersections are intersections of sets, not submodules or ideals. Empty21intersections are `univ`. No completeness or nontriviality is required.22-/2324@[expose] public section2526set_option autoImplicit false2728universe u v2930namespace NormedSpace3132variable (𝕜 : Type v) [RCLike 𝕜]33variable (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E]3435/-- The geometric spectrum as a family of component subsets of `S(E)`. -/36def geometricSpectrumFamily : Set (Set (GeometricStructureSpace 𝕜 E)) :=37  (geometricStructureClosure 𝕜 E).componentFamily3839/-- A point of the geometric spectrum is an actual component subset. -/40def GeometricSpectrum : Type u :=41  {C : Set (GeometricStructureSpace 𝕜 E) // C ∈ geometricSpectrumFamily 𝕜 E}4243/-- The intersection `J_C` of the geometric-structure points in a component. -/44def geometricSpectrumKernel (C : GeometricSpectrum 𝕜 E) : Set E :=45  ClosureSpace.HullKernel.kernel (geometricStructureFamily 𝕜 E) C.val4647/-- The primitive geometric spectrum as a family of subsets of `E`. -/48def primitiveGeometricSpectrumFamily : Set (Set E) :=49  ClosureSpace.HullKernel.componentKernelFamily (geometricStructureFamily 𝕜 E)50    (univ_notMem_geometricStructureFamily 𝕜 E)5152/-- A primitive geometric point is an intersection in `E`, not a subset of `S(E)`. -/53def PrimitiveGeometricSpectrum : Type u :=54  {J : Set E // J ∈ primitiveGeometricSpectrumFamily 𝕜 E}5556/-- Send a geometric-structure point to its component. -/57def toGeometricSpectrum (I : GeometricStructureSpace 𝕜 E) : GeometricSpectrum 𝕜 E :=58  (geometricStructureClosure 𝕜 E).toComponentPoint I5960/-- Send a geometric-structure point to the intersection of its component. -/61def toPrimitiveGeometricSpectrum (I : GeometricStructureSpace 𝕜 E) :62    PrimitiveGeometricSpectrum 𝕜 E :=63  ClosureSpace.HullKernel.toComponentKernelPoint (geometricStructureFamily 𝕜 E)64    (univ_notMem_geometricStructureFamily 𝕜 E) I6566/-- The map gamma: a component is sent to the intersection of its members.67It is surjective; injectivity is a separate condition. -/68def geometricSpectrumToPrimitive : GeometricSpectrum 𝕜 E → PrimitiveGeometricSpectrum 𝕜 E :=69  ClosureSpace.HullKernel.componentPointToComponentKernelPoint70    (geometricStructureFamily 𝕜 E) (univ_notMem_geometricStructureFamily 𝕜 E)7172@[simp]73theorem geometricSpectrumToPrimitive_val (C : GeometricSpectrum 𝕜 E) :74    (geometricSpectrumToPrimitive 𝕜 E C).val = geometricSpectrumKernel 𝕜 E C := rfl7576@[simp]77theorem geometricSpectrumToPrimitive_toGeometricSpectrum (I : GeometricStructureSpace 𝕜 E) :78    geometricSpectrumToPrimitive 𝕜 E (toGeometricSpectrum 𝕜 E I) =79      toPrimitiveGeometricSpectrum 𝕜 E I := rfl8081theorem toGeometricSpectrum_surjective : Function.Surjective (toGeometricSpectrum 𝕜 E) :=82  (geometricStructureClosure 𝕜 E).toComponentPoint_surjective8384theorem toPrimitiveGeometricSpectrum_surjective :85    Function.Surjective (toPrimitiveGeometricSpectrum 𝕜 E) :=86  ClosureSpace.HullKernel.toComponentKernelPoint_surjective _ _8788theorem geometricSpectrumToPrimitive_surjective :89    Function.Surjective (geometricSpectrumToPrimitive 𝕜 E) :=90  ClosureSpace.HullKernel.componentPointToComponentKernelPoint_surjective _ _9192/-- The primitive family is exactly the collection of intersections of component sets. -/93theorem primitiveGeometricSpectrumFamily_eq_range :94    primitiveGeometricSpectrumFamily 𝕜 E = Set.range (geometricSpectrumKernel 𝕜 E) := by95  apply Set.ext96  intro J97  constructor98  · rintro ⟨I, hI⟩99    exact ⟨toGeometricSpectrum 𝕜 E I, hI⟩100  · rintro ⟨C, rfl⟩101    exact (geometricSpectrumToPrimitive 𝕜 E C).property102103/-- No primitive geometric point equals the whole original space. -/104theorem univ_notMem_primitiveGeometricSpectrumFamily :105    Set.univ ∉ primitiveGeometricSpectrumFamily 𝕜 E :=106  ClosureSpace.HullKernel.univ_notMem_componentKernelFamily _ _107108/-- The primitive geometric spectrum carries its own hull-kernel closure. -/109def primitiveGeometricSpectrumClosure : ClosureSpace (PrimitiveGeometricSpectrum 𝕜 E) :=110  ClosureSpace.HullKernel.componentKernelClosure (geometricStructureFamily 𝕜 E)111    (univ_notMem_geometricStructureFamily 𝕜 E)112113/-- The geometric spectrum has the closure pulled back along gamma. -/114def geometricSpectrumClosure : ClosureSpace (GeometricSpectrum 𝕜 E) :=115  (primitiveGeometricSpectrumClosure 𝕜 E).induced (geometricSpectrumToPrimitive 𝕜 E)116117/-- The primitive closure formula, including the empty selection. -/118theorem primitiveGeometricSpectrumClosure_closure (T : Set (PrimitiveGeometricSpectrum 𝕜 E)) :119    (primitiveGeometricSpectrumClosure 𝕜 E).closure T =120      {J | ∀ x : E, (∀ J' : PrimitiveGeometricSpectrum 𝕜 E, J' ∈ T → x ∈ J'.val) →121        x ∈ J.val} := rfl122123/-- Theorem 4.7's exact pullback formula. -/124theorem geometricSpectrumClosure_closure_preimage (S : Set (GeometricSpectrum 𝕜 E)) :125    (geometricSpectrumClosure 𝕜 E).closure S =126      geometricSpectrumToPrimitive 𝕜 E ⁻¹'127        (primitiveGeometricSpectrumClosure 𝕜 E).closure128          (geometricSpectrumToPrimitive 𝕜 E '' S) := rfl129130/-- The geometric closure formula stated directly in terms of `J_C`. -/131theorem geometricSpectrumClosure_closure (S : Set (GeometricSpectrum 𝕜 E)) :132    (geometricSpectrumClosure 𝕜 E).closure S =133      {C | ∀ x : E, (∀ D : GeometricSpectrum 𝕜 E, D ∈ S →134        x ∈ geometricSpectrumKernel 𝕜 E D) → x ∈ geometricSpectrumKernel 𝕜 E C} := by135  apply Set.ext136  intro C137  change (∀ x : E, (∀ J : PrimitiveGeometricSpectrum 𝕜 E,138    J ∈ geometricSpectrumToPrimitive 𝕜 E '' S → x ∈ J.val) →139      x ∈ geometricSpectrumKernel 𝕜 E C) ↔ _140  constructor141  · intro h x hx142    apply h x143    rintro J ⟨D, hD, rfl⟩144    exact hx D hD145  · intro h x hx146    exact h x (fun D hD => hx (geometricSpectrumToPrimitive 𝕜 E D) ⟨D, hD, rfl⟩)147148/-- Gamma is continuous between the two explicit closure spaces. -/149theorem continuous_geometricSpectrumToPrimitive :150    (geometricSpectrumClosure 𝕜 E).Continuous (primitiveGeometricSpectrumClosure 𝕜 E)151      (geometricSpectrumToPrimitive 𝕜 E) := ClosureSpace.continuous_induced _ _152153/-- Surjectivity also gives the exact image-of-closure formula. -/154theorem image_geometricSpectrumToPrimitive_closure (S : Set (GeometricSpectrum 𝕜 E)) :155    geometricSpectrumToPrimitive 𝕜 E '' (geometricSpectrumClosure 𝕜 E).closure S =156      (primitiveGeometricSpectrumClosure 𝕜 E).closure (geometricSpectrumToPrimitive 𝕜 E '' S) :=157  ClosureSpace.image_induced_closure _ _ (geometricSpectrumToPrimitive_surjective 𝕜 E) S158159/-- The primitive spectrum is T0 by its actual hull-kernel realization. -/160theorem isT0_primitiveGeometricSpectrumClosure : (primitiveGeometricSpectrumClosure 𝕜 E).IsT0 :=161  ClosureSpace.HullKernel.isT0_space (primitiveGeometricSpectrumFamily 𝕜 E)162    (univ_notMem_primitiveGeometricSpectrumFamily 𝕜 E)163164/-- The geometric spectrum is T0 exactly when gamma is injective, not just surjective. -/165theorem isT0_geometricSpectrumClosure_iff :166    (geometricSpectrumClosure 𝕜 E).IsT0 ↔ Function.Injective (geometricSpectrumToPrimitive 𝕜 E) :=167  ClosureSpace.isT0_induced_iff _ (isT0_primitiveGeometricSpectrumClosure 𝕜 E) _168169/-- In the zero-space case, the component family remains empty. -/170theorem geometricSpectrumFamily_eq_empty_of_subsingleton [Subsingleton E] :171    geometricSpectrumFamily 𝕜 E = ∅ := by172  letI := isEmpty_geometricStructureSpace_of_subsingleton 𝕜 E173  apply Set.eq_empty_iff_forall_notMem.mpr174  rintro C ⟨I, _⟩175  exact (Set.eq_empty_iff_forall_notMem.mp176    (geometricStructureFamily_eq_empty_of_subsingleton 𝕜 E)) I.val I.property177178/-- Empty geometric-structure spaces yield no primitive geometric point. -/179theorem primitiveGeometricSpectrumFamily_eq_empty_of_subsingleton [Subsingleton E] :180    primitiveGeometricSpectrumFamily 𝕜 E = ∅ := by181  letI := isEmpty_geometricStructureSpace_of_subsingleton 𝕜 E182  apply Set.eq_empty_iff_forall_notMem.mpr183  rintro J ⟨I, _⟩184  exact (Set.eq_empty_iff_forall_notMem.mp185    (geometricStructureFamily_eq_empty_of_subsingleton 𝕜 E)) I.val I.property186187/-- The type-level zero-space statement for the geometric spectrum. -/188theorem isEmpty_geometricSpectrum_of_subsingleton [Subsingleton E] :189    IsEmpty (GeometricSpectrum 𝕜 E) := by190  refine ⟨fun C => ?_⟩191  exact (Set.eq_empty_iff_forall_notMem.mp192    (geometricSpectrumFamily_eq_empty_of_subsingleton 𝕜 E)) C.val C.property193194/-- The type-level zero-space statement for the primitive geometric spectrum. -/195theorem isEmpty_primitiveGeometricSpectrum_of_subsingleton [Subsingleton E] :196    IsEmpty (PrimitiveGeometricSpectrum 𝕜 E) := by197  refine ⟨fun J => ?_⟩198  exact (Set.eq_empty_iff_forall_notMem.mp199    (primitiveGeometricSpectrumFamily_eq_empty_of_subsingleton 𝕜 E)) J.val J.property200201end NormedSpace