homologyOp_hom_naturality — Mathlib

English

The homology op and homology maps are compatible with the opposite construction and with the map φ.

Русский

Гомологическое отображение в противоположном контексте совместимо с конструкциями противоположности и отображением φ.

LaTeX

$$homologyMap ((opFunctor _ _).map φ.op) _ ≫ (K.homologyOp i).hom = (L.homologyOp i).hom ≫ (homologyMap φ i).op$$

Lean4

@[reassoc]
theorem homologyOp_hom_naturality :
    homologyMap ((opFunctor _ _).map φ.op) _ ≫ (K.homologyOp i).hom = (L.homologyOp i).hom ≫ (homologyMap φ i).op :=
  ShortComplex.homologyOpIso_hom_naturality ((shortComplexFunctor V c i).map φ)

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