MathlibAnnex/Topology/ClosureSpace/FiniteConjugation.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.FiniteHomeomorph9public import MathlibAnnex.Topology.ClosureSpace.Category10public import MathlibAnnex.Topology.ClosureSpace.ComponentSubspace1112/-!13# Continuous conjugation of finite homeomorphisms1415For a class `D : ClosureCat → Prop`, `HasContinuousFiniteConjugation c D`16quantifies over every eligible source object and every one of its components,17with the existing subspace closure. The two inputs are finite homeomorphisms18whose FORWARD functions are fully continuous. Their inverses are not assumed19fully continuous. The conclusion concerns both directions of the actual20conjugate `f ∘ g ∘ f⁻¹`.2122This is the closure-language property occurring in Theorem 7.7(ii) of23arXiv:2504.05551v1, not a definition of an elementary algebra and not a proof24of that characterization. Target and eligible-source carrier universes are25independent. No ordinary topology or closedness of a component is assumed.26-/2728@[expose] public section2930set_option autoImplicit false3132universe u v w s t3334namespace ClosureSpace3536variable {α : Type u} {β : Type v} {γ : Type w}37variable {c : ClosureSpace α} {d : ClosureSpace β} {k : ClosureSpace γ}3839/-- Relative finite-conjugation property. The source class is not restricted40to a chosen object or algebra. Components retain their actual subspace closure. -/41def HasContinuousFiniteConjugation (c : ClosureSpace α) (D : ClosureCat.{s} → Prop) : Prop :=42  ∀ (L : ClosureCat.{s}), D L → ∀ t : L,43    ∀ f : FiniteHomeomorph (L.str.subspace (L.str.component t)) c,44      (L.str.subspace (L.str.component t)).Continuous c f.toEquiv →45      ∀ g : FiniteHomeomorph (L.str.subspace (L.str.component t))46          (L.str.subspace (L.str.component t)),47        (L.str.subspace (L.str.component t)).Continuous48          (L.str.subspace (L.str.component t)) g.toEquiv →49        c.Continuous c (f.conjugate g).toEquiv ∧50          c.Continuous c (f.conjugate g).toEquiv.symm5152/-- The property gives a full homeomorphism with exactly the prescribed53conjugate equivalence; this is a construction from the defined property. -/54def HasContinuousFiniteConjugation.conjugateHomeomorph55    {D : ClosureCat.{s} → Prop} (hc : c.HasContinuousFiniteConjugation D)56    (L : ClosureCat.{s}) (hL : D L) (t : L)57    (f : FiniteHomeomorph (L.str.subspace (L.str.component t)) c)58    (hf : (L.str.subspace (L.str.component t)).Continuous c f.toEquiv)59    (g : FiniteHomeomorph (L.str.subspace (L.str.component t))60      (L.str.subspace (L.str.component t)))61    (hg : (L.str.subspace (L.str.component t)).Continuous62      (L.str.subspace (L.str.component t)) g.toEquiv) : Homeomorph c c where63  toEquiv := (f.conjugate g).toEquiv64  continuous_toFun := (hc L hL t f hf g hg).165  continuous_invFun := (hc L hL t f hf g hg).26667@[simp]68theorem HasContinuousFiniteConjugation.conjugateHomeomorph_apply69    {D : ClosureCat.{s} → Prop} (hc : c.HasContinuousFiniteConjugation D)70    (L : ClosureCat.{s}) (hL : D L) (t : L)71    (f : FiniteHomeomorph (L.str.subspace (L.str.component t)) c)72    (hf : (L.str.subspace (L.str.component t)).Continuous c f.toEquiv)73    (g : FiniteHomeomorph (L.str.subspace (L.str.component t))74      (L.str.subspace (L.str.component t)))75    (hg : (L.str.subspace (L.str.component t)).Continuous76      (L.str.subspace (L.str.component t)) g.toEquiv) (x : α) :77    (hc.conjugateHomeomorph L hL t f hf g hg).toEquiv x =78      f.toEquiv (g.toEquiv (f.toEquiv.symm x)) := rfl7980@[simp]81theorem HasContinuousFiniteConjugation.conjugateHomeomorph_symm_apply82    {D : ClosureCat.{s} → Prop} (hc : c.HasContinuousFiniteConjugation D)83    (L : ClosureCat.{s}) (hL : D L) (t : L)84    (f : FiniteHomeomorph (L.str.subspace (L.str.component t)) c)85    (hf : (L.str.subspace (L.str.component t)).Continuous c f.toEquiv)86    (g : FiniteHomeomorph (L.str.subspace (L.str.component t))87      (L.str.subspace (L.str.component t)))88    (hg : (L.str.subspace (L.str.component t)).Continuous89      (L.str.subspace (L.str.component t)) g.toEquiv) (x : α) :90    (hc.conjugateHomeomorph L hL t f hf g hg).toEquiv.symm x =91      f.toEquiv (g.toEquiv.symm (f.toEquiv.symm x)) := rfl9293/-- Restrict the eligible class, retaining its full quantification. -/94theorem HasContinuousFiniteConjugation.mono {D E : ClosureCat.{s} → Prop}95    (hc : c.HasContinuousFiniteConjugation D) (hED : ∀ L, E L → D L) :96    c.HasContinuousFiniteConjugation E :=97  fun L hL t f hf g hg => hc L (hED L hL) t f hf g hg9899/-- A full target homeomorphism preserves the property. No full inverse100continuity is added to the two finite-homeomorphism inputs. -/101theorem Homeomorph.hasContinuousFiniteConjugation {D : ClosureCat.{s} → Prop}102    (a : Homeomorph c d) (hc : c.HasContinuousFiniteConjugation D) :103    d.HasContinuousFiniteConjugation D := by104  intro L hL t f hf g hg105  let f' := f.trans a.symm.toFiniteHomeomorph106  have hf' : (L.str.subspace (L.str.component t)).Continuous c f'.toEquiv :=107    a.continuous_invFun.comp hf108  let b := hc.conjugateHomeomorph L hL t f' hf' g hg109  let q : Homeomorph d d := a.symm.trans (b.trans a)110  have hq : q.toEquiv = (f.conjugate g).toEquiv := by111    apply Equiv.ext112    intro y113    change a.toEquiv (a.toEquiv.symm114      (f.toEquiv (g.toEquiv (f.toEquiv.symm (a.toEquiv (a.toEquiv.symm y)))))) =115        f.toEquiv (g.toEquiv (f.toEquiv.symm y))116    simp only [Equiv.apply_symm_apply]117  constructor118  · rw [← hq]119    exact q.continuous_toFun120  · rw [← hq]121    exact q.continuous_invFun122123/-- Target homeomorphism invariance, in both directions. -/124theorem Homeomorph.hasContinuousFiniteConjugation_iff {D : ClosureCat.{s} → Prop}125    (a : Homeomorph c d) :126    c.HasContinuousFiniteConjugation D ↔ d.HasContinuousFiniteConjugation D :=127  ⟨a.hasContinuousFiniteConjugation, a.symm.hasContinuousFiniteConjugation⟩128129/-- Enlarge the eligible class by genuine homeomorphic copies. Source carrier130universes may differ. Every new object is supplied with an actual old witness;131we pull back its distinguished point and restrict the witness to that component. -/132theorem HasContinuousFiniteConjugation.of_source_homeomorphs133    {D : ClosureCat.{s} → Prop} {E : ClosureCat.{t} → Prop}134    (hc : c.HasContinuousFiniteConjugation D)135    (hED : ∀ (M : ClosureCat.{t}), E M →136      ∃ L : ClosureCat.{s}, D L ∧ Nonempty (Homeomorph L.str M.str)) :137    c.HasContinuousFiniteConjugation E := by138  intro M hM x f hf g hg139  obtain ⟨L, hL, ⟨a⟩⟩ := hED M hM140  let y := a.toEquiv.symm x141  let b : Homeomorph (L.str.subspace (L.str.component y))142      (M.str.subspace (M.str.component x)) := by143    have hb := a.component y144    change Homeomorph (L.str.subspace (L.str.component y))145      (M.str.subspace (M.str.component (a.toEquiv y))) at hb146    have hxy : a.toEquiv y = x := a.toEquiv.apply_symm_apply x147    rw [hxy] at hb148    exact hb149  let f' := b.toFiniteHomeomorph.trans f150  let g' := b.symm.toFiniteHomeomorph.conjugate g151  have hf' : (L.str.subspace (L.str.component y)).Continuous c f'.toEquiv :=152    hf.comp b.continuous_toFun153  have hg' : (L.str.subspace (L.str.component y)).Continuous154      (L.str.subspace (L.str.component y)) g'.toEquiv :=155    b.continuous_invFun.comp (hg.comp b.continuous_toFun)156  have hh := hc L hL y f' hf' g' hg'157  have heq : (f'.conjugate g').toEquiv = (f.conjugate g).toEquiv :=158    FiniteHomeomorph.conjugate_reparam_toEquiv b f g159  rw [heq] at hh160  exact hh161162/-- Equivalent choices of source coordinates give the same target property. -/163theorem hasContinuousFiniteConjugation_iff_of_source_homeomorphs164    {D : ClosureCat.{s} → Prop} {E : ClosureCat.{t} → Prop}165    (hED : ∀ (M : ClosureCat.{t}), E M →166      ∃ L : ClosureCat.{s}, D L ∧ Nonempty (Homeomorph L.str M.str))167    (hDE : ∀ (L : ClosureCat.{s}), D L →168      ∃ M : ClosureCat.{t}, E M ∧ Nonempty (Homeomorph M.str L.str)) :169    c.HasContinuousFiniteConjugation D ↔ c.HasContinuousFiniteConjugation E :=170  ⟨fun hc => hc.of_source_homeomorphs hED, fun hc => hc.of_source_homeomorphs hDE⟩171172/-- Reparameterize a target component using its existing restriction homeomorphism. -/173theorem Homeomorph.hasContinuousFiniteConjugation_component_iff174    {D : ClosureCat.{s} → Prop} (a : Homeomorph c d) (x : α) :175    (c.subspace (c.component x)).HasContinuousFiniteConjugation D ↔176      (d.subspace (d.component (a.toEquiv x))).HasContinuousFiniteConjugation D :=177  (a.component x).hasContinuousFiniteConjugation_iff178179/-- The existential component condition in 7.7(ii) is invariant under a full180ambient homeomorphism. This does not assert that any space satisfies it. -/181theorem Homeomorph.exists_hasContinuousFiniteConjugation_component_iff182    {D : ClosureCat.{s} → Prop} (a : Homeomorph c d) :183    (∃ x : α, (c.subspace (c.component x)).HasContinuousFiniteConjugation D) ↔184      ∃ y : β, (d.subspace (d.component y)).HasContinuousFiniteConjugation D := by185  constructor186  · rintro ⟨x, hx⟩187    exact ⟨a.toEquiv x, (a.hasContinuousFiniteConjugation_component_iff x).mp hx⟩188  · rintro ⟨y, hy⟩189    refine ⟨a.toEquiv.symm y, ?_⟩190    apply (a.hasContinuousFiniteConjugation_component_iff (a.toEquiv.symm y)).mpr191    change (d.subspace (d.component (a.toEquiv (a.toEquiv.symm y)))).HasContinuousFiniteConjugation D192    rw [a.toEquiv.apply_symm_apply]193    exact hy194195end ClosureSpace