Documentation

TauCeti.Topology.Homotopy.GenLoop.Homeomorph

Homeomorphisms of spaces of generalized loops #

Mathlib's bijection genLoopEquivOfUnique between the generalized loops indexed by a singleton and the loop space Ω X x is continuous both ways for the compact-open topologies. A homeomorphism e : X ≃ₜ Y with e x = y also induces, by postcomposition, a homeomorphism of the spaces of generalized loops Ω^ N X x ≃ₜ Ω^ N Y y.

Main declarations #

source
def GenLoop.homeomorphOfUnique {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [Unique N] :
↑(GenLoop N X x) ≃ₜ LoopSpace X x

Mathlib's bijection genLoopEquivOfUnique between the one-dimensional generalized loops at x and the loop space Ω X x, upgraded to a homeomorphism for the compact-open topologies.

Instances For
    source
    @[simp]
    theorem GenLoop.homeomorphOfUnique_apply {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [Unique N] (p : ↑(GenLoop N X x)) (t : ↑unitInterval) :
    ((homeomorphOfUnique N) p) t = p fun (x : N) => t
    source
    @[simp]
    theorem GenLoop.homeomorphOfUnique_symm_apply {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [Unique N] (γ : LoopSpace X x) (t : N → ↑unitInterval) :
    ((homeomorphOfUnique N).symm γ) t = γ (t default)
    source
    @[simp]
    theorem GenLoop.homeomorphOfUnique_const {X : Type u_2} [TopologicalSpace X] {x : X} (N : Type u_3) [Unique N] :
    (homeomorphOfUnique N) const = Path.refl x

    The homeomorphism of GenLoop.homeomorphOfUnique is based: it carries the constant generalized loop to the constant path.

    source
    def Homeomorph.genLoopHomeomorph {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {Y : Type u_3} [TopologicalSpace Y] {y : Y} (e : X ≃ₜ Y) (h : e x = y) :
    ↑(GenLoop N X x) ≃ₜ ↑(GenLoop N Y y)

    A homeomorphism e : X ≃ₜ Y with e x = y induces, by postcomposition, a homeomorphism of the spaces of generalized loops Ω^ N X x ≃ₜ Ω^ N Y y.

    Instances For
      source
      theorem Homeomorph.genLoopHomeomorph_symm {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {Y : Type u_3} [TopologicalSpace Y] {y : Y} (e : X ≃ₜ Y) (h : e x = y) :
      (e.genLoopHomeomorph h).symm = e.symm.genLoopHomeomorph ⋯

      The inverse of Homeomorph.genLoopHomeomorph e is Homeomorph.genLoopHomeomorph e.symm.

      source
      @[simp]
      theorem Homeomorph.genLoopHomeomorph_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {Y : Type u_3} [TopologicalSpace Y] {y : Y} (e : X ≃ₜ Y) (h : e x = y) (p : ↑(GenLoop N X x)) (t : N → ↑unitInterval) :
      ((e.genLoopHomeomorph h) p) t = e (p t)
      source
      @[simp]
      theorem Homeomorph.genLoopHomeomorph_const {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {Y : Type u_3} [TopologicalSpace Y] {y : Y} (e : X ≃ₜ Y) (h : e x = y) :
      (e.genLoopHomeomorph h) GenLoop.const = GenLoop.const

      The homeomorphism Homeomorph.genLoopHomeomorph e is based: it carries the constant generalized loop to the constant generalized loop.

      source
      @[simp]
      theorem Homeomorph.genLoopHomeomorph_symm_const {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {Y : Type u_3} [TopologicalSpace Y] {y : Y} (e : X ≃ₜ Y) (h : e x = y) :
      (e.genLoopHomeomorph h).symm GenLoop.const = GenLoop.const

      The inverse of Homeomorph.genLoopHomeomorph e also carries the constant generalized loop to the constant generalized loop.

      source
      @[simp]
      theorem Homeomorph.genLoopHomeomorph_symm_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {Y : Type u_3} [TopologicalSpace Y] {y : Y} (e : X ≃ₜ Y) (h : e x = y) (p : ↑(GenLoop N Y y)) (t : N → ↑unitInterval) :
      ((e.genLoopHomeomorph h).symm p) t = e.symm (p t)