hasHomology — Mathlib

English

The composition of the i-th pOpcycles map with the restriction-opcycles isomorphism equals the composition of the restrictionXIso with pOpcycles.

Русский

Сочетание i-й карты pOpcycles с изоморфизмом restrictionOpcyclesIso равно композиции restrictionXIso с pOpcycles.

LaTeX

$$$$ (K.restriction e).pOpcycles j \;\circ\; (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom = (K.restrictionXIso e hj').hom \circ K.pOpcycles j $$$$

Lean4

theorem hasHomology [K.HasHomology j'] : (K.restriction e).HasHomology j :=
  ShortComplex.hasHomology_of_iso
    (K.isoSc' i' j' k' hi'' hk'' ≪≫
      (sc'Iso K e i j k hi' hj' hk' hi'' hk'').symm ≪≫ ((K.restriction e).isoSc' i j k hi hk).symm)

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