MathlibAnnex/Topology/ClosureSpace/Maps.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.Basic9public import Mathlib.Data.Set.Finite.Basic1011/-!12# Maps of closure spaces1314Continuity and finite continuity are distinct predicates. A continuous finite15homeomorphism has no assumption of ordinary continuity for its inverse.16-/1718@[expose] public section1920set_option autoImplicit false2122universe u v w2324namespace ClosureSpace2526variable {α : Type u} {β : Type v} {γ : Type w}2728/-- Preservation of closure in the forward direction. -/29def Continuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop :=30  ∀ s : Set α, f '' c.closure s ⊆ d.closure (f '' s)3132/-- Preservation of closure, tested only on finite subsets of the domain. -/33def FinitelyContinuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop :=34  ∀ s : Set α, s.Finite → f '' c.closure s ⊆ d.closure (f '' s)3536theorem continuous_id (c : ClosureSpace α) : c.Continuous c id := by37  intro s x hx38  rcases hx with ⟨y, hy, rfl⟩39  change y ∈ c.closure (id '' s)40  rw [Set.image_id]41  exact hy4243theorem Continuous.comp {c : ClosureSpace α} {d : ClosureSpace β} {e : ClosureSpace γ}44    {f : α → β} {g : β → γ} (hg : d.Continuous e g) (hf : c.Continuous d f) :45    c.Continuous e (g ∘ f) := by46  intro s z hz47  rcases hz with ⟨x, hx, rfl⟩48  have hfx : f x ∈ d.closure (f '' s) := hf s ⟨x, hx, rfl⟩49  have hgfx := hg (f '' s) ⟨f x, hfx, rfl⟩50  simpa only [Set.image_image, Function.comp_def] using hgfx5152theorem Continuous.finitelyContinuous {c : ClosureSpace α} {d : ClosureSpace β}53    {f : α → β} (hf : c.Continuous d f) : c.FinitelyContinuous d f :=54  fun s _ => hf s5556theorem FinitelyContinuous.comp {c : ClosureSpace α} {d : ClosureSpace β}57    {e : ClosureSpace γ} {f : α → β} {g : β → γ}58    (hg : d.FinitelyContinuous e g) (hf : c.FinitelyContinuous d f) :59    c.FinitelyContinuous e (g ∘ f) := by60  intro s hs z hz61  rcases hz with ⟨x, hx, rfl⟩62  have hfx := hf s hs ⟨x, hx, rfl⟩63  have hgfx := hg (f '' s) (hs.image f) ⟨f x, hfx, rfl⟩64  simpa only [Set.image_image, Function.comp_def] using hgfx6566/-- Closed-preimage characterization, valid without finite-union preservation. -/67theorem continuous_iff_isClosed_preimage (c : ClosureSpace α) (d : ClosureSpace β)68    (f : α → β) : c.Continuous d f ↔69      ∀ t : Set β, d.IsClosed t → c.IsClosed (f ⁻¹' t) := by70  constructor71  · intro hf t ht72    apply (c.isClosed_iff_closure_subset _).273    intro x hx74    exact d.closure_min (Set.image_preimage_subset f t) ht75      (hf (f ⁻¹' t) ⟨x, hx, rfl⟩)76  · intro h s y hy77    rcases hy with ⟨x, hx, rfl⟩78    have ht := h (d.closure (f '' s)) (d.isClosed_closure (f '' s))79    apply c.closure_min (t := f ⁻¹' d.closure (f '' s)) ?_ ht hx80    intro a ha81    exact d.subset_closure (f '' s) ⟨a, ha, rfl⟩8283/-- A bijection that is continuous in both directions. -/84structure Homeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where85  continuous_toFun : c.Continuous d toFun86  continuous_invFun : d.Continuous c invFun8788namespace Homeomorph8990variable {c : ClosureSpace α} {d : ClosureSpace β} {e : ClosureSpace γ}9192/-- Reverse a homeomorphism. -/93def symm (h : Homeomorph c d) : Homeomorph d c where94  toEquiv := h.toEquiv.symm95  continuous_toFun := h.continuous_invFun96  continuous_invFun := h.continuous_toFun9798/-- The identity homeomorphism. -/99def refl (c : ClosureSpace α) : Homeomorph c c where100  toEquiv := Equiv.refl α101  continuous_toFun := continuous_id c102  continuous_invFun := continuous_id c103104/-- Compose homeomorphisms. -/105def trans (h : Homeomorph c d) (k : Homeomorph d e) : Homeomorph c e where106  toEquiv := h.toEquiv.trans k.toEquiv107  continuous_toFun := k.continuous_toFun.comp h.continuous_toFun108  continuous_invFun := h.continuous_invFun.comp k.continuous_invFun109110/-- A homeomorphism transports the full closure exactly. -/111theorem image_closure (h : Homeomorph c d) (s : Set α) :112    h.toEquiv '' c.closure s = d.closure (h.toEquiv '' s) := by113  apply Set.Subset.antisymm (h.continuous_toFun s)114  intro y hy115  have hx := h.continuous_invFun (h.toEquiv '' s) ⟨y, hy, rfl⟩116  change h.toEquiv.symm y ∈ c.closure (h.toEquiv.symm '' (h.toEquiv '' s)) at hx117  have hs : h.toEquiv.symm '' (h.toEquiv '' s) = s := by118    apply Set.ext119    intro x120    simp only [Set.mem_image]121    constructor122    · rintro ⟨z, ⟨a, ha, rfl⟩, hx⟩123      have hx' : a = x := (h.toEquiv.symm_apply_apply a).symm.trans hx124      exact hx' ▸ ha125    · intro hx126      exact ⟨h.toEquiv x, ⟨x, hx, rfl⟩, h.toEquiv.symm_apply_apply x⟩127  rw [hs] at hx128  exact ⟨h.toEquiv.symm y, hx, h.toEquiv.apply_symm_apply y⟩129130/-- A bijection commuting with closure is a homeomorphism. -/131def ofImageClosure (c : ClosureSpace α) (d : ClosureSpace β) (e : α ≃ β)132    (he : ∀ s : Set α, e '' c.closure s = d.closure (e '' s)) : Homeomorph c d where133  toEquiv := e134  continuous_toFun s := (he s).subset135  continuous_invFun := by136    intro t x hx137    rcases hx with ⟨y, hy, rfl⟩138    have ht : e '' (e.symm '' t) = t := by139      apply Set.ext140      intro z141      constructor142      · rintro ⟨a, ⟨b, hb, rfl⟩, hz⟩143        have hz' : b = z := (e.apply_symm_apply b).symm.trans hz144        exact hz' ▸ hb145      · intro hz146        exact ⟨e.symm z, ⟨z, hz, rfl⟩, e.apply_symm_apply z⟩147    have hy' : y ∈ e '' c.closure (e.symm '' t) := by148      rw [he, ht]149      exact hy150    rcases hy' with ⟨a, ha, rfl⟩151    change e.symm (e a) ∈ c.closure (e.symm '' t)152    simpa only [Equiv.symm_apply_apply] using ha153154end Homeomorph155156/-- A bijection with finite continuity in both directions. -/157structure FiniteHomeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where158  finitelyContinuous_toFun : c.FinitelyContinuous d toFun159  finitelyContinuous_invFun : d.FinitelyContinuous c invFun160161/-- A finite homeomorphism whose forward map is continuous.162Ordinary continuity of the inverse is deliberately not a field. -/163structure ContinuousFiniteHomeomorph (c : ClosureSpace α) (d : ClosureSpace β)164    extends FiniteHomeomorph c d where165  continuous_toFun : c.Continuous d toFun166167/-- Forget full continuity and retain finite continuity. -/168def Homeomorph.toFiniteHomeomorph {c : ClosureSpace α} {d : ClosureSpace β}169    (h : Homeomorph c d) : FiniteHomeomorph c d where170  toEquiv := h.toEquiv171  finitelyContinuous_toFun := h.continuous_toFun.finitelyContinuous172  finitelyContinuous_invFun := h.continuous_invFun.finitelyContinuous173174/-- Reverse a finite homeomorphism. -/175def FiniteHomeomorph.symm {c : ClosureSpace α} {d : ClosureSpace β}176    (h : FiniteHomeomorph c d) : FiniteHomeomorph d c where177  toEquiv := h.toEquiv.symm178  finitelyContinuous_toFun := h.finitelyContinuous_invFun179  finitelyContinuous_invFun := h.finitelyContinuous_toFun180181end ClosureSpace