Homotopy of generalized loops

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. This file proves that they agree: 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. In the one-dimensional case this is transported across Mathlib's bijection genLoopEquivOfUnique between one-dimensional generalized loops and paths, where homotopy relative to the cube boundary becomes homotopy of paths.

The file also treats homotopies in the base space: a homotopy between based maps must remain fixed at the basepoint in order to induce a homotopy between their postcompositions with a generalized loop. That construction is made explicit, and pointed-homotopic maps are shown to induce the same map on every homotopy group, with the corresponding equality of bundled monoid homomorphisms in positive dimensions.

Main declarations

• GenLoop.homotopic_iff_joined: homotopy relative to the cube boundary is path connectedness in Ω^ N X x.
• GenLoop.homotopic_genLoopEquivOfUnique_iff: for a singleton index type, homotopy relative to the cube boundary is homotopy of the corresponding paths.
• HomotopyGroup.map_eq_of_homotopicRel: pointed-homotopic maps induce the same map on homotopy groups.

Homotopy relative to the boundary is path connectedness

def GenLoop.pathOfHomotopyRel {N : Type u_1} {X : Type u_2} [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.

Equations

• GenLoop.pathOfHomotopyRel H = { toFun := fun (t : ↑unitInterval) => ⟨H.curry t, ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem GenLoop.pathOfHomotopyRel_apply {N : Type u_1} {X : Type u_2} [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)

def GenLoop.homotopyRelOfPath {N : Type u_1} {X : Type u_2} [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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GenLoop.homotopyRelOfPath_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {p q : ↑(GenLoop N X x)} (γ : Path p q) (t : ↑unitInterval) (z : N → ↑unitInterval) : (homotopyRelOfPath γ) (t, z) = (γ t) z

theorem GenLoop.homotopic_iff_joined {N : Type u_1} {X : Type u_2} [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.

theorem GenLoop.homotopic_genLoopEquivOfUnique_iff {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [Unique N] {p q : ↑(GenLoop N X x)} : Path.Homotopic ((genLoopEquivOfUnique N) p) ((genLoopEquivOfUnique N) q) ↔ Homotopic p q

Homotopy of one-dimensional generalized loops relative to the cube boundary is homotopy of the paths they correspond to under Mathlib's bijection genLoopEquivOfUnique. Both sides say that the two classes agree in a quotient, and homotopyGroupEquivFundamentalGroupOfUnique identifies HomotopyGroup N X x with FundamentalGroup X x by exactly this bijection.

Homotopies in the base space

theorem GenLoop.map_homotopic_of_homotopicRel {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {f g : C(X, Y)} (hf : f x = y) {S : Set X} (hx : x ∈ S) (H : f.HomotopicRel g S) (p : ↑(GenLoop N X x)) : Homotopic (map f hf p) (map g ⋯ p)

Postcomposing a generalized loop with maps homotopic relative to a set containing the basepoint gives homotopic generalized loops. The resulting homotopy is relative to the cube boundary.

theorem HomotopyGroup.map_eq_of_homotopicRel {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {f g : C(X, Y)} (hf : f x = y) {S : Set X} (hx : x ∈ S) (H : f.HomotopicRel g S) : map f hf = map g ⋯

Continuous maps homotopic relative to a set containing the basepoint induce the same function on homotopy groups.

theorem HomotopyGroup.mapHom_eq_of_homotopicRel {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [DecidableEq N] [Nonempty N] {f g : C(X, Y)} (hf : f x = y) {S : Set X} (hx : x ∈ S) (H : f.HomotopicRel g S) : mapHom f hf = mapHom g ⋯

Continuous maps homotopic relative to a set containing the basepoint have equal induced monoid homomorphisms on positive-dimensional homotopy groups.