English
For each p in Z, the endomorphism on (mappingCone φ).X_p given by the canonical splitting equals the identity map: the sum of the two contributions from fst and snd equals id.
Русский
Для каждого p ∈ ℤ, конецоморфизм на (mappingCone φ).X_p, получаемый из канонического разложения, равен тождественному отображению.
LaTeX
$$$\forall p:\mathbb{Z},\ (fst\varphi)_{p}\!\circ inl\varphi + (snd\varphi)_{p}\!\circ inr\varphi = \mathrm{id}_{(mappingCone\varphi)X_p}.$$$
Lean4
theorem id_X (p q : ℤ) (hpq : p + 1 = q) :
(fst φ).1.v p q hpq ≫ (inl φ).v q p (by cutsat) + (snd φ).v p p (add_zero p) ≫ (inr φ).f p =
𝟙 ((mappingCone φ).X p) :=
by
simpa only [Cochain.add_v, Cochain.comp_zero_cochain_v, Cochain.ofHom_v, id_f,
Cochain.comp_v _ _ (add_neg_cancel 1) p q p hpq (by cutsat)] using Cochain.congr_v (id φ) p p (add_zero p)
