Grothendieck topology generated by a precoverage

For any category C, we define the Grothendieck topology generated by a precoverage J on C. It is the smallest Grothendieck topology containing all the sieves generated by the covering presieves of J.

The main definitions and theorems are:

• Precoverage.toGrothendieck: The Grothendieck topology generated by the sieves generated by the covering presieves of J.
• Precoverage.toGrothendieck_eq_sInf: The Grothendieck topology generated by J is the infimum of the Grothendieck topologies containing all the sieves generated by the covering presieves of J.
• Presieve.isSheaf_toGrothendieck_iff: Given J : Precoverage C with associated Grothendieck topology K, a Type*-valued presheaf on C is a sheaf for K if and only if it is a sheaf for all pullbacks of the covering presieves of J.

inductive CategoryTheory.Precoverage.Saturate {C : Type u_1} [Category.{u_2, u_1} C] (J : Precoverage C) (X : C) : Sieve X → Prop

An auxiliary definition used to define the Grothendieck topology associated to a precoverage. See Precoverage.toGrothendieck.

• of {C : Type u_1} [Category.{u_2, u_1} C] {J : Precoverage C} (X : C) (S : Presieve X) (hS : S ∈ J.coverings X) : J.Saturate X (Sieve.generate S)
• top {C : Type u_1} [Category.{u_2, u_1} C] {J : Precoverage C} (X : C) : J.Saturate X ⊤
• pullback {C : Type u_1} [Category.{u_2, u_1} C] {J : Precoverage C} (X : C) (S : Sieve X) : J.Saturate X S → ∀ (Y : C) (f : Y ⟶ X), J.Saturate Y (Sieve.pullback f S)
• transitive {C : Type u_1} [Category.{u_2, u_1} C] {J : Precoverage C} (X : C) (S R : Sieve X) : J.Saturate X S → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f R)) → J.Saturate X R

def CategoryTheory.Precoverage.toGrothendieck {C : Type u_1} [Category.{u_2, u_1} C] (J : Precoverage C) : GrothendieckTopology C

The Grothendieck topology associated to a precoverage J. It is defined inductively as follows:

1. If S is a covering presieve for J, then the sieve generated by S is a covering sieve for the associated Grothendieck topology.
2. The top sieves are in the associated Grothendieck topology.
3. Add all sieves required by the pullback stability condition of a Grothendieck topology.
4. Add all sieves required by the local character axiom of a Grothendieck topology.

Equations

• J.toGrothendieck = { sieves := J.Saturate, top_mem' := ⋯, pullback_stable' := ⋯, transitive' := ⋯ }

theorem CategoryTheory.Precoverage.mem_toGrothendieck_iff {C : Type u_2} [Category.{u_1, u_2} C] {J : Precoverage C} {X : C} {S : Sieve X} : S ∈ J.toGrothendieck X ↔ J.Saturate X S

theorem CategoryTheory.Precoverage.generate_mem_toGrothendieck {C : Type u_2} [Category.{u_1, u_2} C] {J : Precoverage C} {X : C} {R : Presieve X} (hR : R ∈ J.coverings X) : Sieve.generate R ∈ J.toGrothendieck X

theorem CategoryTheory.Precoverage.toGrothendieck_eq_sInf {C : Type u_2} [Category.{u_1, u_2} C] (J : Precoverage C) : J.toGrothendieck = sInf {K : GrothendieckTopology C | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X}

An alternative characterization of the Grothendieck topology associated to a precoverage J: it is the infimum of all Grothendieck topologies containing Sieve.generate S for all presieves S in J.

theorem CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff {C : Type u_3} [Category.{u_2, u_3} C] {J : Precoverage C} (P : Functor Cᵒᵖ (Type u_1)) : Presieve.IsSheaf J.toGrothendieck P ↔ ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

The main theorem of this file: given a precoverage J on C, a Type*-valued presheaf on C is a sheaf for the associated Grothendieck topology if and only if it is a sheaf for all pullback sieves of presieves in J.