cocyclesMap_cocyclesIso₀_hom_f — Mathlib

English

A compatibility equality expresses how cocyclesMap interacts with the isomorphism cocyclesIso₀ and the short complex H0 map on degree 0 via φ.

Русский

Эквивалентность совместимости отображения cocyclesMap с изоморфизмом cocyclesIso₀ и отображением короткого комплекса H0 в нулевой степени через φ.

LaTeX

$$$$ cocyclesMap f φ 0 \\\\\\circ (cocyclesIso₀ B).hom \\\\\\circ (shortComplexH0 B).f = (cocyclesIso₀ A).hom \\\\\\circ (shortComplexH0 A).f \\\\\\circ φ.hom $$$$

Lean4

@[reassoc, elementwise]
theorem cocyclesMap_cocyclesIso₀_hom_f :
    cocyclesMap f φ 0 ≫ (cocyclesIso₀ B).hom ≫ (shortComplexH0 B).f =
      (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f ≫ φ.hom :=
  by simp

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