Lean4
/-- The functor `V ⥤ HomologicalComplex V c` creating a chain complex supported in a single degree.
-/
noncomputable def single (j : ι) : V ⥤ HomologicalComplex V c
where
obj
A :=
{ X := fun i => if i = j then A else 0
d := fun _ _ => 0 }
map
f :=
{ f := fun i => if h : i = j then eqToHom (by dsimp; rw [if_pos h]) ≫ f ≫ eqToHom (by dsimp; rw [if_pos h]) else 0 }
map_id
A := by
ext
dsimp
split_ifs with h
· subst h
simp
· #adaptation_note /-- nightly-2024-03-07
previously was `rw [if_neg h]; simp`, but that fails with "motive not type correct"
This is because dsimp does not simplify numerals;
this note should be removable once https://github.com/leanprover/lean4/pull/8433 lands. -/
convert (id_zero (C := V)).symm
all_goals simp [if_neg h]
map_comp f
g := by
ext
dsimp
split_ifs with h
· subst h
simp
· simp
