Documentation

Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

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).)

source
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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SSet.RelativeMorphism.botEquiv_apply {X Y : SSet} (f : RelativeMorphism ⊥ ⊥ (Subcomplex.isInitialBot.to ⊥.toSSet)) :
    botEquiv f = f.map
    source
    @[simp]
    theorem SSet.RelativeMorphism.botEquiv_symm_apply_map {X Y : SSet} (f : X ⟶ Y) :
    (botEquiv.symm f).map = f
    source
    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₁.

    Equations
    Instances For
      source
      @[simp]
      theorem SSet.Homotopy.h₀ {X Y : SSet} {f g : X ⟶ Y} (H : Homotopy f g) :
      CategoryTheory.CategoryStruct.comp ι₀ H.h = f
      source
      @[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
      source
      @[simp]
      theorem SSet.Homotopy.h₁ {X Y : SSet} {f g : X ⟶ Y} (H : Homotopy f g) :
      CategoryTheory.CategoryStruct.comp ι₁ H.h = g
      source
      @[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
      source
      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.

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