MathlibAnnex/Topology/ClosureSpace/ComponentQuotient.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.Transforms9public import Mathlib.Logic.Equiv.Defs1011/-!12# Components as sets and as quotient points1314The quotient `GPoint` and the family of actual component subsets are different15types. This file gives a bijection, retaining both directions and the exact16component-closure map. No nonemptiness or separation assumption is used.17-/1819@[expose] public section2021set_option autoImplicit false2223universe u2425namespace ClosureSpace2627variable {α : Type u}2829/-- Equality of component sets detects the generating equivalence relation. -/30theorem component_eq_iff_related (c : ClosureSpace α) (x y : α) :31    c.component x = c.component y ↔ c.Related x y := by32  constructor33  · intro h34    have hy := c.mem_component y35    rw [← h] at hy36    exact hy37  · exact c.component_eq_of_related3839/-- The family of actual component subsets. -/40def componentFamily (c : ClosureSpace α) : Set (Set α) := Set.range c.component4142/-- A component represented as a subset, rather than as a quotient element. -/43abbrev ComponentPoint (c : ClosureSpace α) : Type u :=44  {C : Set α // C ∈ c.componentFamily}4546/-- The component-set representative associated with an ambient point. -/47def toComponentPoint (c : ClosureSpace α) (x : α) : c.ComponentPoint :=48  ⟨c.component x, ⟨x, rfl⟩⟩4950@[simp]51theorem toComponentPoint_eq_iff (c : ClosureSpace α) (x y : α) :52    c.toComponentPoint x = c.toComponentPoint y ↔ c.Related x y := by53  constructor54  · intro h55    exact (c.component_eq_iff_related x y).mp (congrArg Subtype.val h)56  · intro h57    exact Subtype.ext (c.component_eq_of_related h)5859theorem toComponentPoint_surjective (c : ClosureSpace α) :60    Function.Surjective c.toComponentPoint := by61  rintro ⟨C, x, rfl⟩62  exact ⟨x, rfl⟩6364/-- Quotient elimination constructs the map to component subsets. -/65def gPointToComponentPoint (c : ClosureSpace α) : c.GPoint → c.ComponentPoint :=66  Quotient.lift c.toComponentPoint67    (fun x y h => (c.toComponentPoint_eq_iff x y).mpr h)6869@[simp]70theorem gPointToComponentPoint_toGPoint (c : ClosureSpace α) (x : α) :71    c.gPointToComponentPoint (c.toGPoint x) = c.toComponentPoint x := rfl7273theorem gPointToComponentPoint_bijective (c : ClosureSpace α) :74    Function.Bijective c.gPointToComponentPoint := by75  constructor76  · intro q r77    refine Quotient.inductionOn₂ q r ?_78    intro x y h79    exact Quotient.sound ((c.toComponentPoint_eq_iff x y).mp h)80  · intro C81    obtain ⟨x, rfl⟩ := c.toComponentPoint_surjective C82    exact ⟨c.toGPoint x, rfl⟩8384/-- The actual quotient-to-component-set equivalence. -/85noncomputable def gPointEquivComponentPoint (c : ClosureSpace α) :86    c.GPoint ≃ c.ComponentPoint :=87  Equiv.ofBijective c.gPointToComponentPoint c.gPointToComponentPoint_bijective8889@[simp]90theorem gPointEquivComponentPoint_toGPoint (c : ClosureSpace α) (x : α) :91    c.gPointEquivComponentPoint (c.toGPoint x) = c.toComponentPoint x := rfl9293/-- Closing a component-set representative yields a P-point. -/94def componentPointToPPoint (c : ClosureSpace α) (C : c.ComponentPoint) : c.PPoint :=95  ⟨c.closure C.val, by96    obtain ⟨x, hx⟩ := C.property97    exact ⟨x, congrArg c.closure hx⟩⟩9899@[simp]100theorem componentPointToPPoint_toComponentPoint (c : ClosureSpace α) (x : α) :101    c.componentPointToPPoint (c.toComponentPoint x) = c.toPPoint x := rfl102103/-- The change of G-point representation commutes with the original delta. -/104theorem componentPointToPPoint_gPointEquivComponentPoint (c : ClosureSpace α)105    (q : c.GPoint) :106    c.componentPointToPPoint (c.gPointEquivComponentPoint q) = c.delta q := by107  refine Quotient.inductionOn q ?_108  intro x109  rfl110111end ClosureSpace