presheafToSheaf_additive — Mathlib

English

The presheaf-to-sheaf construction is additive when D is abelian and J is a Grothendieck topology on C.

Русский

Построение перехода от прешиффа к шейфу является аддитивным, когда D абелева и J является топологией Гротендика на C.

LaTeX

$$$(presheafToSheaf\\ J\\ D).Additive$$$

Lean4

instance presheafToSheaf_additive : (presheafToSheaf J D).Additive :=
  (presheafToSheaf J D).additive_of_preservesBinaryBiproducts

Похожие утверждения