alternatingConst_iCycles_even_comp

English

If j is even and i relates to j, then the i-cycles map composed with φ is zero.

Русский

Если j чётно и i Rel j, то композиция iциклы с φ равна нулю.

LaTeX

$$$\text{AltConst}(A, hOdd, hEven, hc).iCycles\, j \;\circ φ = 0$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem alternatingConst_iCycles_even_comp [CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j)
    (hnj : c.Rel j (c.next j)) (h : Even j) : (alternatingConst A hOdd hEven hc).iCycles j ≫ φ = 0 :=
  by
  rw [← cancel_epi (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv]
  simpa [HomologicalComplex.iCycles, -Preadditive.IsIso.comp_left_eq_zero, HomologicalComplex.sc,
    HomologicalComplex.shortComplexFunctor, alternatingConstScIsoEven,
    Category.id_comp (X := (alternatingConst A hOdd hEven hc).X _)] using (ShortComplex.mk ψ φ hEven).iCycles_g

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