MathlibAnnex/Topology/ClosureSpace/HullKernelTransforms.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.Topology.ClosureSpace.ComponentKernel910/-!11# Hull-kernel models for the G- and P-transforms1213The P-transform's points are closed components in the original point set;14component-kernel points are intersections in the ambient set. Their bijection15preserves closure. The G-model keeps actual component subsets, and pulls back16component-kernel closure along their intersection map.17-/1819@[expose] public section2021set_option autoImplicit false2223universe u2425namespace ClosureSpace26namespace HullKernel2728variable {X : Type u} (F : Set (Set X)) (hF : Set.univ ∉ F)2930/-- The preimages of corresponding selections agree under the P-point equivalence. -/31theorem preimage_toComponentKernelPoint_image (T : Set (space F hF).PPoint) :32    toComponentKernelPoint F hF ⁻¹' (pPointEquivComponentKernelPoint F hF '' T) =33      (space F hF).toPPoint ⁻¹' T := by34  apply Set.ext35  intro I36  change toComponentKernelPoint F hF I ∈ (pPointEquivComponentKernelPoint F hF '' T) ↔ _37  rw [← pPointEquivComponentKernelPoint_toPPoint F hF I]38  constructor39  · rintro ⟨p, hp, heq⟩40    have heq' := (pPointEquivComponentKernelPoint F hF).injective heq41    change (space F hF).toPPoint I ∈ T42    rw [← heq']43    exact hp44  · intro hI45    exact ⟨(space F hF).toPPoint I, hI, rfl⟩4647/-- Closure membership is preserved in both directions, not merely on singletons. -/48theorem pPointEquivComponentKernelPoint_mem_closure_iff49    (T : Set (space F hF).PPoint) (p : (space F hF).PPoint) :50    pPointEquivComponentKernelPoint F hF p ∈51        (componentKernelClosure F hF).closure (pPointEquivComponentKernelPoint F hF '' T) ↔52      p ∈ (space F hF).pTransform.closure T := by53  rcases p with ⟨p, I, rfl⟩54  change pPointEquivComponentKernelPoint F hF ((space F hF).toPPoint I) ∈ _ ↔55    (space F hF).componentClosure I ⊆56      (space F hF).closure ((space F hF).toPPoint ⁻¹' T)57  rw [pPointEquivComponentKernelPoint_toPPoint, mem_componentKernelClosure_iff,58    preimage_toComponentKernelPoint_image]5960/-- Exact preservation of the complete P-closure formula. -/61theorem image_pPointEquivComponentKernelPoint_closure (T : Set (space F hF).PPoint) :62    pPointEquivComponentKernelPoint F hF '' (space F hF).pTransform.closure T =63      (componentKernelClosure F hF).closure (pPointEquivComponentKernelPoint F hF '' T) := by64  apply Set.ext65  intro J66  constructor67  · rintro ⟨p, hp, rfl⟩68    exact (pPointEquivComponentKernelPoint_mem_closure_iff F hF T p).mpr hp69  · intro hJ70    obtain ⟨p, rfl⟩ := (pPointEquivComponentKernelPoint F hF).surjective J71    exact ⟨p, (pPointEquivComponentKernelPoint_mem_closure_iff F hF T p).mp hJ, rfl⟩7273/-- The P-transform is homeomorphic to the family of component intersections. -/74def pPointHomeomorphComponentKernelPoint :75    Homeomorph (space F hF).pTransform (componentKernelClosure F hF) :=76  Homeomorph.ofImageClosure _ _ (pPointEquivComponentKernelPoint F hF)77    (image_pPointEquivComponentKernelPoint_closure F hF)7879/-- Intersect an actual component subset to obtain a component-kernel point. -/80def componentPointToComponentKernelPoint (C : (space F hF).ComponentPoint) :81    ComponentKernelPoint F hF :=82  ⟨kernel F C.val, by83    obtain ⟨I, hI⟩ := C.property84    exact ⟨I, congrArg (kernel F) hI⟩⟩8586@[simp]87theorem componentPointToComponentKernelPoint_toComponentPoint (I : F) :88    componentPointToComponentKernelPoint F hF ((space F hF).toComponentPoint I) =89      toComponentKernelPoint F hF I := rfl9091theorem componentPointToComponentKernelPoint_surjective :92    Function.Surjective (componentPointToComponentKernelPoint F hF) := by93  intro J94  obtain ⟨I, rfl⟩ := toComponentKernelPoint_surjective F hF J95  exact ⟨(space F hF).toComponentPoint I, rfl⟩9697/-- The concrete component model of the G-transform has pullback closure. -/98def componentPointClosure : ClosureSpace (space F hF).ComponentPoint :=99  (componentKernelClosure F hF).induced (componentPointToComponentKernelPoint F hF)100101/-- Commutativity of the quotient/component/intersection square. -/102theorem componentPointToComponentKernelPoint_gPointEquivComponentPoint103    (q : (space F hF).GPoint) :104    componentPointToComponentKernelPoint F hF ((space F hF).gPointEquivComponentPoint q) =105      pPointEquivComponentKernelPoint F hF ((space F hF).delta q) := by106  refine Quotient.inductionOn q ?_107  intro I108  exact (pPointEquivComponentKernelPoint_toPPoint F hF I).symm109110/-- Naturality on image sets, with no injectivity claim for the intersection map. -/111theorem image_componentPointToComponentKernelPoint_gPointEquivComponentPoint112    (S : Set (space F hF).GPoint) :113    componentPointToComponentKernelPoint F hF '' ((space F hF).gPointEquivComponentPoint '' S) =114      pPointEquivComponentKernelPoint F hF '' ((space F hF).delta '' S) := by115  apply Set.ext116  intro J117  constructor118  · rintro ⟨C, ⟨q, hq, rfl⟩, hJ⟩119    exact ⟨(space F hF).delta q, ⟨q, hq, rfl⟩,120      (componentPointToComponentKernelPoint_gPointEquivComponentPoint F hF q).symm.trans hJ⟩121  · rintro ⟨p, ⟨q, hq, rfl⟩, hJ⟩122    exact ⟨(space F hF).gPointEquivComponentPoint q, ⟨q, hq, rfl⟩,123      (componentPointToComponentKernelPoint_gPointEquivComponentPoint F hF q).trans hJ⟩124125/-- The G-closure comparison follows from the actual P-homeomorphism and126commuting maps, without identifying the two point types by definitional equality. -/127theorem gPointEquivComponentPoint_mem_closure_iff128    (S : Set (space F hF).GPoint) (q : (space F hF).GPoint) :129    (space F hF).gPointEquivComponentPoint q ∈130        (componentPointClosure F hF).closure ((space F hF).gPointEquivComponentPoint '' S) ↔131      q ∈ (space F hF).gTransform.closure S := by132  change componentPointToComponentKernelPoint F hF ((space F hF).gPointEquivComponentPoint q) ∈133      (componentKernelClosure F hF).closure134        (componentPointToComponentKernelPoint F hF ''135          ((space F hF).gPointEquivComponentPoint '' S)) ↔ _136  rw [componentPointToComponentKernelPoint_gPointEquivComponentPoint,137    image_componentPointToComponentKernelPoint_gPointEquivComponentPoint]138  exact pPointEquivComponentKernelPoint_mem_closure_iff F hF139    ((space F hF).delta '' S) ((space F hF).delta q)140141/-- Exact preservation of G-closure under the quotient-to-subset equivalence. -/142theorem image_gPointEquivComponentPoint_closure (S : Set (space F hF).GPoint) :143    (space F hF).gPointEquivComponentPoint '' (space F hF).gTransform.closure S =144      (componentPointClosure F hF).closure ((space F hF).gPointEquivComponentPoint '' S) := by145  apply Set.ext146  intro C147  constructor148  · rintro ⟨q, hq, rfl⟩149    exact (gPointEquivComponentPoint_mem_closure_iff F hF S q).mpr hq150  · intro hC151    obtain ⟨q, rfl⟩ := (space F hF).gPointEquivComponentPoint.surjective C152    exact ⟨q, (gPointEquivComponentPoint_mem_closure_iff F hF S q).mp hC, rfl⟩153154/-- The G-transform is homeomorphic to the concrete component-set model. -/155noncomputable def gPointHomeomorphComponentPoint :156    Homeomorph (space F hF).gTransform (componentPointClosure F hF) :=157  Homeomorph.ofImageClosure _ _ (space F hF).gPointEquivComponentPoint158    (image_gPointEquivComponentPoint_closure F hF)159160end HullKernel161end ClosureSpace