MathlibAnnex/Topology/ClosureSpace/Induced.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.Maps910/-!11# Induced and subspace closures1213The induced closure is `s ↦ f ⁻¹' d.closure (f '' s)`, with no assumption on `f`.14A subspace is the special case of a subtype inclusion. This is not a quotient topology.15-/1617@[expose] public section1819set_option autoImplicit false2021universe u v w2223namespace ClosureSpace2425variable {α : Type u} {β : Type v} {γ : Type w}2627/-- Pull back a closure space along any function. -/28def induced (d : ClosureSpace β) (f : α → β) : ClosureSpace α where29  toClosureOperator := ClosureOperator.mk'30    (fun s => f ⁻¹' d.closure (f '' s))31    (by32      intro s t h x hx33      exact d.closure_mono (Set.image_mono h) hx)34    (by35      intro s x hx36      exact d.subset_closure (f '' s) ⟨x, hx, rfl⟩)37    (by38      intro s x hx39      exact d.closure_min (Set.image_preimage_subset f _)40        (d.isClosed_closure (f '' s)) hx)41  map_empty' := by42    change f ⁻¹' d.closure (f '' ∅) = ∅43    rw [Set.image_empty, d.closure_empty, Set.preimage_empty]4445@[simp]46theorem induced_closure (d : ClosureSpace β) (f : α → β) (s : Set α) :47    (d.induced f).closure s = f ⁻¹' d.closure (f '' s) := rfl4849theorem continuous_induced (d : ClosureSpace β) (f : α → β) :50    (d.induced f).Continuous d f := by51  intro s y hy52  rcases hy with ⟨x, hx, rfl⟩53  exact hx5455/-- The universal property for a map into an induced closure space. -/56theorem continuous_induced_iff (c : ClosureSpace α) (d : ClosureSpace γ)57    (f : β → γ) (g : α → β) :58    c.Continuous (d.induced f) g ↔ c.Continuous d (f ∘ g) := by59  constructor60  · intro h61    exact (continuous_induced d f).comp h62  · intro h s y hy63    rcases hy with ⟨x, hx, rfl⟩64    change f (g x) ∈ d.closure (f '' (g '' s))65    simpa only [Set.image_image, Function.comp_def] using h s ⟨x, hx, rfl⟩6667theorem isTopologizable_induced {d : ClosureSpace β} (hd : d.IsTopologizable)68    (f : α → β) : (d.induced f).IsTopologizable := by69  intro s t70  change f ⁻¹' d.closure (f '' (s ∪ t)) =71    (f ⁻¹' d.closure (f '' s)) ∪ (f ⁻¹' d.closure (f '' t))72  rw [Set.image_union, hd, Set.preimage_union]7374theorem image_induced_closure (d : ClosureSpace β) (f : α → β)75    (hf : Function.Surjective f) (s : Set α) :76    f '' (d.induced f).closure s = d.closure (f '' s) := by77  apply Set.Subset.antisymm (continuous_induced d f s)78  intro y hy79  obtain ⟨x, rfl⟩ := hf y80  exact ⟨x, hy, rfl⟩8182/-- An equivalence is a homeomorphism from its induced closure space. -/83def homeomorphInduced (d : ClosureSpace β) (e : α ≃ β) :84    Homeomorph (d.induced e) d :=85  Homeomorph.ofImageClosure (d.induced e) d e86    (image_induced_closure d e e.surjective)8788/-- The closure on a subset, represented on its subtype. -/89def subspace (c : ClosureSpace α) (A : Set α) : ClosureSpace A :=90  c.induced (Subtype.val : A → α)9192@[simp]93theorem subspace_closure (c : ClosureSpace α) (A : Set α) (s : Set A) :94    (c.subspace A).closure s =95      (Subtype.val : A → α) ⁻¹' c.closure ((Subtype.val : A → α) '' s) := rfl9697/-- In ambient-set notation the subspace closure is intersection with the subset. -/98theorem image_subspace_closure (c : ClosureSpace α) (A : Set α) (s : Set A) :99    (Subtype.val : A → α) '' (c.subspace A).closure s =100      A ∩ c.closure ((Subtype.val : A → α) '' s) := by101  apply Set.ext102  intro x103  constructor104  · rintro ⟨y, hy, rfl⟩105    exact ⟨y.property, hy⟩106  · rintro ⟨hxA, hx⟩107    exact ⟨⟨x, hxA⟩, hx, rfl⟩108109theorem continuous_subtype_val (c : ClosureSpace α) (A : Set α) :110    (c.subspace A).Continuous c (Subtype.val : A → α) :=111  continuous_induced c Subtype.val112113/-- Pullback of a T0 closure is T0 precisely when the inducing map is injective. -/114theorem isT0_induced_iff (d : ClosureSpace β) (hd : d.IsT0) (f : α → β) :115    (d.induced f).IsT0 ↔ Function.Injective f := by116  constructor117  · intro h x y hxy118    apply h x y119    · exact d.subset_closure (f '' {y}) ⟨y, Set.mem_singleton y, hxy.symm⟩120    · exact d.subset_closure (f '' {x}) ⟨x, Set.mem_singleton x, hxy⟩121  · intro hf x y hxy hyx122    apply hf123    apply hd (f x) (f y)124    · change f x ∈ d.closure (f '' {y}) at hxy125      simpa only [Set.image_singleton] using hxy126    · change f y ∈ d.closure (f '' {x}) at hyx127      simpa only [Set.image_singleton] using hyx128129end ClosureSpace