descIdHomotopy — Mathlib

English

The descent of the identity morphism is homotopic to the identity on the cocomplex, i.e., the descent of id_X along I,J yields a homotopy between desc id_X I I and id on I.cocomplex.

Русский

Спуск тождественного морфизма равен гомотопии к тождественному отображению на кококомплексе.

LaTeX

$$descIdHomotopy(X,I) = Homotopy (desc (id X) I I) (id I.cocomplex)$$

Lean4

/-- The descent of the identity morphism is homotopic to the identity cochain map. -/
def descIdHomotopy (X : C) (I : InjectiveResolution X) : Homotopy (desc (𝟙 X) I I) (𝟙 I.cocomplex) := by
  apply descHomotopy (𝟙 X) <;> simp

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