English
Similarly, when i~j, j~k and j is odd, the i-j-k short complex is isomorphic to the short complex with φ, ψ and hOdd.
Русский
Аналогично для i~j, j~k и нечетного j, i-j-k короткий комплекс изоморфен короткому комплексу с φ, ψ и hOdd.
LaTeX
$$$\text{AltConstScIsoOdd}(A, hOdd, hEven, hc)\;:\; (\mathrm{alternatingConst}\; A\; hOdd\; hEven\; hc)\;\mathrm{sc'}\; i\; j\; k \cong \mathrm{ShortComplex.mk}\; φ\; ψ\; hOdd$$$
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 alternatingConstScIsoOdd {i j k : ℕ} (hij : c.Rel i j) (hjk : c.Rel j k) (h : Odd j) :
(alternatingConst A hOdd hEven hc).sc' i j k ≅ ShortComplex.mk φ ψ hOdd :=
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, left_eq_ite_iff]
intro hi
have := hc i j hij
exact False.elim <| Nat.not_even_iff_odd.2 h <| by simp_all [Nat.odd_add])
(by simp_all [alternatingConst])
