MathlibAnnex/Topology/ClosureSpace/HullKernel.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.Induced910/-!11# Hull-kernel closure for arbitrary families of sets1213No linear, normed, algebraic, or ideal structure is assumed. The kernel is an14intersection of members, including the empty intersection `univ`. Excluding15`univ` from the family is precisely the condition needed for empty preservation.16-/1718@[expose] public section1920set_option autoImplicit false2122universe u2324namespace ClosureSpace25namespace HullKernel2627variable {X : Type u}2829/-- Intersect the members selected by a set of points of the family subtype. -/30def kernel (F : Set (Set X)) (s : Set F) : Set X :=31  {x | ∀ I : F, I ∈ s → x ∈ I.val}3233/-- Select all members containing a given subset of the ambient set. -/34def hull (F : Set (Set X)) (a : Set X) : Set F := {I | a ⊆ I.val}3536@[simp]37theorem mem_kernel (F : Set (Set X)) (s : Set F) (x : X) :38    x ∈ kernel F s ↔ ∀ I : F, I ∈ s → x ∈ I.val := Iff.rfl3940@[simp]41theorem mem_hull (F : Set (Set X)) (a : Set X) (I : F) :42    I ∈ hull F a ↔ a ⊆ I.val := Iff.rfl4344@[simp]45theorem kernel_empty (F : Set (Set X)) : kernel F ∅ = Set.univ := by46  apply Set.ext47  intro x48  simp only [mem_kernel, Set.mem_empty_iff_false, false_implies, implies_true,49    Set.mem_univ]5051theorem kernel_antitone (F : Set (Set X)) {s t : Set F} (hst : s ⊆ t) :52    kernel F t ⊆ kernel F s := fun _ hx I hI => hx I (hst hI)5354theorem hull_antitone (F : Set (Set X)) {a b : Set X} (hab : a ⊆ b) :55    hull F b ⊆ hull F a := fun _ hI => hab.trans hI5657theorem subset_hull_kernel (F : Set (Set X)) (s : Set F) : s ⊆ hull F (kernel F s) :=58  fun I hI _ hx => hx I hI5960/-- The intersection does not change on passing to the hull-kernel closure. -/61@[simp]62theorem kernel_hull_kernel (F : Set (Set X)) (s : Set F) :63    kernel F (hull F (kernel F s)) = kernel F s := by64  apply Set.Subset.antisymm (kernel_antitone F (subset_hull_kernel F s))65  intro x hx I hI66  exact hI hx6768/-- The generic hull-kernel closure space. -/69def space (F : Set (Set X)) (hF : Set.univ ∉ F) : ClosureSpace F where70  toClosureOperator := ClosureOperator.mk'71    (fun s => hull F (kernel F s))72    (by73      intro s t hst74      exact hull_antitone F (kernel_antitone F hst))75    (subset_hull_kernel F)76    (by77      intro s78      rw [kernel_hull_kernel])79  map_empty' := by80    change hull F (kernel F ∅) = ∅81    rw [kernel_empty]82    apply Set.eq_empty_iff_forall_notMem.283    intro I hI84    have hval : I.val = Set.univ := Set.Subset.antisymm (Set.subset_univ _) hI85    exact hF (hval ▸ I.property)8687@[simp]88theorem space_closure (F : Set (Set X)) (hF : Set.univ ∉ F) (s : Set F) :89    (space F hF).closure s = hull F (kernel F s) := rfl9091/-- Hull-kernel closure is determined exactly by the intersection of the selected members. -/92theorem closure_eq_iff_kernel_eq (F : Set (Set X)) (hF : Set.univ ∉ F)93    (s t : Set F) :94    (space F hF).closure s = (space F hF).closure t ↔ kernel F s = kernel F t := by95  constructor96  · intro h97    have hk := congrArg (kernel F) h98    simpa only [space_closure, kernel_hull_kernel] using hk99  · intro h100    change hull F (kernel F s) = hull F (kernel F t)101    rw [h]102103/-- A hull-kernel space is T0, even for a completely arbitrary family of subsets. -/104theorem isT0_space (F : Set (Set X)) (hF : Set.univ ∉ F) : (space F hF).IsT0 := by105  intro I J hIJ hJI106  apply Subtype.ext107  apply Set.Subset.antisymm108  · intro x hx109    apply hJI110    intro K hK111    have hK' : K = I := Set.mem_singleton_iff.1 hK112    subst K113    exact hx114  · intro x hx115    apply hIJ116    intro K hK117    have hK' : K = J := Set.mem_singleton_iff.1 hK118    subst K119    exact hx120121/-- An antichain of subsets gives a T1 hull-kernel space. -/122theorem isT1_space_of_antichain (F : Set (Set X)) (hF : Set.univ ∉ F)123    (hanti : ∀ I J : F, I.val ⊆ J.val → I = J) : (space F hF).IsT1 := by124  intro I125  apply ((space F hF).isClosed_iff_closure_subset {I}).2126  intro J hJ127  apply Set.mem_singleton_iff.2128  apply (hanti I J ?_).symm129  intro x hx130  apply hJ131  intro K hK132  have hK' : K = I := Set.mem_singleton_iff.1 hK133  subst K134  exact hx135136end HullKernel137end ClosureSpace