chainsMap_f_1_comp_chainsIso₁ — Mathlib

English

The short complex map with identity on G and trivial φ is the identity on the short complex H1.

Русский

Отображение короткого комплекса с тождественным действием на G и тривиальным φ есть тождественность на коротком комплексе H1.

LaTeX

$$$\mathrm{mapShortComplexH1}(\mathrm{Id}_G, \mathrm{id}_A) = \mathrm{Id}$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem chainsMap_f_1_comp_chainsIso₁ :
    (chainsMap f φ).f 1 ≫ (chainsIso₁ B).hom = (chainsIso₁ A).hom ≫ chainsMap₁ f φ :=
  by
  ext x
  simp [chainsMap_f, chainsIso₁]

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