Based topological pairs

Relative homology is a functor on Mathlib's category TopPair of embeddings A ↪ X, with no basepoint. Relative homotopy groups π_n(X, A, a₀) instead need a basepoint, and that basepoint must lie in the subspace A: the boundary map π_n(X, A, a₀) → π_{n-1}(A, a₀) lands in a homotopy group of A based at a₀. This file introduces the corresponding carrier.

A TauCeti.BasedTopPair is a TopPair together with an actual point of its subspace, and a morphism of based pairs is a morphism of pairs whose subspace component preserves that point. In particular the pair (X, ∅) admits no based structure, and no declaration chooses a point from a bare pair.

Main declarations

• TauCeti.BasedTopPair: a topological pair with a basepoint in its subspace.
• TauCeti.BasedTopPair.Hom: basepoint-preserving maps of pairs, forming the category TauCeti.BasedTopPair with faithful forgetful functor TauCeti.BasedTopPair.forget to TopPair.

structure TauCeti.BasedTopPair : Type (u + 1)

A based topological pair: a topological pair A ↪ X together with a basepoint lying in the subspace A. This is the carrier of relative homotopy groups π_n(X, A, a₀).

• pair : TopPair

  The underlying topological pair.

• basepoint : ↑TopPair.snd

  The basepoint, a point of the subspace.

structure TauCeti.BasedTopPair.Hom (X Y : BasedTopPair) : Type u

A morphism of based pairs: a map of the underlying pairs whose subspace component preserves the basepoint.

• toTopPairHom : X.pair ⟶ Y.pair

  The underlying map of topological pairs.

• map_basepoint : (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.snd self.toTopPairHom)) X.basepoint = Y.basepoint

  The subspace component sends the basepoint to the basepoint.

theorem TauCeti.BasedTopPair.Hom.ext {X Y : BasedTopPair} {x y : X.Hom Y} (toTopPairHom : x.toTopPairHom = y.toTopPairHom) : x = y

theorem TauCeti.BasedTopPair.Hom.ext_iff {X Y : BasedTopPair} {x y : X.Hom Y} : x = y ↔ x.toTopPairHom = y.toTopPairHom

@[instance_reducible]

instance TauCeti.BasedTopPair.instCategory : CategoryTheory.Category.{u, u + 1} BasedTopPair

theorem TauCeti.BasedTopPair.hom_ext {X Y : BasedTopPair} {f g : X ⟶ Y} (h : f.toTopPairHom = g.toTopPairHom) : f = g

theorem TauCeti.BasedTopPair.hom_ext_iff {X Y : BasedTopPair} {f g : X ⟶ Y} : f = g ↔ f.toTopPairHom = g.toTopPairHom

@[simp]

theorem TauCeti.BasedTopPair.id_toTopPairHom (X : BasedTopPair) : (CategoryTheory.CategoryStruct.id X).toTopPairHom = CategoryTheory.CategoryStruct.id X.pair

@[simp]

theorem TauCeti.BasedTopPair.comp_toTopPairHom {X Y Z : BasedTopPair} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).toTopPairHom = CategoryTheory.CategoryStruct.comp f.toTopPairHom g.toTopPairHom

@[simp]

theorem TauCeti.BasedTopPair.Hom.fst_map_basepoint {X Y : BasedTopPair} (f : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst f.toTopPairHom)) ((CategoryTheory.ConcreteCategory.hom TopPair.map) X.basepoint) = (CategoryTheory.ConcreteCategory.hom TopPair.map) Y.basepoint

The ambient component of a morphism of based pairs sends the basepoint (viewed in the ambient space) to the basepoint.

def TauCeti.BasedTopPair.forget : CategoryTheory.Functor BasedTopPair TopPair

The functor forgetting the basepoint of a based pair.

@[simp]

theorem TauCeti.BasedTopPair.forget_obj (X : BasedTopPair) : forget.obj X = X.pair

@[simp]

theorem TauCeti.BasedTopPair.forget_map {X✝ Y✝ : BasedTopPair} (f : X✝ ⟶ Y✝) : forget.map f = f.toTopPairHom

instance TauCeti.BasedTopPair.instFaithfulTopPairForget : forget.Faithful