Relative homotopy sets of based pairs

Let X be a based pair (X, A, a₀), with A ↪ X a topological pair and a₀ ∈ A. This file defines the relative homotopy set π_{n+1}(X, A, a₀) in the cubical model that Mathlib uses for HomotopyGroup, where n is the cardinality of an index type N.

A relative cube is a continuous map p : I × I^N → X that sends the face {0} × I^N into A, and the rest of the boundary of the cube — the opposite face {1} × I^N and the sides I × ∂I^N — to a₀. This is the classical description of relative homotopy classes as maps (I^{n+1}, ∂I^{n+1}, J^n) → (X, A, a₀); see Hatcher, Algebraic Topology, Section 4.1, where the face mapped to A is also the one where the distinguished coordinate vanishes. Two relative cubes are homotopic when they are joined by a homotopy through relative cubes, which is Mathlib's ContinuousMap.HomotopicWith for the relative-cube predicate. Unlike homotopy of generalized loops, such a homotopy is not stationary on the face {0} × I^N: it may move inside A there.

The resulting type TauCeti.RelHomotopyGroup N X is pointed by the class of the constant cube. Its group structure in dimensions at least two is not constructed here; in particular nothing here makes π_2(X, A, a₀) commutative.

A morphism of based pairs acts by postcomposition, functorially, giving the functor TauCeti.RelHomotopyGroup.functor N : BasedTopPair ⥤ Pointed. Restricting a relative cube to the face {0} × I^N gives a generalized loop in A based at a₀, and hence the boundary map π_{n+1}(X, A, a₀) → π_n(A, a₀), which is natural in the based pair. Finally, a relative cube that lies entirely in A is trivial, by pushing it towards the face {1} × I^N (the easy half of the compression criterion); in particular π_{n+1}(X, X, x₀) is trivial.

Main declarations

• TauCeti.RelGenLoop N X: relative cubes I × I^N → X of the based pair X.
• TauCeti.RelGenLoop.mk: the relative cube given by a continuous map satisfying the face conditions.
• TauCeti.RelGenLoop.Homotopic: homotopy through relative cubes, characterised by TauCeti.RelGenLoop.homotopic_iff.
• TauCeti.RelHomotopyGroup N X: the relative homotopy set π_{n+1}(X, A, a₀), with induced maps TauCeti.RelHomotopyGroup.map and the functor TauCeti.RelHomotopyGroup.functor.
• TauCeti.RelHomotopyGroup.boundary: the boundary map π_{n+1}(X, A, a₀) → π_n(A, a₀), natural by TauCeti.RelHomotopyGroup.boundary_map.
• TauCeti.RelHomotopyGroup.mk_eq_default_of_mem_range: a relative cube with values in A represents the distinguished class.

def TauCeti.RelGenLoop (N : Type v) (X : BasedTopPair) : Set C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)

The relative cubes of the based pair X = (X, A, a₀): continuous maps I × I^N → X sending the face {0} × I^N into A, and the face {1} × I^N and the sides I × ∂I^N to a₀.

theorem TauCeti.RelGenLoop.mem_iff {N : Type v} {X : BasedTopPair} {p : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)} : p ∈ RelGenLoop N X ↔ (∀ (t : N → ↑unitInterval), p (0, t) ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) ∧ ∀ (s : ↑unitInterval) (t : N → ↑unitInterval), s = 1 ∨ t ∈ Cube.boundary N → p (s, t) = (CategoryTheory.ConcreteCategory.hom TopPair.map) X.basepoint

@[instance_reducible]

instance TauCeti.RelGenLoop.instFunLike {N : Type v} {X : BasedTopPair} : FunLike (↑(RelGenLoop N X)) (↑unitInterval × (N → ↑unitInterval)) ↑TopPair.fst

@[simp]

theorem TauCeti.RelGenLoop.coe_coe {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) : ⇑↑p = ⇑p

theorem TauCeti.RelGenLoop.ext {N : Type v} {X : BasedTopPair} {p q : ↑(RelGenLoop N X)} (h : ∀ (y : ↑unitInterval × (N → ↑unitInterval)), p y = q y) : p = q

theorem TauCeti.RelGenLoop.ext_iff {N : Type v} {X : BasedTopPair} {p q : ↑(RelGenLoop N X)} : p = q ↔ ∀ (y : ↑unitInterval × (N → ↑unitInterval)), p y = q y

def TauCeti.RelGenLoop.mk {N : Type v} {X : BasedTopPair} (p : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)) (h₀ : ∀ (t : N → ↑unitInterval), p (0, t) ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) (h₁ : ∀ (s : ↑unitInterval) (t : N → ↑unitInterval), s = 1 ∨ t ∈ Cube.boundary N → p (s, t) = (CategoryTheory.ConcreteCategory.hom TopPair.map) X.basepoint) : ↑(RelGenLoop N X)

The relative cube given by a continuous map I × I^N → X that sends the face {0} × I^N into the subspace, and the face {1} × I^N and the sides I × ∂I^N to the basepoint.

@[simp]

theorem TauCeti.RelGenLoop.coe_mk {N : Type v} {X : BasedTopPair} (p : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)) (h₀ : ∀ (t : N → ↑unitInterval), p (0, t) ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) (h₁ : ∀ (s : ↑unitInterval) (t : N → ↑unitInterval), s = 1 ∨ t ∈ Cube.boundary N → p (s, t) = (CategoryTheory.ConcreteCategory.hom TopPair.map) X.basepoint) : ↑(mk p h₀ h₁) = p

@[simp]

theorem TauCeti.RelGenLoop.mk_apply {N : Type v} {X : BasedTopPair} (p : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)) (h₀ : ∀ (t : N → ↑unitInterval), p (0, t) ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) (h₁ : ∀ (s : ↑unitInterval) (t : N → ↑unitInterval), s = 1 ∨ t ∈ Cube.boundary N → p (s, t) = (CategoryTheory.ConcreteCategory.hom TopPair.map) X.basepoint) (y : ↑unitInterval × (N → ↑unitInterval)) : (mk p h₀ h₁) y = p y

theorem TauCeti.RelGenLoop.apply_zero_mem_range {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) (t : N → ↑unitInterval) : p (0, t) ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)

A relative cube sends the face {0} × I^N into the subspace.

@[simp]

theorem TauCeti.RelGenLoop.apply_one {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) (t : N → ↑unitInterval) : p (1, t) = (CategoryTheory.ConcreteCategory.hom TopPair.map) X.basepoint

A relative cube sends the face {1} × I^N to the basepoint.

theorem TauCeti.RelGenLoop.apply_of_mem_boundary {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) (s : ↑unitInterval) {t : N → ↑unitInterval} (ht : t ∈ Cube.boundary N) : p (s, t) = (CategoryTheory.ConcreteCategory.hom TopPair.map) X.basepoint

A relative cube sends the sides I × ∂I^N to the basepoint.

theorem TauCeti.RelGenLoop.apply_update {N : Type v} {X : BasedTopPair} [DecidableEq N] (p : ↑(RelGenLoop N X)) (s : ↑unitInterval) (t : N → ↑unitInterval) (j : N) {a : ↑unitInterval} (ha : a = 0 ∨ a = 1) : p (s, Function.update t j a) = (CategoryTheory.ConcreteCategory.hom TopPair.map) X.basepoint

A relative cube sends the faces t j = 0 and t j = 1 to the basepoint.

def TauCeti.RelGenLoop.const {N : Type v} {X : BasedTopPair} : ↑(RelGenLoop N X)

The constant relative cube at the basepoint.

@[simp]

theorem TauCeti.RelGenLoop.const_apply {N : Type v} {X : BasedTopPair} (y : ↑unitInterval × (N → ↑unitInterval)) : const y = (CategoryTheory.ConcreteCategory.hom TopPair.map) X.basepoint

@[instance_reducible]

instance TauCeti.RelGenLoop.instInhabitedElemContinuousMapProdRealUnitIntervalForallCarrierFst {N : Type v} {X : BasedTopPair} : Inhabited ↑(RelGenLoop N X)

Homotopy through relative cubes

def TauCeti.RelGenLoop.Homotopic {N : Type v} {X : BasedTopPair} (p q : ↑(RelGenLoop N X)) : Prop

Two relative cubes are homotopic if they are joined by a homotopy all of whose stages are relative cubes. On the face {0} × I^N the homotopy may move inside the subspace.

theorem TauCeti.RelGenLoop.homotopic_iff {N : Type v} {X : BasedTopPair} {p q : ↑(RelGenLoop N X)} : Homotopic p q ↔ (↑p).HomotopicWith ↑q fun (x : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)) => x ∈ RelGenLoop N X

The characteristic property of Homotopic: a homotopy through relative cubes is a homotopy of the underlying continuous maps all of whose stages are relative cubes.

theorem TauCeti.RelGenLoop.Homotopic.refl {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) : Homotopic p p

theorem TauCeti.RelGenLoop.Homotopic.symm {N : Type v} {X : BasedTopPair} ⦃p q : ↑(RelGenLoop N X)⦄ (h : Homotopic p q) : Homotopic q p

theorem TauCeti.RelGenLoop.Homotopic.trans {N : Type v} {X : BasedTopPair} ⦃p q r : ↑(RelGenLoop N X)⦄ (h₀ : Homotopic p q) (h₁ : Homotopic q r) : Homotopic p r

theorem TauCeti.RelGenLoop.Homotopic.equiv {N : Type v} {X : BasedTopPair} : Equivalence Homotopic

@[instance_reducible]

instance TauCeti.RelGenLoop.setoid (N : Type v) (X : BasedTopPair) : Setoid ↑(RelGenLoop N X)

Homotopy through relative cubes, as a setoid.

Functoriality

theorem TauCeti.RelGenLoop.comp_mem {N : Type v} {X Y : BasedTopPair} (f : X ⟶ Y) {p : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)} (hp : p ∈ RelGenLoop N X) : (TopCat.Hom.hom (TopPair.Hom.fst f.toTopPairHom)).comp p ∈ RelGenLoop N Y

Postcomposing with the ambient component of a morphism of based pairs preserves relative cubes.

def TauCeti.RelGenLoop.map {N : Type v} {X Y : BasedTopPair} (f : X ⟶ Y) (p : ↑(RelGenLoop N X)) : ↑(RelGenLoop N Y)

A morphism of based pairs sends relative cubes to relative cubes by postcomposition.

@[simp]

theorem TauCeti.RelGenLoop.map_apply {N : Type v} {X Y : BasedTopPair} (f : X ⟶ Y) (p : ↑(RelGenLoop N X)) (y : ↑unitInterval × (N → ↑unitInterval)) : (map f p) y = (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst f.toTopPairHom)) (p y)

@[simp]

theorem TauCeti.RelGenLoop.map_id {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) : map (CategoryTheory.CategoryStruct.id X) p = p

@[simp]

theorem TauCeti.RelGenLoop.map_map {N : Type v} {X Y Z : BasedTopPair} (f : X ⟶ Y) (g : Y ⟶ Z) (p : ↑(RelGenLoop N X)) : map g (map f p) = map (CategoryTheory.CategoryStruct.comp f g) p

@[simp]

theorem TauCeti.RelGenLoop.map_const {N : Type v} {X Y : BasedTopPair} (f : X ⟶ Y) : map f const = const

theorem TauCeti.RelGenLoop.Homotopic.map {N : Type v} {X Y : BasedTopPair} {p q : ↑(RelGenLoop N X)} (h : Homotopic p q) (f : X ⟶ Y) : Homotopic (RelGenLoop.map f p) (RelGenLoop.map f q)

Postcomposition preserves homotopy through relative cubes.

The face in the subspace

noncomputable def TauCeti.RelGenLoop.boundary {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) : ↑(GenLoop N (↑TopPair.snd) X.basepoint)

The restriction of a relative cube to the face {0} × I^N, as a generalized loop in the subspace based at the basepoint.

@[simp]

theorem TauCeti.RelGenLoop.map_boundary_apply {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) (t : N → ↑unitInterval) : (CategoryTheory.ConcreteCategory.hom TopPair.map) ((boundary p) t) = p (0, t)

theorem TauCeti.RelGenLoop.boundary_apply_eq_iff {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) (t : N → ↑unitInterval) (a : ↑TopPair.snd) : (boundary p) t = a ↔ p (0, t) = (CategoryTheory.ConcreteCategory.hom TopPair.map) a

@[simp]

theorem TauCeti.RelGenLoop.boundary_const {N : Type v} {X : BasedTopPair} : boundary const = GenLoop.const

theorem TauCeti.RelGenLoop.boundary_map {N : Type v} {X Y : BasedTopPair} (f : X ⟶ Y) (p : ↑(RelGenLoop N X)) : boundary (map f p) = GenLoop.map (TopCat.Hom.hom (TopPair.Hom.snd f.toTopPairHom)) ⋯ (boundary p)

Restricting to the face {0} × I^N commutes with the action of morphisms of based pairs.

theorem TauCeti.RelGenLoop.Homotopic.boundary {N : Type v} {X : BasedTopPair} {p q : ↑(RelGenLoop N X)} (h : Homotopic p q) : GenLoop.Homotopic (RelGenLoop.boundary p) (RelGenLoop.boundary q)

A homotopy through relative cubes restricts on the face {0} × I^N to a homotopy of generalized loops in the subspace, relative to the cube boundary.

theorem TauCeti.RelGenLoop.homotopic_const_of_mem_range {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) (hp : ∀ (y : ↑unitInterval × (N → ↑unitInterval)), p y ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) : Homotopic p const

A relative cube with all of its values in the subspace is homotopic, through relative cubes, to the constant cube: push it towards the face {1} × I^N.

def TauCeti.RelHomotopyGroup (N : Type v) (X : BasedTopPair) : Type (max u v)

The relative homotopy set π_{n+1}(X, A, a₀) of a based pair X = (X, A, a₀), where n is the cardinality of N: relative cubes I × I^N → X up to homotopy through relative cubes.

def TauCeti.RelHomotopyGroup.mk {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) : RelHomotopyGroup N X

The class of a relative cube.

theorem TauCeti.RelHomotopyGroup.mk_surjective {N : Type v} {X : BasedTopPair} : Function.Surjective mk

theorem TauCeti.RelHomotopyGroup.mk_eq_mk {N : Type v} {X : BasedTopPair} {p q : ↑(RelGenLoop N X)} : mk p = mk q ↔ RelGenLoop.Homotopic p q

def TauCeti.RelHomotopyGroup.lift {N : Type v} {X : BasedTopPair} {β : Sort u_1} (f : ↑(RelGenLoop N X) → β) (hf : ∀ (p q : ↑(RelGenLoop N X)), RelGenLoop.Homotopic p q → f p = f q) : RelHomotopyGroup N X → β

Lift a function on relative cubes that is invariant under homotopy through relative cubes to the relative homotopy set.

@[simp]

theorem TauCeti.RelHomotopyGroup.lift_mk {N : Type v} {X : BasedTopPair} {β : Sort u_1} (f : ↑(RelGenLoop N X) → β) (hf : ∀ (p q : ↑(RelGenLoop N X)), RelGenLoop.Homotopic p q → f p = f q) (p : ↑(RelGenLoop N X)) : lift f hf (mk p) = f p

def TauCeti.RelHomotopyGroup.lift₂ {N : Type v} {X : BasedTopPair} {N' : Type u_1} {X' : BasedTopPair} {β : Sort u_2} (f : ↑(RelGenLoop N X) → ↑(RelGenLoop N' X') → β) (hf : ∀ (p₁ : ↑(RelGenLoop N X)) (q₁ : ↑(RelGenLoop N' X')) (p₂ : ↑(RelGenLoop N X)) (q₂ : ↑(RelGenLoop N' X')), RelGenLoop.Homotopic p₁ p₂ → RelGenLoop.Homotopic q₁ q₂ → f p₁ q₁ = f p₂ q₂) : RelHomotopyGroup N X → RelHomotopyGroup N' X' → β

Lift a function of two relative cubes that is invariant under homotopy through relative cubes in each argument to a function of two relative homotopy classes.

@[simp]

theorem TauCeti.RelHomotopyGroup.lift₂_mk {N : Type v} {X : BasedTopPair} {N' : Type u_1} {X' : BasedTopPair} {β : Sort u_2} (f : ↑(RelGenLoop N X) → ↑(RelGenLoop N' X') → β) (hf : ∀ (p₁ : ↑(RelGenLoop N X)) (q₁ : ↑(RelGenLoop N' X')) (p₂ : ↑(RelGenLoop N X)) (q₂ : ↑(RelGenLoop N' X')), RelGenLoop.Homotopic p₁ p₂ → RelGenLoop.Homotopic q₁ q₂ → f p₁ q₁ = f p₂ q₂) (p : ↑(RelGenLoop N X)) (q : ↑(RelGenLoop N' X')) : lift₂ f hf (mk p) (mk q) = f p q

@[instance_reducible]

instance TauCeti.RelHomotopyGroup.instInhabited {N : Type v} {X : BasedTopPair} : Inhabited (RelHomotopyGroup N X)

The relative homotopy set is pointed by the class of the constant cube.

theorem TauCeti.RelHomotopyGroup.default_eq {N : Type v} {X : BasedTopPair} : default = mk RelGenLoop.const

def TauCeti.RelHomotopyGroup.map {N : Type v} {X Y : BasedTopPair} (f : X ⟶ Y) : RelHomotopyGroup N X → RelHomotopyGroup N Y

The map on relative homotopy sets induced by a morphism of based pairs.

@[simp]

theorem TauCeti.RelHomotopyGroup.map_mk {N : Type v} {X Y : BasedTopPair} (f : X ⟶ Y) (p : ↑(RelGenLoop N X)) : map f (mk p) = mk (RelGenLoop.map f p)

@[simp]

theorem TauCeti.RelHomotopyGroup.map_id {N : Type v} {X : BasedTopPair} : map (CategoryTheory.CategoryStruct.id X) = id

theorem TauCeti.RelHomotopyGroup.map_comp {N : Type v} {X Y Z : BasedTopPair} (f : X ⟶ Y) (g : Y ⟶ Z) : map (CategoryTheory.CategoryStruct.comp f g) = map g ∘ map f

@[simp]

theorem TauCeti.RelHomotopyGroup.map_map {N : Type v} {X Y Z : BasedTopPair} (f : X ⟶ Y) (g : Y ⟶ Z) (a : RelHomotopyGroup N X) : map g (map f a) = map (CategoryTheory.CategoryStruct.comp f g) a

@[simp]

theorem TauCeti.RelHomotopyGroup.map_default {N : Type v} {X Y : BasedTopPair} (f : X ⟶ Y) : map f default = default

theorem TauCeti.RelHomotopyGroup.subsingleton_of_comp_eq_id {N : Type v} {X Y : BasedTopPair} {f : X ⟶ Y} {g : Y ⟶ X} (h : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X) [Subsingleton (RelHomotopyGroup N Y)] : Subsingleton (RelHomotopyGroup N X)

If a based pair X is a retract of a based pair Y, and the relative homotopy set of Y is trivial, then so is the relative homotopy set of X: the map induced by the inclusion is injective, since the retraction induces a left inverse.

def TauCeti.RelHomotopyGroup.functor (N : Type v) : CategoryTheory.Functor BasedTopPair Pointed

Relative homotopy sets as a functor from based pairs to pointed types.

@[simp]

theorem TauCeti.RelHomotopyGroup.functor_obj (N : Type v) (X : BasedTopPair) : (functor N).obj X = { X := RelHomotopyGroup N X, point := default }

@[simp]

theorem TauCeti.RelHomotopyGroup.functor_map_toFun (N : Type v) {X✝ Y✝ : BasedTopPair} (f : X✝ ⟶ Y✝) (a✝ : RelHomotopyGroup N X✝) : ((functor N).map f).toFun a✝ = map f a✝

noncomputable def TauCeti.RelHomotopyGroup.boundary {N : Type v} {X : BasedTopPair} : RelHomotopyGroup N X → HomotopyGroup N (↑TopPair.snd) X.basepoint

The boundary map π_{n+1}(X, A, a₀) → π_n(A, a₀), restricting a relative cube to the face that lies in the subspace.

@[simp]

theorem TauCeti.RelHomotopyGroup.boundary_mk {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) : (mk p).boundary = ⟦RelGenLoop.boundary p⟧

@[simp]

theorem TauCeti.RelHomotopyGroup.boundary_default {N : Type v} {X : BasedTopPair} : default.boundary = ⟦GenLoop.const⟧

theorem TauCeti.RelHomotopyGroup.boundary_map {N : Type v} {X Y : BasedTopPair} (f : X ⟶ Y) (a : RelHomotopyGroup N X) : (map f a).boundary = HomotopyGroup.map (TopCat.Hom.hom (TopPair.Hom.snd f.toTopPairHom)) ⋯ a.boundary

The boundary map is natural in the based pair.

theorem TauCeti.RelHomotopyGroup.mk_eq_default_of_mem_range {N : Type v} {X : BasedTopPair} (p : ↑(RelGenLoop N X)) (hp : ∀ (y : ↑unitInterval × (N → ↑unitInterval)), p y ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) : mk p = default

A relative cube with all of its values in the subspace represents the distinguished class.

theorem TauCeti.RelHomotopyGroup.subsingleton_of_surjective {N : Type v} {X : BasedTopPair} (h : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) : Subsingleton (RelHomotopyGroup N X)

If the subspace is all of the space, every relative homotopy class is trivial.