Documentation

TauCeti.Topology.Homotopy.GenLoop.Homotopic

Homotopy of generalized loops is path connectedness #

Mathlib defines GenLoop.Homotopic, homotopy of generalized loops relative to the cube boundary, and separately topologises Ω^ N X x with the compact-open topology, but does not relate the two. Two generalized loops are homotopic relative to the cube boundary exactly when they are joined by a path in Ω^ N X x: currying a homotopy I × I^N → X gives the path, and uncurrying a path gives the homotopy; the boundary condition is automatic in both directions, because every generalized loop is constant at x on the cube boundary. Consequently any homeomorphism between spaces of generalized loops preserves and reflects homotopy.

Main declarations #

Homotopy relative to the boundary is path connectedness #

source
def GenLoop.pathOfHomotopyRel {N : Type u_2} {X : Type u_3} [TopologicalSpace X] {x : X} {p q : ↑(GenLoop N X x)} (H : (↑p).HomotopyRel (↑q) (Cube.boundary N)) :
Path p q

The path in the space of generalized loops traced by a homotopy relative to the cube boundary. Each stage of the homotopy is a generalized loop because the homotopy is stationary on the cube boundary, where its initial stage takes the value x.

Instances For
    source
    @[simp]
    theorem GenLoop.pathOfHomotopyRel_apply {N : Type u_2} {X : Type u_3} [TopologicalSpace X] {x : X} {p q : ↑(GenLoop N X x)} (H : (↑p).HomotopyRel (↑q) (Cube.boundary N)) (t : ↑unitInterval) (z : N → ↑unitInterval) :
    ((pathOfHomotopyRel H) t) z = H (t, z)
    source
    def GenLoop.homotopyRelOfPath {N : Type u_2} {X : Type u_3} [TopologicalSpace X] {x : X} {p q : ↑(GenLoop N X x)} (γ : Path p q) :
    (↑p).HomotopyRel (↑q) (Cube.boundary N)

    The homotopy relative to the cube boundary underlying a path in the space of generalized loops. The relative condition is automatic: every stage of the path is a generalized loop, so it takes the value x at every point of the cube boundary.

    Instances For
      source
      @[simp]
      theorem GenLoop.homotopyRelOfPath_apply {N : Type u_2} {X : Type u_3} [TopologicalSpace X] {x : X} {p q : ↑(GenLoop N X x)} (γ : Path p q) (t : ↑unitInterval) (z : N → ↑unitInterval) :
      (homotopyRelOfPath γ) (t, z) = (γ t) z
      source
      theorem GenLoop.homotopic_of_continuousMap {N : Type u_2} {X : Type u_3} [TopologicalSpace X] {x : X} {p q : ↑(GenLoop N X x)} (H : C(↑unitInterval × (N → ↑unitInterval), X)) (h₀ : ∀ (z : N → ↑unitInterval), H (0, z) = p z) (h₁ : ∀ (z : N → ↑unitInterval), H (1, z) = q z) (hb : ∀ (t : ↑unitInterval), ∀ z ∈ Cube.boundary N, H (t, z) = x) :
      Homotopic p q

      A continuous map I × I^N → X from p to q that takes the value x over the cube boundary is a homotopy of generalized loops relative to the cube boundary.

      source
      theorem GenLoop.homotopic_iff_joined {N : Type u_2} {X : Type u_3} [TopologicalSpace X] {x : X} {p q : ↑(GenLoop N X x)} :
      Homotopic p q ↔ Joined p q

      Two generalized loops are homotopic relative to the cube boundary exactly when they are joined by a path in the space of generalized loops. The compact-open topology on Ω^ N X x therefore records the homotopy relation of HomotopyGroup N X x as its path components.

      source
      @[simp]
      theorem Homeomorph.genLoopHomotopic_iff {M : Type u_1} {N : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (φ : ↑(GenLoop M X x) ≃ₜ ↑(GenLoop N Y y)) {p q : ↑(GenLoop M X x)} :
      GenLoop.Homotopic (φ p) (φ q) ↔ GenLoop.Homotopic p q

      A homeomorphism between spaces of generalized loops preserves and reflects homotopy relative to the cube boundary: both are path connectedness, which a homeomorphism transports in both directions.