Lean4
/-- Given a complex shape `c`, two indices `i₀` and `i₁` such that `c.Rel i₀ i₁`,
and `f : X₀ ⟶ X₁`, this is the homological complex which, if `i₀ ≠ i₁`, only
consists of the map `f` in degrees `i₀` and `i₁`, and zero everywhere else. -/
noncomputable def double : HomologicalComplex C c
where
X k := if k = i₀ then X₀ else if k = i₁ then X₁ else 0
d k
k' :=
if hk : k = i₀ ∧ k' = i₁ ∧ i₀ ≠ i₁ then
eqToHom (if_pos hk.1) ≫
f ≫
eqToHom
(by
rw [if_neg, if_pos hk.2.1]
aesop)
else 0
d_comp_d' := by
rintro i j k hij hjk
dsimp
by_cases hi : i = i₀
· subst hi
by_cases hj : j = i₁
· subst hj
nth_rw 2 [dif_neg (by tauto)]
rw [comp_zero]
· rw [dif_neg (by tauto), zero_comp]
· rw [dif_neg (by tauto), zero_comp]
shape i j hij := dif_neg (by aesop)
