MathlibAnnex/Topology/ClosureSpace/FiniteHomeomorph.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# Finite homeomorphism composition and conjugation1213The composition, conjugate and source-reparameterization identities depend only14on closure-space maps, not on categories or a class-relative property.15-/1617@[expose] public section1819set_option autoImplicit false2021universe u v w s t2223namespace ClosureSpace2425variable {α : Type u} {β : Type v} {γ : Type w}26variable {c : ClosureSpace α} {d : ClosureSpace β} {k : ClosureSpace γ}2728/-- Compose the existing finite homeomorphisms; `f.trans g` acts as `g ∘ f`. -/29def FiniteHomeomorph.trans (f : FiniteHomeomorph c d) (g : FiniteHomeomorph d k) :30    FiniteHomeomorph c k where31  toEquiv := f.toEquiv.trans g.toEquiv32  finitelyContinuous_toFun := g.finitelyContinuous_toFun.comp f.finitelyContinuous_toFun33  finitelyContinuous_invFun := f.finitelyContinuous_invFun.comp g.finitelyContinuous_invFun3435@[simp]36theorem FiniteHomeomorph.trans_apply (f : FiniteHomeomorph c d)37    (g : FiniteHomeomorph d k) (x : α) :38    (f.trans g).toEquiv x = g.toEquiv (f.toEquiv x) := rfl3940@[simp]41theorem FiniteHomeomorph.trans_symm_apply (f : FiniteHomeomorph c d)42    (g : FiniteHomeomorph d k) (z : γ) :43    (f.trans g).toEquiv.symm z = f.toEquiv.symm (g.toEquiv.symm z) := rfl4445/-- Conjugation on the target. Full continuity is not part of this construction. -/46def FiniteHomeomorph.conjugate (f : FiniteHomeomorph c d)47    (g : FiniteHomeomorph c c) : FiniteHomeomorph d d :=48  f.symm.trans (g.trans f)4950@[simp]51theorem FiniteHomeomorph.conjugate_apply (f : FiniteHomeomorph c d)52    (g : FiniteHomeomorph c c) (y : β) :53    (f.conjugate g).toEquiv y = f.toEquiv (g.toEquiv (f.toEquiv.symm y)) := rfl5455@[simp]56theorem FiniteHomeomorph.conjugate_symm_apply (f : FiniteHomeomorph c d)57    (g : FiniteHomeomorph c c) (y : β) :58    (f.conjugate g).toEquiv.symm y =59      f.toEquiv (g.toEquiv.symm (f.toEquiv.symm y)) := rfl6061/-- Changing source coordinates by a full homeomorphism leaves the conjugate62unchanged as an actual equivalence, including its inverse. -/63theorem FiniteHomeomorph.conjugate_reparam_toEquiv (a : Homeomorph c d)64    (f : FiniteHomeomorph d k) (g : FiniteHomeomorph d d) :65    ((a.toFiniteHomeomorph.trans f).conjugate66      (a.symm.toFiniteHomeomorph.conjugate g)).toEquiv =67      (f.conjugate g).toEquiv := by68  apply Equiv.ext69  intro z70  change f.toEquiv (a.toEquiv (a.toEquiv.symm71    (g.toEquiv (a.toEquiv (a.toEquiv.symm (f.toEquiv.symm z)))))) =72      f.toEquiv (g.toEquiv (f.toEquiv.symm z))73  simp only [Equiv.apply_symm_apply]7475/-- The same coordinate change transports full continuity of the conjugate76in both directions. It assumes no continuity of the inverses of `f` or `g`. -/77theorem FiniteHomeomorph.continuous_conjugate_reparam_iff (a : Homeomorph c d)78    (f : FiniteHomeomorph d k) (g : FiniteHomeomorph d d) :79    (k.Continuous k ((a.toFiniteHomeomorph.trans f).conjugate80        (a.symm.toFiniteHomeomorph.conjugate g)).toEquiv ∧81      k.Continuous k ((a.toFiniteHomeomorph.trans f).conjugate82        (a.symm.toFiniteHomeomorph.conjugate g)).toEquiv.symm) ↔83    (k.Continuous k (f.conjugate g).toEquiv ∧84      k.Continuous k (f.conjugate g).toEquiv.symm) := by85  rw [FiniteHomeomorph.conjugate_reparam_toEquiv]8687end ClosureSpace