Finite biproducts of sheaves of modules #
Sheaves of modules over a sheaf of rings form a preadditive category with finite coproducts, so they have finite biproducts. These biproducts provide the finite direct sums used to construct finite free sheaves and their monoidal duality.
Main declaration #
instance
TauCeti.SheafOfModules.hasFiniteBiproducts
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
:
Sheaves of modules have finite biproducts, since they form a preadditive category with finite coproducts.