inl_snd_assoc — Mathlib

English

Canonical isomorphisms exist between shifted Hom complexes and their images under functors after mapping cone constructions, preserving the homotopical information.

Русский

Существуют канонические изоморфизмы между смещёнными Hom-комплексами и их отображениями после конструкций mapping cone, сохраняющие гомотопическую информацию.

LaTeX

$$$\mathrm{mappingCone}\;φ \cong \mathrm{HomComplex}(F,G)^{[a]}.$$$

Lean4

@[simp]
theorem inl_snd_assoc {K : CochainComplex C ℤ} {d e f : ℤ} (γ : Cochain G K d) (he : 0 + d = e) (hf : -1 + e = f) :
    (inl φ).comp ((snd φ).comp γ he) hf = 0 :=
  by
  obtain rfl : e = d := by cutsat
  rw [← Cochain.comp_assoc_of_second_is_zero_cochain, inl_snd, Cochain.zero_comp]

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