English
Construct the alternating-constant complex on an object A with endomorphisms φ, ψ: A → A whenever the indices i and j are related; the differential is φ when i is even and ψ when i is odd, and 0 otherwise.
Русский
Построим чередующийся константный комплекс на объекте A с концевыми отображениями φ, ψ: A → A: если i и j связаны, то дифференциал равен φ при чётном i и ψ при нечётном i, иначе 0.
LaTeX
$$$\text{AlternatingConst}(A, φ, ψ, c) :\; \text{d}_{i j} = \begin{cases} φ, & \text{if } c.Rel i j \text{ and } i \text{ even}, \\ ψ, & \text{if } c.Rel i j \ and \ i \text{ odd}, \\ 0, & \text{otherwise}. \end{cases}$$$
Lean4
/-- Let `c : ComplexShape ℕ` be such that `i j : ℕ` have opposite parity if they are related by
`c`. Let `φ, ψ : A ⟶ A` be such that `φ ∘ ψ = ψ ∘ φ = 0`. This is a complex of shape `c` whose
objects are all `A`. For all `i, j` related by `c`, `dᵢⱼ = φ` when `i` is even, and `dᵢⱼ = ψ` when
`i` is odd. -/
@[simps!]
noncomputable def alternatingConst {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ i j, c.Rel i j → Odd (i + j)) :
HomologicalComplex C c where
X n := A
d i j := if hij : c.Rel i j then if hi : Even i then φ else ψ else 0
shape i j := by aesop
d_comp_d' i j k hij
hjk := by
have := hc i j hij
split_ifs with hi hj hj
· exact False.elim <| Nat.not_odd_iff_even.2 hi <| by simp_all [Nat.odd_add]
· assumption
· assumption
· exact False.elim <| hj <| by simp_all [Nat.odd_add]
