Simplicial homotopies of simplicial objects

This file defines the notion of a combinatorial simplicial homotopy between two morphisms of simplicial objects.

Main definitions

• Homotopy f g: The type of simplicial homotopies between morphisms f g : X ⟶ Y.
• Homotopy.refl f: The constant homotopy from f to f.

Implementation notes

The definition follows the combinatorial description of simplicial homotopies. Given simplicial objects X Y : SimplicialObject C and morphisms f g : X ⟶ Y, a simplicial homotopy consists of a family of morphisms h n i : X _⦋n⦌ ⟶ Y _⦋n+1⦌ satisfying compatibilities involving the faces and degeneracies.

References

• nLab, Simplicial Homotopy

structure CategoryTheory.SimplicialObject.Homotopy {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} (f g : X ⟶ Y) : Type v

A simplicial homotopy between morphisms f g : X ⟶ Y of simplicial objects consists of a family of morphisms h n i : X _⦋n⦌ ⟶ Y _⦋n + 1⦌ for i : Fin (n + 1), satisfying compatibility conditions with respect to face and degeneracy maps

• h {n : ℕ} (i : Fin (n + 1)) : X.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Y.obj (Opposite.op (SimplexCategory.mk (n + 1)))

  Basic data: h i : Xₙ ⟶ Yₙ₊₁ for i : Fin (n + 1).

• h_zero_comp_δ_zero (n : ℕ) : CategoryStruct.comp (self.h 0) (Y.δ 0) = g.app (Opposite.op (SimplexCategory.mk n))
• h_last_comp_δ_last (n : ℕ) : CategoryStruct.comp (self.h (Fin.last n)) (Y.δ (Fin.last (n + 1))) = f.app (Opposite.op (SimplexCategory.mk n))
• h_succ_comp_δ_castSucc_of_lt {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (hij : i ≤ j.castSucc) : CategoryStruct.comp (self.h j.succ) (Y.δ i.castSucc) = CategoryStruct.comp (X.δ i) (self.h j)
• h_succ_comp_δ_castSucc_succ {n : ℕ} (j : Fin (n + 1)) : CategoryStruct.comp (self.h j.succ) (Y.δ j.castSucc.succ) = CategoryStruct.comp (self.h j.castSucc) (Y.δ j.castSucc.succ)
• h_castSucc_comp_δ_succ_of_lt {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (hji : j.castSucc < i) : CategoryStruct.comp (self.h j.castSucc) (Y.δ i.succ) = CategoryStruct.comp (X.δ i) (self.h j)
• h_comp_σ_castSucc_of_le {n : ℕ} (i j : Fin (n + 1)) (hij : i ≤ j) : CategoryStruct.comp (self.h j) (Y.σ i.castSucc) = CategoryStruct.comp (X.σ i) (self.h j.succ)
• h_comp_σ_succ_of_lt {n : ℕ} (i j : Fin (n + 1)) (hji : j ≤ i) : CategoryStruct.comp (self.h j) (Y.σ i.succ) = CategoryStruct.comp (X.σ i) (self.h j.castSucc)

theorem CategoryTheory.SimplicialObject.Homotopy.ext {C : Type u} {inst✝ : Category.{v, u} C} {X Y : SimplicialObject C} {f g : X ⟶ Y} {x y : Homotopy f g} (h : @h C inst✝ X Y f g x = @h C inst✝ X Y f g y) : x = y

theorem CategoryTheory.SimplicialObject.Homotopy.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {X Y : SimplicialObject C} {f g : X ⟶ Y} {x y : Homotopy f g} : x = y ↔ @h C inst✝ X Y f g x = @h C inst✝ X Y f g y

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.h_last_comp_δ_last_assoc {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (self : Homotopy f g) (n : ℕ) {Z : C} (h : Y.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryStruct.comp (self.h (Fin.last n)) (CategoryStruct.comp (Y.δ (Fin.last (n + 1))) h) = CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) h

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.h_castSucc_comp_δ_succ_of_lt_assoc {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (self : Homotopy f g) {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (hji : j.castSucc < i) {Z : C} (h : Y.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ Z) : CategoryStruct.comp (self.h j.castSucc) (CategoryStruct.comp (Y.δ i.succ) h) = CategoryStruct.comp (X.δ i) (CategoryStruct.comp (self.h j) h)

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_of_lt_assoc {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (self : Homotopy f g) {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (hij : i ≤ j.castSucc) {Z : C} (h : Y.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ Z) : CategoryStruct.comp (self.h j.succ) (CategoryStruct.comp (Y.δ i.castSucc) h) = CategoryStruct.comp (X.δ i) (CategoryStruct.comp (self.h j) h)

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_succ_of_lt_assoc {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (self : Homotopy f g) {n : ℕ} (i j : Fin (n + 1)) (hji : j ≤ i) {Z : C} (h : Y.obj (Opposite.op (SimplexCategory.mk (n + 1 + 1))) ⟶ Z) : CategoryStruct.comp (self.h j) (CategoryStruct.comp (Y.σ i.succ) h) = CategoryStruct.comp (X.σ i) (CategoryStruct.comp (self.h j.castSucc) h)

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.h_zero_comp_δ_zero_assoc {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (self : Homotopy f g) (n : ℕ) {Z : C} (h : Y.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryStruct.comp (self.h 0) (CategoryStruct.comp (Y.δ 0) h) = CategoryStruct.comp (g.app (Opposite.op (SimplexCategory.mk n))) h

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_castSucc_of_le_assoc {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (self : Homotopy f g) {n : ℕ} (i j : Fin (n + 1)) (hij : i ≤ j) {Z : C} (h : Y.obj (Opposite.op (SimplexCategory.mk (n + 1 + 1))) ⟶ Z) : CategoryStruct.comp (self.h j) (CategoryStruct.comp (Y.σ i.castSucc) h) = CategoryStruct.comp (X.σ i) (CategoryStruct.comp (self.h j.succ) h)

theorem CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_succ_assoc {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (self : Homotopy f g) {n : ℕ} (j : Fin (n + 1)) {Z : C} (h : Y.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ Z) : CategoryStruct.comp (self.h j.succ) (CategoryStruct.comp (Y.δ j.castSucc.succ) h) = CategoryStruct.comp (self.h j.castSucc) (CategoryStruct.comp (Y.δ j.castSucc.succ) h)

def CategoryTheory.SimplicialObject.Homotopy.refl {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} (f : X ⟶ Y) : Homotopy f f

The constant homotopy from f to f.

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.refl_h {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} (f : X ⟶ Y) {n✝ : ℕ} (i : Fin (n✝ + 1)) : (refl f).h i = CategoryStruct.comp (X.σ i) (f.app (Opposite.op (SimplexCategory.mk (n✝ + 1))))

def CategoryTheory.SimplicialObject.Homotopy.whiskerRight {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (H : Homotopy f g) {D : Type u'} [Category.{v', u'} D] (F : Functor C D) : Homotopy (((whiskering C D).obj F).map f) (((whiskering C D).obj F).map g)

Postcompose a simplicial homotopy with a functor F : C ⥤ D.

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.whiskerRight_h {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (H : Homotopy f g) {D : Type u'} [Category.{v', u'} D] (F : Functor C D) {n✝ : ℕ} (i : Fin (n✝ + 1)) : (H.whiskerRight F).h i = F.map (H.h i)

def CategoryTheory.SimplicialObject.Homotopy.postcomp {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (H : Homotopy f g) {Y' : SimplicialObject C} (p : Y ⟶ Y') : Homotopy (CategoryStruct.comp f p) (CategoryStruct.comp g p)

Postcompose a simplicial homotopy with a morphism of simplicial objects.

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.postcomp_h {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (H : Homotopy f g) {Y' : SimplicialObject C} (p : Y ⟶ Y') {n✝ : ℕ} (i : Fin (n✝ + 1)) : (H.postcomp p).h i = CategoryStruct.comp (H.h i) (p.app (Opposite.op (SimplexCategory.mk (n✝ + 1))))

def CategoryTheory.SimplicialObject.Homotopy.precomp {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (H : Homotopy f g) {X' : SimplicialObject C} (p : X' ⟶ X) : Homotopy (CategoryStruct.comp p f) (CategoryStruct.comp p g)

Precompose a simplicial homotopy with a morphism of simplicial objects.

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.precomp_h {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (H : Homotopy f g) {X' : SimplicialObject C} (p : X' ⟶ X) {n✝ : ℕ} (i : Fin (n✝ + 1)) : (H.precomp p).h i = CategoryStruct.comp (p.app (Opposite.op (SimplexCategory.mk n✝))) (H.h i)