English
For i, j, k with i related to j and j related to k and j even, the i-j-k short complex of the alternating-constant complex is isomorphic to the short complex with ψ, φ and hEven, i.e., the middle map is ψ and the next is φ.
Русский
Для i, j, k с i~j, j~k и j чётно, соответствующий i-j-k короткий комплекс чредного константного комплекса изоморфен короткому комплексу с мапами ψ, φ и условием hEven.
LaTeX
$$$\text{AltConstScIsoEven}(A, hOdd, hEven, hc)\;:\; (\mathrm{alternatingConst}\; A\; hOdd\; hEven\; hc)\;\mathrm{sc'}\; i\; j\; k \cong \mathrm{ShortComplex.mk}\; ψ\; φ\; hEven$$$
Lean4
/-- The `i, j, k`th short complex associated to the alternating constant complex on `φ, ψ : A ⟶ A`
is `A --ψ--> A --φ--> A` when `i ~ j, j ~ k` and `j` is even. -/
noncomputable def alternatingConstScIsoEven {i j k : ℕ} (hij : c.Rel i j) (hjk : c.Rel j k) (h : Even j) :
(alternatingConst A hOdd hEven hc).sc' i j k ≅ ShortComplex.mk ψ φ hEven :=
isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)
(by
simp_all only [alternatingConst, dite_eq_ite, Iso.refl_hom, Category.id_comp, shortComplexFunctor'_obj_f,
↓reduceIte, Category.comp_id, right_eq_ite_iff]
intro hi
have := hc i j hij
exact False.elim <| Nat.not_odd_iff_even.2 hi <| by simp_all [Nat.odd_add])
(by simp_all [alternatingConst])
