Homotopy groups of products

Generalized loops and homotopies relative to the cube boundary are computed coordinatewise. Consequently, the homotopy group of a binary or indexed product is the corresponding product of homotopy groups. This file supplies the generalized-loop constructions, their characteristic API, and the resulting equivalences of homotopy groups. In positive dimensions the equivalences are multiplicative.

The relative-homotopy product constructions are due to Praneeth Kolichala and come from Mathlib.Topology.Homotopy.Product.

This is the product prerequisite for the torus calculation requested in TauCetiRoadmap/UniversalCovers/README.md, Stage 4, item 13: combining the indexed-product equivalence with the vanishing of the higher homotopy groups of a circle computes the higher homotopy groups of a torus.

Main declarations

• HomotopyGroup.prodEquiv: the homotopy group of a binary product is the product of the homotopy groups.
• HomotopyGroup.piEquiv: the homotopy group of an indexed product is the indexed product of the homotopy groups.
• HomotopyGroup.prodMulEquiv, HomotopyGroup.piMulEquiv: the positive-dimensional multiplicative forms.

def GenLoop.prod {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)) (q : ↑(GenLoop N Y y)) : ↑(GenLoop N (X × Y) (x, y))

The coordinatewise product of two generalized loops.

Equations

• GenLoop.prod p q = ⟨(↑p).prodMk ↑q, ⋯⟩

@[simp]

theorem GenLoop.prod_apply {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)) (q : ↑(GenLoop N Y y)) (t : N → ↑unitInterval) : (prod p q) t = (p t, q t)

@[simp]

theorem GenLoop.map_fst_prod {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)) (q : ↑(GenLoop N Y y)) : map ContinuousMap.fst ⋯ (prod p q) = p

Taking the first coordinate of a product generalized loop recovers the first loop.

@[simp]

theorem GenLoop.map_snd_prod {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)) (q : ↑(GenLoop N Y y)) : map ContinuousMap.snd ⋯ (prod p q) = q

Taking the second coordinate of a product generalized loop recovers the second loop.

@[simp]

theorem GenLoop.prod_map_fst_map_snd {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (p : ↑(GenLoop N (X × Y) (x, y))) : prod (map ContinuousMap.fst ⋯ p) (map ContinuousMap.snd ⋯ p) = p

A generalized loop in a product is recovered from its two coordinate loops.

theorem GenLoop.prod_homotopic {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {p p' : ↑(GenLoop N X x)} {q q' : ↑(GenLoop N Y y)} (hp : Homotopic p p') (hq : Homotopic q q') : Homotopic (prod p q) (prod p' q')

Coordinatewise products preserve homotopy relative to the cube boundary.

def GenLoop.pi {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} (p : (i : ι) → ↑(GenLoop N (Z i) (z i))) : ↑(GenLoop N ((i : ι) → Z i) z)

The coordinatewise indexed product of generalized loops.

Equations

• GenLoop.pi p = ⟨ContinuousMap.pi fun (i : ι) => ↑(p i), ⋯⟩

@[simp]

theorem GenLoop.pi_apply {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} (p : (i : ι) → ↑(GenLoop N (Z i) (z i))) (t : N → ↑unitInterval) (i : ι) : (pi p) t i = (p i) t

@[simp]

theorem GenLoop.map_eval_pi {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} (p : (i : ι) → ↑(GenLoop N (Z i) (z i))) (i : ι) : map (ContinuousMap.eval i) ⋯ (pi p) = p i

Taking a coordinate of an indexed product generalized loop recovers that coordinate loop.

@[simp]

theorem GenLoop.pi_map_eval {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} (p : ↑(GenLoop N ((i : ι) → Z i) z)) : (pi fun (i : ι) => map (ContinuousMap.eval i) ⋯ p) = p

A generalized loop in an indexed product is recovered from all of its coordinate loops.

theorem GenLoop.pi_homotopic {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} {p q : (i : ι) → ↑(GenLoop N (Z i) (z i))} (h : ∀ (i : ι), Homotopic (p i) (q i)) : Homotopic (pi p) (pi q)

Indexed products preserve coordinatewise homotopy relative to the cube boundary.

def HomotopyGroup.prod {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (a : HomotopyGroup N X x) (b : HomotopyGroup N Y y) : HomotopyGroup N (X × Y) (x, y)

The product of two homotopy classes, represented by the coordinatewise product of generalized loops.

Equations

• a.prod b = Quotient.map₂ GenLoop.prod ⋯ a b

@[simp]

theorem HomotopyGroup.prod_mk {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)) (q : ↑(GenLoop N Y y)) : prod ⟦p⟧ ⟦q⟧ = ⟦GenLoop.prod p q⟧

@[simp]

theorem HomotopyGroup.map_fst_prod {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (a : HomotopyGroup N X x) (b : HomotopyGroup N Y y) : map ContinuousMap.fst ⋯ (a.prod b) = a

The first-coordinate map sends a product of homotopy classes to its first factor.

@[simp]

theorem HomotopyGroup.map_snd_prod {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (a : HomotopyGroup N X x) (b : HomotopyGroup N Y y) : map ContinuousMap.snd ⋯ (a.prod b) = b

The second-coordinate map sends a product of homotopy classes to its second factor.

@[simp]

theorem HomotopyGroup.prod_map_fst_map_snd {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (a : HomotopyGroup N (X × Y) (x, y)) : (map ContinuousMap.fst ⋯ a).prod (map ContinuousMap.snd ⋯ a) = a

A homotopy class in a product is recovered from its two coordinate classes.

def HomotopyGroup.prodEquiv {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) : HomotopyGroup N (X × Y) (x, y) ≃ HomotopyGroup N X x × HomotopyGroup N Y y

The homotopy group of a binary product is the product of the homotopy groups.

Equations

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

@[simp]

theorem HomotopyGroup.prodEquiv_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) (a : HomotopyGroup N (X × Y) (x, y)) : (prodEquiv x y) a = (map ContinuousMap.fst ⋯ a, map ContinuousMap.snd ⋯ a)

@[simp]

theorem HomotopyGroup.prodEquiv_symm_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) (a : HomotopyGroup N X x × HomotopyGroup N Y y) : (prodEquiv x y).symm a = a.1.prod a.2

def HomotopyGroup.prodMulEquiv {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DecidableEq N] [Nonempty N] (x : X) (y : Y) : HomotopyGroup N (X × Y) (x, y) ≃* HomotopyGroup N X x × HomotopyGroup N Y y

In positive dimensions, the homotopy group of a binary product is multiplicatively equivalent to the product of the homotopy groups.

Equations

• HomotopyGroup.prodMulEquiv x y = { toEquiv := HomotopyGroup.prodEquiv x y, map_mul' := ⋯ }

@[simp]

theorem HomotopyGroup.prodMulEquiv_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DecidableEq N] [Nonempty N] (x : X) (y : Y) (a : HomotopyGroup N (X × Y) (x, y)) : (prodMulEquiv x y) a = (prodEquiv x y) a

@[simp]

theorem HomotopyGroup.prodMulEquiv_symm_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [DecidableEq N] [Nonempty N] (x : X) (y : Y) (a : HomotopyGroup N X x × HomotopyGroup N Y y) : (prodMulEquiv x y).symm a = a.1.prod a.2

@[simp]

theorem HomotopyGroup.prod_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] : prod 1 1 = 1

The coordinatewise product of identity homotopy classes is the identity.

@[simp]

theorem HomotopyGroup.prod_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] (a₁ a₂ : HomotopyGroup N X x) (b₁ b₂ : HomotopyGroup N Y y) : (a₁ * a₂).prod (b₁ * b₂) = a₁.prod b₁ * a₂.prod b₂

Coordinatewise products commute with multiplication of homotopy classes.

noncomputable def HomotopyGroup.pi {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} (a : (i : ι) → HomotopyGroup N (Z i) (z i)) : HomotopyGroup N ((i : ι) → Z i) z

The indexed product of homotopy classes, represented by the coordinatewise product of generalized loops.

Equations

• HomotopyGroup.pi a = Quotient.map GenLoop.pi ⋯ (Quotient.choice a)

@[simp]

theorem HomotopyGroup.pi_mk {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} (p : (i : ι) → ↑(GenLoop N (Z i) (z i))) : (pi fun (i : ι) => ⟦p i⟧) = ⟦GenLoop.pi p⟧

@[simp]

theorem HomotopyGroup.map_eval_pi {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} (a : (i : ι) → HomotopyGroup N (Z i) (z i)) (i : ι) : map (ContinuousMap.eval i) ⋯ (pi a) = a i

Taking a coordinate of an indexed product of homotopy classes recovers that coordinate.

@[simp]

theorem HomotopyGroup.pi_map_eval {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} (a : HomotopyGroup N ((i : ι) → Z i) z) : (pi fun (i : ι) => map (ContinuousMap.eval i) ⋯ a) = a

A homotopy class in an indexed product is recovered from all of its coordinate classes.

noncomputable def HomotopyGroup.piEquiv {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] (z : (i : ι) → Z i) : HomotopyGroup N ((i : ι) → Z i) z ≃ ((i : ι) → HomotopyGroup N (Z i) (z i))

The homotopy group of an indexed product is the indexed product of the homotopy groups.

Equations

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

@[simp]

theorem HomotopyGroup.piEquiv_apply {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] (z : (i : ι) → Z i) (a : HomotopyGroup N ((i : ι) → Z i) z) (i : ι) : (piEquiv z) a i = map (ContinuousMap.eval i) ⋯ a

@[simp]

theorem HomotopyGroup.piEquiv_symm_apply {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] (z : (i : ι) → Z i) (a : (i : ι) → HomotopyGroup N (Z i) (z i)) : (piEquiv z).symm a = pi a

instance HomotopyGroup.subsingleton_pi {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} [∀ (i : ι), Subsingleton (HomotopyGroup N (Z i) (z i))] : Subsingleton (HomotopyGroup N ((i : ι) → Z i) z)

The homotopy group of an indexed product is a subsingleton when every factor homotopy group is a subsingleton.

noncomputable def HomotopyGroup.piMulEquiv {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] [DecidableEq N] [Nonempty N] (z : (i : ι) → Z i) : HomotopyGroup N ((i : ι) → Z i) z ≃* ((i : ι) → HomotopyGroup N (Z i) (z i))

In positive dimensions, the homotopy group of an indexed product is multiplicatively equivalent to the indexed product of the homotopy groups.

Equations

• HomotopyGroup.piMulEquiv z = { toEquiv := HomotopyGroup.piEquiv z, map_mul' := ⋯ }

@[simp]

theorem HomotopyGroup.piMulEquiv_apply {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] [DecidableEq N] [Nonempty N] (z : (i : ι) → Z i) (a : HomotopyGroup N ((i : ι) → Z i) z) (i : ι) : (piMulEquiv z) a i = map (ContinuousMap.eval i) ⋯ a

@[simp]

theorem HomotopyGroup.piMulEquiv_symm_apply {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] [DecidableEq N] [Nonempty N] (z : (i : ι) → Z i) (a : (i : ι) → HomotopyGroup N (Z i) (z i)) : (piMulEquiv z).symm a = pi a

@[simp]

theorem HomotopyGroup.pi_one {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} [DecidableEq N] [Nonempty N] : (pi fun (x : ι) => 1) = 1

The coordinatewise indexed product of identity homotopy classes is the identity.

@[simp]

theorem HomotopyGroup.pi_mul {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} [DecidableEq N] [Nonempty N] (a b : (i : ι) → HomotopyGroup N (Z i) (z i)) : pi (a * b) = pi a * pi b

Coordinatewise indexed products commute with multiplication of homotopy classes.