English
Let φ: F → G be a morphism of cochain complexes admitting a homotopy cofibre. For any γ in Cochain G K d with the degree shift condition 0 + d = e, the composite of the inr-portion with the snd-projection applied to γ recovers γ; i.e., the equation (Cochain.ofHom (inr φ)) ∘ ((snd φ) ∘ γ) equals γ (up to the specified degree shift).
Русский
Пусть φ: F → G — морфизм комплексов сопряжённых коChain, имеющий гомотопическое cofibre. Для любого γ в Cochain G K d удовлетворяющего смещению степеней 0 + d = e, композиция черезinr φ и snd φ восстанавливает γ; то есть (Cochain.ofHom (inr φ)) ∘ ((snd φ) ∘ γ) = γ при соответствующем сдвиге степеней.
LaTeX
$$$\forall \varphi,\ \gamma,\ hij: 0+d=e:\ (Cochain.ofHom (inr\varphi))\circ ((\text{snd}\ \varphi)\circ\gamma\ hij) = \gamma.$$$
Lean4
@[simp]
theorem inr_snd_assoc {K : CochainComplex C ℤ} {d e : ℤ} (γ : Cochain G K d) (he : 0 + d = e) :
(Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) (by simp only [← he, zero_add]) = γ :=
by
obtain rfl : d = e := by cutsat
rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_snd, Cochain.id_comp]
