inl_fst_assoc — Mathlib

English

There exists a generic IsHomological instance for the Up-shift homology functor across all integers, enabling uniform management of shifted homology theories.

Русский

Существует общий экземпляр IsHomological для функторной гомологии при сдвиге вверх по всем целым, позволяя единообразно управлять сдвинутыми гомологическими теориями.

LaTeX

$$$\forall n\in\mathbb{Z},\; (\mathrm{homologyFunctor}\; \text{Up})_n \text{ is IsHomological}.$$$

Lean4

@[simp]
theorem inl_fst_assoc {K : CochainComplex C ℤ} {d e : ℤ} (γ : Cochain F K d) (he : 1 + d = e) :
    (inl φ).comp ((fst φ).1.comp γ he) (by rw [← he, neg_add_cancel_left]) = γ := by
  rw [← Cochain.comp_assoc _ _ _ (neg_add_cancel 1) (by cutsat) (by cutsat), inl_fst, Cochain.id_comp]

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