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

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

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