descCompHomotopy — Mathlib

English

The descent of a composition is homotopic to the composition of the descents: desc (f ≫ g) K I is homotopic to (desc f J I) ≫ (desc g K J).

Русский

Спуск композиции есть гомотопия к композиции спусков: desc (f ∘ g) K I гомотопичен к (desc f J I) ∘ (desc g K J).

LaTeX

$$desc (f ≫ g) K I \; \sim_{hom} \; (desc f J I) ≫ (desc g K J)$$

Lean4

/-- The descent of a composition is homotopic to the composition of the descents. -/
def descCompHomotopy {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (I : InjectiveResolution X) (J : InjectiveResolution Y)
    (K : InjectiveResolution Z) : Homotopy (desc (f ≫ g) K I) (desc f J I ≫ desc g K J) := by
  apply descHomotopy (f ≫ g) <;>
    simp
      -- We don't care about the actual definitions of these homotopies.

Похожие утверждения