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.

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_mono {C : Type u_2} [Category.{u_1, u_2} C] {J K : Precoverage C} (h : J ≤ K) : J.toGrothendieck ≤ K.toGrothendieck

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.

theorem CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition {C : Type u_2} [Category.{u_1, u_2} C] {J : Precoverage C} [J.IsStableUnderComposition] [J.IsStableUnderBaseChange] [J.HasPullbacks] [J.HasIsos] {X : C} {S : Sieve X} : S ∈ J.toGrothendieck X ↔ ∃ R ∈ J.coverings X, R ≤ S.arrows

theorem CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck {C : Type u_2} [Category.{u_1, u_2} C] {J : Precoverage C} [J.IsStableUnderComposition] [J.IsStableUnderBaseChange] [Limits.HasPullbacks C] [J.HasIsos] : (toPretopology C J).toGrothendieck = J.toGrothendieck

theorem CategoryTheory.Presieve.IsSheaf.isSheafFor_of_mem_precoverage {C : Type u_3} [Category.{u_2, u_3} C] {J : Precoverage C} {P : Functor Cᵒᵖ (Type u_1)} (h : IsSheaf J.toGrothendieck P) {S : C} {R : Presieve S} (hR : R ∈ J.coverings S) : IsSheafFor P R

theorem CategoryTheory.PreZeroHypercover.isSheafFor_iff_of_iso {C : Type u_3} [Category.{u_2, u_3} C] {F : Functor Cᵒᵖ (Type u_1)} {S : C} {𝒰 𝒱 : PreZeroHypercover S} (e : 𝒰 ≅ 𝒱) : Presieve.IsSheafFor F 𝒰.presieve₀ ↔ Presieve.IsSheafFor F 𝒱.presieve₀

theorem CategoryTheory.Presieve.isSheafFor_ofArrows_comp_iff {C : Type u_4} [Category.{u_3, u_4} C] {F : Functor Cᵒᵖ (Type u_1)} {X : C} {ι : Type u_2} {Y Z : ι → C} (g : (i : ι) → Z i ⟶ X) (e : (i : ι) → Y i ≅ Z i) : IsSheafFor F (ofArrows Y fun (i : ι) => CategoryStruct.comp (e i).hom (g i)) ↔ IsSheafFor F (ofArrows Z g)

theorem CategoryTheory.Presieve.isSheafFor_singleton_iff_of_iso {C : Type u_3} [Category.{u_2, u_3} C] {F : Functor Cᵒᵖ (Type u_1)} {S X Y : C} (f : X ⟶ S) (g : Y ⟶ S) (e : X ≅ Y) (he : CategoryStruct.comp e.hom g = f) : IsSheafFor F (singleton f) ↔ IsSheafFor F (singleton g)

theorem CategoryTheory.Presieve.IsSheafFor.comp_iff_of_preservesPairwisePullbacks {C : Type u_4} [Category.{u_3, u_4} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) (P : Functor Dᵒᵖ (Type u_2)) {X : C} (R : Presieve X) [R.HasPairwisePullbacks] [F.PreservesPairwisePullbacks R] : IsSheafFor (F.op.comp P) R ↔ IsSheafFor P (map F R)