def PiBase.Formal.genLoopMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {N : Type u_3} (f : C(X, Y)) {x : X} {y : Y} (hf : f x = y) : ↑(GenLoop N X x) → ↑(GenLoop N Y y)

Postcomposition of a generalized loop based at x with a continuous map taking x to y.

Equations

• PiBase.Formal.genLoopMap f hf p = ⟨f.comp ↑p, ⋯⟩

@[simp]

theorem PiBase.Formal.genLoopMap_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {N : Type u_3} (f : C(X, Y)) {x : X} {y : Y} (hf : f x = y) (p : ↑(GenLoop N X x)) : ↑(genLoopMap f hf p) = f.comp ↑p

def PiBase.Formal.homotopyGroupMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {N : Type u_3} (f : C(X, Y)) {x : X} {y : Y} (hf : f x = y) : HomotopyGroup N X x → HomotopyGroup N Y y

The map on homotopy groups induced by postcomposition with a continuous map taking the base point x to the base point y.

Equations

• PiBase.Formal.homotopyGroupMap f hf = Quotient.lift (fun (p : ↑(GenLoop N X x)) => ⟦PiBase.Formal.genLoopMap f hf p⟧) ⋯

@[simp]

theorem PiBase.Formal.homotopyGroupMap_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {N : Type u_3} (f : C(X, Y)) {x : X} {y : Y} (hf : f x = y) (p : ↑(GenLoop N X x)) : homotopyGroupMap f hf ⟦p⟧ = ⟦genLoopMap f hf p⟧

theorem PiBase.Formal.homotopyGroupMap_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {N : Type u_3} (φ : X ≃ₜ Y) (y : Y) : Function.Surjective (homotopyGroupMap ↑φ ⋯)

A homeomorphism induces a surjection on homotopy groups: postcomposition with φ.symm provides a section.

theorem PiBase.WellDefined.weaklyContractibleSpace : WellDefined WeaklyContractibleSpace