Functoriality of homotopy groups

Mathlib defines the generalized loop space Ω^ N X x and the quotient HomotopyGroup N X x, but it does not yet provide the map induced by a based continuous map. This file supplies that small API: postcomposition sends generalized loops based at x to generalized loops based at y, descends to homotopy classes, respects identity and composition, handles constant maps and subsingleton targets, and is a monoid homomorphism in positive dimensions.

This is a prerequisite for the higher-homotopy API requested in the Tau Ceti universal-covers roadmap, Stage 3 item 9, before proving that a covering map induces isomorphisms on π_n for n ≥ 2.

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

A based continuous map sends generalized loops to generalized loops by postcomposition.

Equations

• GenLoop.map f hf p = ⟨f.comp ↑p, ⋯⟩

@[simp]

theorem GenLoop.map_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (p : ↑(GenLoop N X x)) (t : N → ↑unitInterval) : (map f hf p) t = f (p t)

@[simp]

theorem GenLoop.map_const {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) : map f hf const = const

theorem GenLoop.map_continuousMap_const {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} (y : Y) (p : ↑(GenLoop N X x)) : map (ContinuousMap.const X y) ⋯ p = const

Postcomposition by a constant continuous map gives the constant generalized loop.

This is not a simp lemma: baking the basepoint proof rfl into the statement forces the target basepoint to be (ContinuousMap.const X y) x rather than y, so simp cannot close even its own statement. Use it as an explicit rewrite.

@[simp]

theorem GenLoop.map_id {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (p : ↑(GenLoop N X x)) : map (ContinuousMap.id X) ⋯ p = p

@[simp]

theorem GenLoop.map_comp {N : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {x : X} {y : Y} {z : Z} (g : C(Y, Z)) (hg : g y = z) (f : C(X, Y)) (hf : f x = y) (p : ↑(GenLoop N X x)) : map g hg (map f hf p) = map (g.comp f) ⋯ p

theorem GenLoop.map_homotopic {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {f g : ↑(GenLoop N X x)} (h : Homotopic f g) (F : C(X, Y)) (hF : F x = y) : Homotopic (map F hF f) (map F hF g)

Postcomposition preserves homotopy relative to the cube boundary.

@[simp]

theorem GenLoop.map_transAt {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [DecidableEq N] (F : C(X, Y)) (hF : F x = y) (i : N) (p q : ↑(GenLoop N X x)) : map F hF (transAt i p q) = transAt i (map F hF p) (map F hF q)

@[simp]

theorem GenLoop.map_symmAt {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [DecidableEq N] (F : C(X, Y)) (hF : F x = y) (i : N) (p : ↑(GenLoop N X x)) : map F hF (symmAt i p) = symmAt i (map F hF p)

@[simp]

theorem HomotopyGroup.mk_const_eq_one {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] [Nonempty N] : ⟦GenLoop.const⟧ = 1

In positive dimensions, the class of the constant generalized loop is the identity element. This is HomotopyGroup.one_def oriented towards 1, so that 1 is the simp normal form for the constant-map results below.

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

The map on homotopy classes induced by a based continuous map.

Equations

• HomotopyGroup.map f hf = Quotient.map (GenLoop.map f hf) ⋯

@[simp]

theorem HomotopyGroup.map_mk {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (p : ↑(GenLoop N X x)) : map f hf ⟦p⟧ = ⟦GenLoop.map f hf p⟧

@[simp]

theorem HomotopyGroup.map_continuousMap_const_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} (y : Y) (hy : (ContinuousMap.const X y) x = y) (a : HomotopyGroup N X x) : map (ContinuousMap.const X y) hy a = ⟦GenLoop.const⟧

A constant continuous map sends every homotopy class to the class of the constant generalized loop. This statement also covers dimension zero, where the target need not carry the positive-dimensional group structure.

theorem HomotopyGroup.map_eq_continuousMap_const_of_subsingleton {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [Subsingleton Y] (f : C(X, Y)) (hf : f x = y) : map f hf = map (ContinuousMap.const X y) ⋯

A based map into a subsingleton space induces the same map as the constant map at the target basepoint.

@[simp]

theorem HomotopyGroup.map_apply_of_subsingleton {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [Subsingleton Y] (f : C(X, Y)) (hf : f x = y) (a : HomotopyGroup N X x) : map f hf a = ⟦GenLoop.const⟧

A based map into a subsingleton space sends every homotopy class to the class of the constant generalized loop.

theorem HomotopyGroup.map_continuousMap_const_apply_eq_one {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} [DecidableEq N] [Nonempty N] (y : Y) (hy : (ContinuousMap.const X y) x = y) (a : HomotopyGroup N X x) : map (ContinuousMap.const X y) hy a = 1

In positive dimensions, a constant continuous map sends every homotopy class to the identity.

This is not a simp lemma: the positive-dimensional normal form is already reached by map_continuousMap_const_apply followed by mk_const_eq_one, so a separate ⟦const⟧-keyed = 1 rule would be redundant. It is kept as an explicit rewrite.

theorem HomotopyGroup.map_apply_eq_one_of_subsingleton {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [DecidableEq N] [Nonempty N] [Subsingleton Y] (f : C(X, Y)) (hf : f x = y) (a : HomotopyGroup N X x) : map f hf a = 1

In positive dimensions, a based map into a subsingleton space sends every homotopy class to the identity.

This is not a simp lemma: the positive-dimensional normal form is already reached by map_apply_of_subsingleton followed by mk_const_eq_one, so a separate composite = 1 rule would be redundant. It is kept as an explicit rewrite.

@[simp]

theorem HomotopyGroup.map_id_apply {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (a : HomotopyGroup N X x) : map (ContinuousMap.id X) ⋯ a = a

Identity law: the map induced by the identity continuous map is the identity on homotopy classes.

@[simp]

theorem HomotopyGroup.map_comp_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {x : X} {y : Y} {z : Z} (g : C(Y, Z)) (hg : g y = z) (f : C(X, Y)) (hf : f x = y) (a : HomotopyGroup N X x) : map g hg (map f hf a) = map (g.comp f) ⋯ a

Composition law: the map induced by a composite continuous map is the composite of the induced maps on homotopy classes.

theorem HomotopyGroup.map_congr {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {f₁ f₂ : C(X, Y)} (hfe : f₁ = f₂) (h₁ : f₁ x = y) (h₂ : f₂ x = y) (a : HomotopyGroup N X x) : map f₁ h₁ a = map f₂ h₂ a

The induced map HomotopyGroup.map depends only on the underlying continuous map, not on the chosen proof of the basepoint equation.

theorem HomotopyGroup.map_map_of_comp_eq_id {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (g : C(Y, X)) (f : C(X, Y)) (hf : f x = y) (hg : g y = x) (hgf : g.comp f = ContinuousMap.id X) (a : HomotopyGroup N X x) : map g hg (map f hf a) = a

If g ∘ f is the identity, then the induced map of g undoes the induced map of f on homotopy classes.

def HomotopyGroup.mapHom {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 : C(X, Y)) (hf : f x = y) : HomotopyGroup N X x →* HomotopyGroup N Y y

In positive dimensions, the map induced by a based continuous map is a monoid homomorphism for the standard group structure on homotopy groups.

Equations

• HomotopyGroup.mapHom f hf = { toFun := HomotopyGroup.map f hf, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem HomotopyGroup.mapHom_apply {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 : C(X, Y)) (hf : f x = y) (a : HomotopyGroup N X x) : (mapHom f hf) a = map f hf a

theorem HomotopyGroup.mapHom_continuousMap_const_eq_one {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} [DecidableEq N] [Nonempty N] (y : Y) : mapHom (ContinuousMap.const X y) ⋯ = 1

In positive dimensions, a constant continuous map induces the trivial homomorphism on homotopy groups.

This is not a simp lemma: baking the basepoint proof rfl into the statement forces the target basepoint to be (ContinuousMap.const X y) x rather than y, so simp cannot close even its own statement. Use it as an explicit rewrite.

@[simp]

theorem HomotopyGroup.mapHom_eq_one_of_subsingleton {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [DecidableEq N] [Nonempty N] [Subsingleton Y] (f : C(X, Y)) (hf : f x = y) : mapHom f hf = 1

A based map into a subsingleton space induces the trivial homomorphism on every positive-dimensional homotopy group.

@[simp]

theorem HomotopyGroup.mapHom_id {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [DecidableEq N] [Nonempty N] : mapHom (ContinuousMap.id X) ⋯ = MonoidHom.id (HomotopyGroup N X x)

Identity law for the bundled homomorphism: the induced monoid homomorphism of the identity continuous map is the identity homomorphism.

@[simp]

theorem HomotopyGroup.mapHom_comp {N : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {x : X} {y : Y} {z : Z} [DecidableEq N] [Nonempty N] (g : C(Y, Z)) (hg : g y = z) (f : C(X, Y)) (hf : f x = y) : (mapHom g hg).comp (mapHom f hf) = mapHom (g.comp f) ⋯

Composition law for the bundled homomorphism: the induced monoid homomorphism of a composite continuous map is the composite of the induced homomorphisms.

@[simp]

theorem HomotopyGroup.map_mul {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 : C(X, Y)) (hf : f x = y) (a b : HomotopyGroup N X x) : map f hf (a * b) = map f hf a * map f hf b

@[simp]

theorem HomotopyGroup.map_one {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 : C(X, Y)) (hf : f x = y) : map f hf 1 = 1