opcyclesOpIso_hom_toCycles_op — Mathlib

English

The homology map is natural with respect to maps between complexes, compatible with the op-functor and the homology operations.

Русский

Гомологическое отображение естественно по отношению к гомоморфизмам между комплексами и совместимо с операциями в противоположном контексте.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem opcyclesOpIso_hom_toCycles_op : (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j :=
  by
  by_cases hij : c.Rel j i
  · obtain rfl := c.prev_eq' hij
    exact (K.sc i).opcyclesOpIso_hom_toCycles_op
  · rw [K.toCycles_eq_zero hij, K.op.fromOpcycles_eq_zero hij, op_zero, comp_zero]

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