def HomotopyTheory.Homotopy {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f₀ f₁ : C(X, Y)) : Type (max u_2 u_1)

Definition 5.1 (Homotopy). A homotopy from f₀ to f₁ is a continuous map h : X × I → Y satisfying h(x, 0) = f₀(x) and h(x, 1) = f₁(x). Here it is realized as the Mathlib datum ContinuousMap.Homotopy f₀ f₁.

def HomotopyTheory.Homotopic {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f₀ f₁ : C(X, Y)) : Prop

The proposition that f₀ and f₁ are homotopic, written f₀ ≃ f₁ in the textbook (Definition 5.1).

@[implicit_reducible]

instance HomotopyCategory.homotopicSetoid (X Y : TopCat) : Setoid C(↑X, ↑Y)

The setoid on C(X, Y) for which two continuous maps are identified iff they are homotopic. Used to form the morphisms of the homotopy category.

def HomotopyCategory.HoTop : Type (u₀ + 1)

Definition 5.3 (Homotopy category). HoTop is the homotopy category of topological spaces: same objects as Top, but with morphisms Top(X, Y) / ≃ given by homotopy classes of continuous maps.

@[implicit_reducible]

instance HomotopyCategory.HoTop.instCoeSortType : CoeSort HoTop (Type u₀)

An object of HoTop may be coerced to its underlying type.

@[implicit_reducible]

instance HomotopyCategory.HoTop.instTopologicalSpaceCarrier (X : HoTop) : TopologicalSpace ↑X

The topology on the underlying type of an object of HoTop.

def HomotopyCategory.HoTop.of (X : Type u₀) [TopologicalSpace X] : HoTop

Bundle a topological space X as an object of the homotopy category HoTop.

@[implicit_reducible]

instance HomotopyCategory.HoTop.instCategoryStruct : CategoryTheory.CategoryStruct.{u₀, u₀ + 1} HoTop

Categorical data on HoTop: morphisms X ⟶ Y are homotopy classes of continuous maps, identities are the classes of id, and composition is induced from composition of representatives (well-defined because homotopy is compatible with composition).

@[implicit_reducible]

instance HomotopyCategory.HoTop.instCategory : CategoryTheory.Category.{u₀, u₀ + 1} HoTop

HoTop is a category: composition is associative and the homotopy classes of identities act as left and right units.

@[reducible, inline]

abbrev HomotopyTheory.IsContractible (X : Type u_1) [TopologicalSpace X] : Prop

Definition 5.6 (Contractible). A space X is contractible if the unique map X → * is a homotopy equivalence; equivalently, X is homotopy equivalent to a point. Realized here as Mathlib's ContractibleSpace.

@[reducible, inline]

abbrev HomotopyTheory.HomotopyEquivalence (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] : Type (max u_1 u_2)

Definition 5.4 (Homotopy equivalence). A homotopy equivalence between X and Y is a pair of continuous maps f : X → Y and g : Y → X with g ∘ f ≃ idₓ and f ∘ g ≃ id_Y. Bundled here as Mathlib's ContinuousMap.HomotopyEquiv.

def HomotopyEquivalence.IsHomotopyEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : Prop

A continuous map f : X → Y is a homotopy equivalence (Definition 5.4) iff there exists g : Y → X such that g ∘ f ≃ idₓ and f ∘ g ≃ id_Y.

@[reducible, inline]

abbrev HomotopyInvariance.ChainHomotopy {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f₀ f₁ : C ⟶ D) : Type (max u_1 v)

Definition 5.9 (Chain homotopy). A chain homotopy between two chain maps f₀, f₁ : C → D is a family of maps h : Cₙ → Dₙ₊₁ such that dh + hd = f₁ - f₀. Realized here as Mathlib's Homotopy of HomologicalComplex maps.

theorem HomotopyInvariance.chainHomotopy_homologyMap_eq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f₀ f₁ : C ⟶ D} (h : ChainHomotopy f₀ f₁) (i : ι) [C.HasHomology i] [D.HasHomology i] : HomologicalComplex.homologyMap f₀ i = HomologicalComplex.homologyMap f₁ i

Lemma 5.10. Chain-homotopic chain maps induce the same map on homology: if f₀, f₁ : C → D are chain homotopic, then H_n(f₀) = H_n(f₁).

noncomputable def HomotopyInvariance.homotopyEquivHomologyIso {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (e : HomotopyEquiv C D) (i : ι) [C.HasHomology i] [D.HasHomology i] : C.homology i ≅ D.homology i

A chain homotopy equivalence between chain complexes C and D induces an isomorphism on i-th homology (a consequence of Lemma 5.10).

theorem HomotopyInvariance.homotopy_invariance_of_homology {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.CategoryWithHomology C] {X Y : TopCat} {f g : X ⟶ Y} (H : TopCat.Homotopy f g) (R : C) (n : ℕ) : ((AlgebraicTopology.singularHomologyFunctor C n).obj R).map f = ((AlgebraicTopology.singularHomologyFunctor C n).obj R).map g

Theorem 5.2 (Homotopy invariance of homology). Homotopic continuous maps f, g : X → Y induce the same map on singular homology. Combined with Proposition 5.11 (homotopic maps yield chain-homotopic chain maps) and Lemma 5.10 (chain-homotopic maps induce the same homology map).

noncomputable def HomotopyTheory.homotopyEquivHomologyIso {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (e : ContinuousMap.HomotopyEquiv X Y) {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) (n : ℕ) : ((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj (TopCat.of X) ≅ ((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj (TopCat.of Y)

Corollary 5.5. A homotopy equivalence of topological spaces X ≃ Y induces an isomorphism on n-th singular homology (with coefficients in R).

structure DeformationRetract.IsDeformationRetract {X : Type u} [TopologicalSpace X] (A : Set X) : Type u

Definition 5.8 (Deformation retract). An inclusion A ↪ X is a deformation retract if there is a continuous map h : X × I → X such that h(x, 0) = x, h(x, 1) ∈ A for all x, and h(a, t) = a for all a ∈ A and t ∈ I. This is packaged as a retract X → X landing in A together with a relative homotopy from the identity to the retract, fixing A pointwise.

• retract : C(X, X)
• retract_mem (x : X) : self.retract x ∈ A
• homotopy : (ContinuousMap.id X).HomotopyRel self.retract A

@[reducible, inline]

abbrev HomotopyTheory.IsStarShaped {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (b : E) (s : Set E) : Prop

Definition 5.12 (Star-shaped). A subset s ⊆ E is star-shaped with respect to b ∈ s if for every x ∈ s the segment {tb + (1-t)x : t ∈ [0,1]} lies in s. Realized as Mathlib's StarConvex ℝ b s.

def HomotopyTheory.topConstAt {X : TopCat} (b : ↑X) : X ⟶ X

The continuous self-map of X constant at the point b ∈ X.

def HomotopyTheory.topProjToPoint (X : TopCat) : X ⟶ TopCat.of PUnit.{1}

The unique continuous projection X → * to the one-point space.

def HomotopyTheory.topInclFromPoint {X : TopCat} (b : ↑X) : TopCat.of PUnit.{1} ⟶ X

The continuous inclusion * → X of the one-point space picking out b ∈ X.

theorem HomotopyTheory.isZero_singularHomology_of_contractibleSpace {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) (n : ℕ) (hn : n ≠ 0) (X : TopCat) [ContractibleSpace ↑X] : CategoryTheory.Limits.IsZero (((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj X)

Corollary 5.7 (positive-degree part). If X is contractible then H_n(X) = 0 for all n ≠ 0. Proved by factoring the identity through a point and using homotopy invariance plus the vanishing of higher homology of a point.

noncomputable def HomotopyTheory.singularChainHomotopyEquivOfHomotopyEquiv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (e : ContinuousMap.HomotopyEquiv X Y) (R : C) : HomotopyEquiv (((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj (TopCat.of X)) (((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj (TopCat.of Y))

A homotopy equivalence of topological spaces X ≃ Y lifts to a chain homotopy equivalence of singular chain complexes. This is the chain-level form of Corollary 5.5, combining Theorem 5.2 / Proposition 5.11 with the definition of homotopy equivalence.

noncomputable def HomotopyTheory.starShaped_singularHomology {E : Type} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {s : Set E} {b : E} (hstar : StarConvex ℝ b s) (hne : s.Nonempty) : HomotopyEquiv (((AlgebraicTopology.singularChainComplexFunctor AddCommGrpCat).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of ↑s)) ((ChainComplex.single₀ AddCommGrpCat).obj (AddCommGrpCat.of ℤ))

Proposition 5.13. For a nonempty star-shaped subset s of a real topological vector space, the singular chain complex S_*(s; ℤ) is chain-homotopy equivalent to the chain complex ℤ concentrated in degree zero. Combines contractibility of s with the chain-level homotopy invariance and identification of S_*(*) with ℤ.

noncomputable def HomotopyInvariance.singularChainHomotopy_of_homotopy {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (H : TopCat.Homotopy f₀ f₁) (R : C) : Homotopy (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map f₀) (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map f₁)

Proposition 5.11. A homotopy H : f₀ ≃ f₁ between continuous maps X → Y determines a natural chain homotopy between the induced chain maps f₀*, f₁* : S_*(X) → S_*(Y).

theorem HomotopyInvariance.nonempty_singularChainHomotopy_of_homotopy {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (H : TopCat.Homotopy f₀ f₁) (R : C) : Nonempty (Homotopy (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map f₀) (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map f₁))

The "nonempty" form of Proposition 5.11: there exists a chain homotopy between the induced chain maps f₀*, f₁* : S_*(X) → S_*(Y) whenever f₀ and f₁ are homotopic.