Simplicial homotopies

In this file, we define the notion of homotopy (SSet.Homotopy) between morphisms f : X ⟶ Y and g : X ⟶ Y of simplicial sets: it involves a morphism X ⊗ Δ[1] ⟶ Y inducing both f and g. (This definition is a particular case of SSet.RelativeMorphism.Homotopy that is defined in the file Mathlib/AlgebraicTopology/SimplicialSet/RelativeMorphism.lean). We show that from H : SSet.Homotopy f g, we can obtain a combinatorial homotopy SimplicialObject.Homotopy f g (where the data involve a family of maps X _⦋n⦌ → Y _⦋n + 1⦌ for all n : ℕ and i : Fin (n + 1).)

def SSet.RelativeMorphism.botEquiv {X Y : SSet} : RelativeMorphism ⊥ ⊥ (Subcomplex.isInitialBot.to ⊥.toSSet) ≃ (X ⟶ Y)

Morphisms relatively to the ⊥ subcomplexes of X and Y identify to morphisms X ⟶ Y.

@[simp]

theorem SSet.RelativeMorphism.botEquiv_symm_apply_map {X Y : SSet} (f : X ⟶ Y) : (botEquiv.symm f).map = f

@[simp]

theorem SSet.RelativeMorphism.botEquiv_apply {X Y : SSet} (f : RelativeMorphism ⊥ ⊥ (Subcomplex.isInitialBot.to ⊥.toSSet)) : botEquiv f = f.map

def SSet.Homotopy {X Y : SSet} (f g : X ⟶ Y) : Type u

The type of homotopies between morphisms X ⟶ Y of simplicial sets. The data consists of a morphism h : X ⊗ Δ[1] ⟶ Y which induces both f and g, see the lemmas SSet.Homotopy.h₀ and SSet.Homotopy.h₁.

@[simp]

theorem SSet.Homotopy.h₀ {X Y : SSet} {f g : X ⟶ Y} (H : Homotopy f g) : CategoryTheory.CategoryStruct.comp ι₀ H.h = f

@[simp]

theorem SSet.Homotopy.h₀_assoc {X Y : SSet} {f g : X ⟶ Y} (H : Homotopy f g) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp H.h h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem SSet.Homotopy.h₁ {X Y : SSet} {f g : X ⟶ Y} (H : Homotopy f g) : CategoryTheory.CategoryStruct.comp ι₁ H.h = g

@[simp]

theorem SSet.Homotopy.h₁_assoc {X Y : SSet} {f g : X ⟶ Y} (H : Homotopy f g) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp H.h h) = CategoryTheory.CategoryStruct.comp g h

noncomputable def SSet.Homotopy.toSimplicialObjectHomotopy {X Y : SSet} {f g : X ⟶ Y} (H : Homotopy f g) : CategoryTheory.SimplicialObject.Homotopy f g

If H : Homotopy f g is a homotopy between morphisms of simplicial sets f : X ⟶ Y and g : X ⟶ Y (i.e. H.h is a morphism X ⊗ Δ[1] ⟶ Y inducing f and g), then this is the corresponding (combinatorial) homotopy of morphisms of simplicial objects between f and g.