homologyι_truncGE'XIsoOpcycles_inv_d

English

If K.isStrictlySupported along e', then (K.truncGE e).IsStrictlySupported e'.

Русский

Если K строго поддержан по e', тогда (K.truncGE e) тоже строго поддержан по e'.

LaTeX

$$$(K\mathrm{truncGE} e).\mathrm{IsStrictlySupported}(e')$$$

Lean4

theorem homologyι_truncGE'XIsoOpcycles_inv_d :
    (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0 :=
  by
  by_cases hjk : c.Rel j k
  ·
    rw [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj, assoc, Iso.inv_hom_id_assoc, homologyι_comp_fromOpcycles_assoc,
      zero_comp]
  · rw [shape _ _ _ hjk, comp_zero]

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