MathlibAnnex/Topology/ClosureSpace/ComponentKernel.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.ComponentQuotient9public import MathlibAnnex.Topology.ClosureSpace.HullKernel1011/-!12# Intersections of components in a hull-kernel space1314For a family of proper subsets of an arbitrary set, intersect the members of15one component. These intersections are themselves actual subsets of the16ambient set. No submodule, ideal or other algebraic structure is assumed.1718The component-closure and intersection representations are different types;19the equivalence below uses intersection in one direction and hull in the other.20Empty indexed intersections retain their ordinary value `univ`.21-/2223@[expose] public section2425set_option autoImplicit false2627universe u2829namespace ClosureSpace30namespace HullKernel3132variable {X : Type u} (F : Set (Set X)) (hF : Set.univ ∉ F)3334/-- Intersect the members of the component of a hull-kernel point. -/35def componentKernel (I : F) : Set X := kernel F ((space F hF).component I)3637/-- Closing a selection of members does not change their intersection. -/38@[simp]39theorem kernel_space_closure (S : Set F) :40    kernel F ((space F hF).closure S) = kernel F S := kernel_hull_kernel F S4142theorem componentKernel_subset (I : F) : componentKernel F hF I ⊆ I.val :=43  fun _ hx => hx I ((space F hF).mem_component I)4445theorem componentKernel_ne_univ (I : F) : componentKernel F hF I ≠ Set.univ := by46  intro h47  have hI : I.val = Set.univ := Set.Subset.antisymm (Set.subset_univ _) (by48    rw [← h]49    exact componentKernel_subset F hF I)50  exact hF (hI ▸ I.property)5152theorem componentKernel_eq_of_related {I J : F} (h : (space F hF).Related I J) :53    componentKernel F hF I = componentKernel F hF J :=54  congrArg (kernel F) ((space F hF).component_eq_of_related h)5556/-- The closure of a component is the hull of its intersection. -/57theorem componentClosure_eq_hull_componentKernel (I : F) :58    (space F hF).componentClosure I = hull F (componentKernel F hF I) := rfl5960@[simp]61theorem kernel_componentClosure (I : F) :62    kernel F ((space F hF).componentClosure I) = componentKernel F hF I :=63  kernel_hull_kernel F ((space F hF).component I)6465/-- Equality of component closures is exactly equality of their intersections. -/66theorem componentClosure_eq_iff_componentKernel_eq (I J : F) :67    (space F hF).componentClosure I = (space F hF).componentClosure J ↔68      componentKernel F hF I = componentKernel F hF J :=69  closure_eq_iff_kernel_eq F hF ((space F hF).component I) ((space F hF).component J)7071/-- The family of component intersections. Repeated subsets give one member. -/72def componentKernelFamily : Set (Set X) := Set.range (componentKernel F hF)7374/-- Points of the component-intersection family, as subsets of the ambient set. -/75abbrev ComponentKernelPoint : Type u := {J : Set X // J ∈ componentKernelFamily F hF}7677/-- Send an original family member to its component intersection. -/78def toComponentKernelPoint (I : F) : ComponentKernelPoint F hF :=79  ⟨componentKernel F hF I, ⟨I, rfl⟩⟩8081theorem toComponentKernelPoint_surjective :82    Function.Surjective (toComponentKernelPoint F hF) := by83  rintro ⟨J, I, rfl⟩84  exact ⟨I, rfl⟩8586theorem univ_notMem_componentKernelFamily : Set.univ ∉ componentKernelFamily F hF := by87  rintro ⟨I, hI⟩88  exact componentKernel_ne_univ F hF I hI8990/-- Hull-kernel closure on the component-intersection family. -/91def componentKernelClosure : ClosureSpace (ComponentKernelPoint F hF) :=92  space (componentKernelFamily F hF) (univ_notMem_componentKernelFamily F hF)9394/-- Intersect the carrier of a P-point. -/95def pPointToComponentKernelPoint (p : (space F hF).PPoint) : ComponentKernelPoint F hF :=96  ⟨kernel F p.val, by97    obtain ⟨I, hI⟩ := p.property98    exact ⟨I, (kernel_componentClosure F hF I).symm.trans (congrArg (kernel F) hI)⟩⟩99100/-- Recover the closed component as the hull of its intersection. -/101def componentKernelPointToPPoint (J : ComponentKernelPoint F hF) : (space F hF).PPoint :=102  ⟨hull F J.val, by103    obtain ⟨I, hI⟩ := J.property104    exact ⟨I, (componentClosure_eq_hull_componentKernel F hF I).trans105      (congrArg (hull F) hI)⟩⟩106107/-- The intersection/hull equivalence; both inverse laws are actual set equalities. -/108def pPointEquivComponentKernelPoint : (space F hF).PPoint ≃ ComponentKernelPoint F hF where109  toFun := pPointToComponentKernelPoint F hF110  invFun := componentKernelPointToPPoint F hF111  left_inv p := by112    apply Subtype.ext113    change (space F hF).closure p.val = p.val114    exact ((space F hF).isClosed_iff p.val).mp ((space F hF).isClosed_pPoint p)115  right_inv J := by116    apply Subtype.ext117    change kernel F (hull F J.val) = J.val118    obtain ⟨I, hI⟩ := J.property119    rw [← hI]120    exact kernel_hull_kernel F ((space F hF).component I)121122@[simp]123theorem pPointEquivComponentKernelPoint_toPPoint (I : F) :124    pPointEquivComponentKernelPoint F hF ((space F hF).toPPoint I) =125      toComponentKernelPoint F hF I := Subtype.ext (kernel_componentClosure F hF I)126127/-- The kernel of a selected family of component intersections equals the128kernel of all original members whose component intersection was selected. -/129theorem kernel_componentKernelFamily (T : Set (ComponentKernelPoint F hF)) :130    kernel (componentKernelFamily F hF) T =131      kernel F (toComponentKernelPoint F hF ⁻¹' T) := by132  apply Set.ext133  intro x134  constructor135  · intro hx I hI136    exact componentKernel_subset F hF I (hx (toComponentKernelPoint F hF I) hI)137  · intro hx J hJ138    obtain ⟨I, hI⟩ := J.property139    change x ∈ J.val140    rw [← hI]141    intro I' hI'142    apply hx I'143    have heq : toComponentKernelPoint F hF I' = J := by144      apply Subtype.ext145      exact (componentKernel_eq_of_related F hF hI').symm.trans hI146    change toComponentKernelPoint F hF I' ∈ T147    rw [heq]148    exact hJ149150/-- Membership in the new hull-kernel closure expressed in the original space.151This is the component-intersection criterion, before any G/P identification. -/152theorem mem_componentKernelClosure_iff (I : F) (T : Set (ComponentKernelPoint F hF)) :153    toComponentKernelPoint F hF I ∈ (componentKernelClosure F hF).closure T ↔154      (space F hF).componentClosure I ⊆155        (space F hF).closure (toComponentKernelPoint F hF ⁻¹' T) := by156  change (kernel (componentKernelFamily F hF) T ⊆ componentKernel F hF I) ↔ _157  rw [kernel_componentKernelFamily F hF T]158  constructor159  · intro h160    exact hull_antitone F h161  · intro h162    have hk := kernel_antitone F h163    simpa only [componentKernel, componentClosure, space_closure, kernel_hull_kernel] using hk164165end HullKernel166end ClosureSpace