Generators in the category of sheaves

In this file, we show that if J : GrothendieckTopology C and A is a preadditive category which has a separator (and suitable coproducts), then Sheaf J A has a separator.

noncomputable def CategoryTheory.Sheaf.freeYoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] [HasWeakSheafify J A] (X : C) (M : A) : Sheaf J A

Given J : GrothendieckTopology C, X : C and M : A, this is the associated sheaf to the presheaf Presheaf.freeYoneda X M.

Equations

• CategoryTheory.Sheaf.freeYoneda J X M = (CategoryTheory.presheafToSheaf J A).obj (CategoryTheory.Presheaf.freeYoneda X M)

noncomputable def CategoryTheory.Sheaf.freeYonedaHomEquiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] [HasWeakSheafify J A] {X : C} {M : A} {F : Sheaf J A} : (freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (Opposite.op X))

The bijection (Sheaf.freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X)) when F : Sheaf J A, X : C and M : A.

Equations

• CategoryTheory.Sheaf.freeYonedaHomEquiv = ((CategoryTheory.sheafificationAdjunction J A).homEquiv (CategoryTheory.Presheaf.freeYoneda X M) F).trans CategoryTheory.Presheaf.freeYonedaHomEquiv

theorem CategoryTheory.Sheaf.isSeparating {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] [HasWeakSheafify J A] {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) : IsSeparating (Set.range fun (x : C × ι) => match x with | (X, i) => freeYoneda J X (S i))

theorem CategoryTheory.Sheaf.isSeparator {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] [HasWeakSheafify J A] {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) [Limits.HasCoproduct fun (x : C × ι) => match x with | (X, i) => freeYoneda J X (S i)] [Preadditive A] : IsSeparator (∐ fun (x : C × ι) => match x with | (X, i) => freeYoneda J X (S i))

instance CategoryTheory.Sheaf.hasSeparator {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] [Limits.HasCoproducts A] [HasWeakSheafify J A] [HasSeparator A] [Preadditive A] [Limits.HasCoproducts A] : HasSeparator (Sheaf J A)