alternatingConst_iCycles_odd_comp

English

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

Русский

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

LaTeX

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

Lean4

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

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