Lean4
/-- The short complex of abelian sheaves
`ℤ[S.X₁] ⟶ ℤ[S.X₂] ⊞ ℤ[S.X₃] ⟶ ℤ[S.X₄]`
where the left map is a difference and the right map a sum. -/
@[simps]
noncomputable def shortComplex : ShortComplex (Sheaf J AddCommGrpCat.{v})
where
X₁ := (presheafToSheaf J _).obj (yoneda.obj S.X₁ ⋙ AddCommGrpCat.free)
X₂ :=
(presheafToSheaf J _).obj (yoneda.obj S.X₂ ⋙ AddCommGrpCat.free) ⊞
(presheafToSheaf J _).obj (yoneda.obj S.X₃ ⋙ AddCommGrpCat.free)
X₃ := (presheafToSheaf J _).obj (yoneda.obj S.X₄ ⋙ AddCommGrpCat.free)
f :=
biprod.lift ((presheafToSheaf J _).map (Functor.whiskerRight (yoneda.map S.f₁₂) _))
(-(presheafToSheaf J _).map (Functor.whiskerRight (yoneda.map S.f₁₃) _))
g :=
biprod.desc ((presheafToSheaf J _).map (Functor.whiskerRight (yoneda.map S.f₂₄) _))
((presheafToSheaf J _).map (Functor.whiskerRight (yoneda.map S.f₃₄) _))
zero :=
(S.map
(yoneda ⋙
(Functor.whiskeringRight _ _ _).obj AddCommGrpCat.free ⋙ presheafToSheaf J _)).cokernelCofork.condition
