Documentation

Mathlib.CategoryTheory.Sites.Precoverage.Generates

Generators of a Grothendieck topology #

Let K be a precoverage and J a Grothendieck topology on a category C. We say K generates J if for every presheaf F on C, it is a sheaf for J if and only if it is a sheaf for every covering in K.

If K generates J, then J is the smallest Grothendieck topology containing K. The converse only holds if K is a coverage or a pretopology.

Implementation details #

For C : Type u and Category.{v} C, the definition of Precoverage.Generates quantifies over presheafs Cᵒᵖ ⥤ Type max u v. We then show that this implies that the condition holds for all presheafs Cᵒᵖ ⥤ Type w.

source
structure CategoryTheory.Precoverage.Generates {C : Type u} [Category.{v, u} C] (K : Precoverage C) (J : GrothendieckTopology C) :
Prop

A precoverage K generates the topology J if a presheaf on C is a sheaf for K if and only if it is a sheaf for J.

Instances For
    source
    theorem CategoryTheory.Precoverage.Generates.generate_mem {C : Type u} [Category.{v, u} C] {K : Precoverage C} {J : GrothendieckTopology C} (H : K.Generates J) {X : C} {R : Presieve X} (h : R ∈ K.coverings X) :
    Sieve.generate R ∈ J X
    source
    theorem CategoryTheory.Precoverage.Generates.isSheaf_of_forall {C : Type u} [Category.{v, u} C] {K : Precoverage C} {J : GrothendieckTopology C} (h : K.Generates J) (F : Functor Cᵒᵖ (Type w)) (H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R) :
    Presieve.IsSheaf J F

    If K generates J, then any presheaf Cᵒᵖ ⥤ Type w that satisfies the sheaf condition for all K-coverings, is a J-sheaf.

    source
    theorem CategoryTheory.Precoverage.Generates.isSheaf_type_iff {C : Type u} [Category.{v, u} C] {K : Precoverage C} {J : GrothendieckTopology C} (H : K.Generates J) {F : Functor Cᵒᵖ (Type w)} :
    Presieve.IsSheaf J F ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R

    If K generates J, then any presheaf is a sheaf if and only if it is a sheaf for all K-covers.

    source
    theorem CategoryTheory.Precoverage.Generates.toGrothendieck_eq {C : Type u} [Category.{v, u} C] {K : Precoverage C} {J : GrothendieckTopology C} (H : K.Generates J) :
    K.toGrothendieck = J

    If K generates J, then J is equal to the smallest Grothendieck topology containing K. The converse is false, but holds if K is a coverage, see CategoryTheory.Coverage.generates_iff.

    source
    theorem CategoryTheory.Precoverage.Generates.isSheaf_iff {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {K : Precoverage C} {J : GrothendieckTopology C} (H : K.Generates J) {F : Functor Cᵒᵖ A} :
    Presheaf.IsSheaf J F ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, ∀ (M : A), Presieve.IsSheafFor (F.comp (coyoneda.obj (Opposite.op M))) R
    source
    theorem CategoryTheory.Coverage.generates_toGrothendieck {C : Type u} [Category.{v, u} C] (K : Coverage C) :
    K.Generates K.toGrothendieck

    If K is a coverage, it generates the smallest Grothendieck topology containing K.

    source
    theorem CategoryTheory.Coverage.generates_iff {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {K : Coverage C} :
    K.Generates J ↔ K.toGrothendieck = J