MathlibAnnex/Topology/ClosureSpace/HullKernelMap.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.HullKernel910/-!11# Transport of hull-kernel spaces1213A pair of equivalences preserving incidence between points and sets transports14hull-kernel closure. Closure preservation is proved, not included in the input.15-/1617@[expose] public section1819set_option autoImplicit false2021universe u v2223namespace ClosureSpace24namespace HullKernel2526variable {X : Type u} {Y : Type v} {F : Set (Set X)} {G : Set (Set Y)}2728/-- Incidence-preserving equivalences transport intersections of selected members. -/29theorem image_kernel (e : X ≃ Y) (φ : F ≃ G)30    (hmem : ∀ (I : F) (x : X), e x ∈ (φ I).val ↔ x ∈ I.val) (S : Set F) :31    e '' kernel F S = kernel G (φ '' S) := by32  apply Set.ext33  intro y34  constructor35  · rintro ⟨x, hx, rfl⟩36    rintro J ⟨I, hI, rfl⟩37    exact (hmem I x).2 (hx I hI)38  · intro hy39    refine ⟨e.symm y, ?_, e.apply_symm_apply y⟩40    intro I hI41    apply (hmem I (e.symm y)).142    simpa only [Equiv.apply_symm_apply] using hy (φ I) ⟨I, hI, rfl⟩4344/-- Incidence-preserving equivalences commute with hull-kernel closure. -/45theorem image_closure (hF : Set.univ ∉ F) (hG : Set.univ ∉ G)46    (e : X ≃ Y) (φ : F ≃ G)47    (hmem : ∀ (I : F) (x : X), e x ∈ (φ I).val ↔ x ∈ I.val) (S : Set F) :48    φ '' (space F hF).closure S = (space G hG).closure (φ '' S) := by49  apply Set.ext50  intro J51  constructor52  · rintro ⟨I, hI, rfl⟩53    intro y hy54    have hy' : y ∈ e '' kernel F S := by55      rw [image_kernel e φ hmem]56      exact hy57    rcases hy' with ⟨x, hx, rfl⟩58    exact (hmem I x).2 (hI hx)59  · intro hJ60    refine ⟨φ.symm J, ?_, φ.apply_symm_apply J⟩61    intro x hx62    apply (hmem (φ.symm J) x).163    have hx' : e x ∈ kernel G (φ '' S) := by64      rw [← image_kernel e φ hmem]65      exact ⟨x, hx, rfl⟩66    simpa only [Equiv.apply_symm_apply] using hJ hx'6768/-- The induced homeomorphism of arbitrary hull-kernel families. -/69def homeomorphOfMemIff (hF : Set.univ ∉ F) (hG : Set.univ ∉ G)70    (e : X ≃ Y) (φ : F ≃ G)71    (hmem : ∀ (I : F) (x : X), e x ∈ (φ I).val ↔ x ∈ I.val) :72    Homeomorph (space F hF) (space G hG) :=73  Homeomorph.ofImageClosure _ _ φ (image_closure hF hG e φ hmem)7475end HullKernel76end ClosureSpace