Chain complexes of abelian sheaves

Stream: Is there code for X?

[Kyle Miller]

A student of mine (@Mingjie Wang) is working on a project involving chain complexes of abelian sheaves, and we got stuck with satisfying the typeclass hypotheses for docs#ChainComplex. After defining Zero for for the hom sets between abelian sheaves and Limits.HasZeroMorphisms for AbSheaf itself we could get the last definition to go through, but we were wondering if there was another way?

import Mathlib

open CategoryTheory

variable (X : TopCat) (Y : TopCat)

-- Abelian sheaf
abbrev AbSheaf (base : TopCat) := TopCat.Sheaf Ab base

-- Is this missing from Mathlib?
instance (F G : AbSheaf X) : Zero (F ⟶ G) where
  zero := ⟨⟨0, by simp⟩⟩

-- Is this missing from Mathlib?
instance : Limits.HasZeroMorphisms (AbSheaf X) where
  comp_zero := by
    intros
    rfl
  zero_comp := by
    intros
    apply Sheaf.hom_ext
    ext
    -- How to do directly?
    unfold_projs
    simp
    apply map_zero

def K (X : TopCat) := ChainComplex (AbSheaf X) ℤ

[Andrew Yang]

Does docs#CategoryTheory.instPreadditiveSheaf not fire automatically?

[Kyle Miller]

Ah, thanks, docs#TopCat.Sheaf is a def and not an abbrev so that wasn't being found.

[Kyle Miller]

At least this is a workaround:

import Mathlib

open CategoryTheory

variable (X : TopCat) (Y : TopCat)

-- Abelian sheaf
abbrev AbSheaf (base : TopCat) := TopCat.Sheaf Ab base

instance : Preadditive (AbSheaf X) := CategoryTheory.instPreadditiveSheaf

def K (X : TopCat) := ChainComplex (AbSheaf X) ℤ