inl_v_d — Mathlib

English

The mapping cone is unital in each degree, with the identity realized as the sum of the fst and inr compositions described above.

Русский

Конус отображения обладает единицей в каждомGrado, равной сумме составляющих fst и inr.

LaTeX

$$$\forall p:\mathbb{Z},\ id_{(mappingCone\varphi)X_p} = (fst\varphi)_{p}\circ inl\varphi + (snd\varphi)_{p}\circ inr\varphi.$$$

Lean4

@[reassoc]
theorem inl_v_d (i j k : ℤ) (hij : i + (-1) = j) (hik : k + (-1) = i) :
    (inl φ).v i j hij ≫ (mappingCone φ).d j i = φ.f i ≫ (inr φ).f i - F.d i k ≫ (inl φ).v _ _ hik :=
  by
  dsimp [mappingCone, inl, inr]
  rw [homotopyCofiber.inlX_d φ j i k (by dsimp; cutsat) (by dsimp; cutsat)]
  abel

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