MathlibAnnex/Topology/ClosureSpace/Components.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.Maps9public import Mathlib.Logic.Relation1011/-!12# Components generated by nonclosed pairs1314The equivalence closure is the existing `Relation.EqvGen`. The generating relation15is symmetric; hence it describes exactly finite chains of nonclosed pairs, with16identity steps allowed. The component and its closure are kept separate.17-/1819@[expose] public section2021set_option autoImplicit false2223universe u v2425namespace ClosureSpace2627variable {α : Type u} {β : Type v}2829/-- Equality or a nonclosed two-point set. -/30def Linked (c : ClosureSpace α) (x y : α) : Prop := x = y ∨ ¬ c.IsClosed {x, y}3132theorem linked_refl (c : ClosureSpace α) (x : α) : c.Linked x x := Or.inl rfl3334theorem linked_symm (c : ClosureSpace α) {x y : α} (h : c.Linked x y) :35    c.Linked y x := by36  rcases h with h | h37  · exact Or.inl h.symm38  · apply Or.inr39    intro hyx40    apply h41    have hset : ({x, y} : Set α) = {y, x} := by42      apply Set.ext43      intro z44      simp only [Set.mem_insert_iff, Set.mem_singleton_iff, or_comm]45    rw [hset]46    exact hyx4748/-- The equivalence relation generated by linked pairs. -/49def componentSetoid (c : ClosureSpace α) : Setoid α := Relation.EqvGen.setoid c.Linked5051/-- Belonging to the same finite-chain component. -/52abbrev Related (c : ClosureSpace α) (x y : α) : Prop := (c.componentSetoid).r x y5354theorem related_refl (c : ClosureSpace α) (x : α) : c.Related x x :=55  c.componentSetoid.iseqv.refl x5657theorem related_symm (c : ClosureSpace α) {x y : α} (h : c.Related x y) :58    c.Related y x := c.componentSetoid.iseqv.symm h5960theorem related_trans (c : ClosureSpace α) {x y z : α}61    (hxy : c.Related x y) (hyz : c.Related y z) : c.Related x z :=62  c.componentSetoid.iseqv.trans hxy hyz6364theorem related_of_linked (c : ClosureSpace α) {x y : α} (h : c.Linked x y) :65    c.Related x y := Relation.EqvGen.rel x y h6667/-- The equivalence class as an ambient subset. -/68def component (c : ClosureSpace α) (x : α) : Set α := {y | c.Related x y}6970theorem mem_component (c : ClosureSpace α) (x : α) : x ∈ c.component x :=71  c.related_refl x7273theorem component_eq_of_related (c : ClosureSpace α) {x y : α} (h : c.Related x y) :74    c.component x = c.component y := by75  apply Set.ext76  intro z77  exact ⟨fun hxz => c.related_trans (c.related_symm h) hxz,78    fun hyz => c.related_trans h hyz⟩7980/-- The closure of a component, not the component itself. -/81def componentClosure (c : ClosureSpace α) (x : α) : Set α := c.closure (c.component x)8283theorem mem_componentClosure (c : ClosureSpace α) (x : α) : x ∈ c.componentClosure x :=84  c.subset_closure (c.component x) (c.mem_component x)8586/-- Finite continuity preserves linked pairs when the map is injective.87The injectivity assumption is essential. -/88theorem FinitelyContinuous.linked {c : ClosureSpace α} {d : ClosureSpace β}89    {f : α → β} (hf : c.FinitelyContinuous d f) (hinj : Function.Injective f)90    {x y : α} (hxy : c.Linked x y) : d.Linked (f x) (f y) := by91  rcases hxy with hxy | hxy92  · exact Or.inl (congrArg f hxy)93  · apply Or.inr94    intro hclosed95    apply hxy96    apply (c.isClosed_iff_closure_subset {x, y}).297    intro z hz98    have hz' := hf {x, y} ((Set.finite_singleton y).insert x) ⟨z, hz, rfl⟩99    rw [Set.image_pair, (d.isClosed_iff {f x, f y}).1 hclosed] at hz'100    rcases Set.mem_insert_iff.1 hz' with hx | hy101    · exact Set.mem_insert_iff.2 (Or.inl (hinj hx))102    · exact Set.mem_insert_iff.2103        (Or.inr (Set.mem_singleton_iff.2 (hinj (Set.mem_singleton_iff.1 hy))))104105/-- An injective finitely continuous map preserves the equivalence closure. -/106theorem FinitelyContinuous.related {c : ClosureSpace α} {d : ClosureSpace β}107    {f : α → β} (hf : c.FinitelyContinuous d f) (hinj : Function.Injective f)108    {x y : α} (hxy : c.Related x y) : d.Related (f x) (f y) := by109  change Relation.EqvGen c.Linked x y at hxy110  change Relation.EqvGen d.Linked (f x) (f y)111  induction hxy with112  | rel a b hab => exact Relation.EqvGen.rel _ _ (hf.linked hinj hab)113  | refl a => exact Relation.EqvGen.refl _114  | symm a b _ ih => exact Relation.EqvGen.symm _ _ ih115  | trans a b z _ _ ih₁ ih₂ => exact Relation.EqvGen.trans _ _ _ ih₁ ih₂116117theorem FiniteHomeomorph.related_iff {c : ClosureSpace α} {d : ClosureSpace β}118    (h : FiniteHomeomorph c d) (x y : α) :119    d.Related (h.toEquiv x) (h.toEquiv y) ↔ c.Related x y := by120  constructor121  · intro hxy122    have h' := h.finitelyContinuous_invFun.related h.toEquiv.symm.injective hxy123    change c.Related (h.toEquiv.symm (h.toEquiv x)) (h.toEquiv.symm (h.toEquiv y)) at h'124    simpa only [Equiv.symm_apply_apply] using h'125  · exact h.finitelyContinuous_toFun.related h.toEquiv.injective126127theorem FiniteHomeomorph.image_component {c : ClosureSpace α} {d : ClosureSpace β}128    (h : FiniteHomeomorph c d) (x : α) :129    h.toEquiv '' c.component x = d.component (h.toEquiv x) := by130  apply Set.ext131  intro y132  constructor133  · rintro ⟨z, hz, rfl⟩134    exact (h.related_iff x z).2 hz135  · intro hy136    refine ⟨h.toEquiv.symm y, ?_, h.toEquiv.apply_symm_apply y⟩137    apply (h.related_iff x (h.toEquiv.symm y)).1138    change d.Related (h.toEquiv x) y at hy139    simpa only [Equiv.apply_symm_apply] using hy140141theorem Homeomorph.image_componentClosure {c : ClosureSpace α} {d : ClosureSpace β}142    (h : Homeomorph c d) (x : α) :143    h.toEquiv '' c.componentClosure x = d.componentClosure (h.toEquiv x) := by144  change h.toEquiv '' c.closure (c.component x) =145    d.closure (d.component (h.toEquiv x))146  rw [h.image_closure]147  change d.closure (h.toFiniteHomeomorph.toEquiv '' c.component x) =148    d.closure (d.component (h.toFiniteHomeomorph.toEquiv x))149  rw [h.toFiniteHomeomorph.image_component]150151end ClosureSpace