# Coverages #

A coverage K on a category C is a set of presieves associated to every object X : C, called "covering presieves". This collection must satisfy a certain "pullback compatibility" condition, saying that whenever S is a covering presieve on X and f : Y ⟶ X is a morphism, then there exists some covering sieve T on Y such that T factors through S along f.

The main difference between a coverage and a Grothendieck pretopology is that we do not require C to have pullbacks. This is useful, for example, when we want to consider the Grothendieck topology on the category of extremally disconnected sets in the context of condensed mathematics.

A more concrete example: If ℬ is a basis for a topology on a type X (in the sense of TopologicalSpace.IsTopologicalBasis) then it naturally induces a coverage on Opens X whose associated Grothendieck topology is the one induced by the topology on X generated by ℬ. (Project: Formalize this!)

## Main Definitions and Results: #

All definitions are in the CategoryTheory namespace.

• Coverage C: The type of coverages on C.
• Coverage.ofGrothendieck C: A function which associates a coverage to any Grothendieck topology.
• Coverage.toGrothendieck C: A function which associates a Grothendieck topology to any coverage.
• Coverage.gi: The two functions above form a Galois insertion.
• Presieve.isSheaf_coverage: Given K : Coverage C with associated Grothendieck topology J, a Type*-valued presheaf on C is a sheaf for K if and only if it is a sheaf for J.

# References #

We don't follow any particular reference, but the arguments can probably be distilled from the following sources:

• [Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.1.
• nLab, Coverage
def CategoryTheory.Presieve.FactorsThruAlong {C : Type u_1} [] {X : C} {Y : C} (S : ) (T : ) (f : Y X) :

Given a morphism f : Y ⟶ X, a presieve S on Y and presieve T on X, we say that S factors through T along f, written S.FactorsThruAlong T f, provided that for any morphism g : Z ⟶ Y in S, there exists some morphism e : W ⟶ X in T and some morphism i : Z ⟶ W such that the obvious square commutes: i ≫ e = g ≫ f.

This is used in the definition of a coverage.

Equations
• S.FactorsThruAlong T f = ∀ ⦃Z : C⦄ ⦃g : Z Y⦄, S g∃ (W : C) (i : Z W) (e : W X),
Instances For
def CategoryTheory.Presieve.FactorsThru {C : Type u_1} [] {X : C} (S : ) (T : ) :

Given S T : Presieve X, we say that S factors through T if any morphism in S factors through some morphism in T.

The lemma Presieve.isSheafFor_of_factorsThru gives a sufficient condition for a presheaf to be a sheaf for a presieve T, in terms of S.FactorsThru T, provided that the presheaf is a sheaf for S.

Equations
• S.FactorsThru T = ∀ ⦃Z : C⦄ ⦃g : Z X⦄, S g∃ (W : C) (i : Z W) (e : W X), T e
Instances For
@[simp]
theorem CategoryTheory.Presieve.factorsThruAlong_id {C : Type u_2} [] {X : C} (S : ) (T : ) :
S.FactorsThruAlong T S.FactorsThru T
theorem CategoryTheory.Presieve.factorsThru_of_le {C : Type u_2} [] {X : C} (S : ) (T : ) (h : S T) :
S.FactorsThru T
theorem CategoryTheory.Presieve.le_of_factorsThru_sieve {C : Type u_2} [] {X : C} (S : ) (T : ) (h : S.FactorsThru T.arrows) :
S T.arrows
theorem CategoryTheory.Presieve.factorsThru_top {C : Type u_2} [] {X : C} (S : ) :
S.FactorsThru
theorem CategoryTheory.Presieve.isSheafFor_of_factorsThru {C : Type u_3} [] {X : C} {S : } {T : } (P : ) (H : S.FactorsThru T) (hS : ) (h : ∀ ⦃Y : C⦄ ⦃f : Y X⦄, T f∃ (R : ), R.FactorsThruAlong S f) :
theorem CategoryTheory.Coverage.ext_iff {C : Type u_1} :
∀ {inst : } (x y : ), x = y x.covering = y.covering
theorem CategoryTheory.Coverage.ext {C : Type u_1} :
∀ {inst : } (x y : ), x.covering = y.coveringx = y
structure CategoryTheory.Coverage (C : Type u_1) [] :
Type (max u_1 u_2)

The type Coverage C of coverages on C. A coverage is a collection of covering presieves on every object X : C, which satisfies a pullback compatibility condition. Explicitly, this condition says that whenever S is a covering presieve for X and f : Y ⟶ X is a morphism, then there exists some covering presieve T for Y such that T factors through S along f.

• covering : (X : C) →

The collection of covering presieves for an object X.

• pullback : ∀ ⦃X Y : C⦄ (f : Y X), Sself.covering X, Tself.covering Y, T.FactorsThruAlong S f

Given any covering sieve S on X and a morphism f : Y ⟶ X, there exists some covering sieve T on Y such that T factors through S along f.

Instances For
theorem CategoryTheory.Coverage.pullback {C : Type u_1} [] (self : ) ⦃X : C ⦃Y : C (f : Y X) (S : ) :
S self.covering XTself.covering Y, T.FactorsThruAlong S f

Given any covering sieve S on X and a morphism f : Y ⟶ X, there exists some covering sieve T on Y such that T factors through S along f.

instance CategoryTheory.Coverage.instCoeFunForallSetPresieve {C : Type u_1} [] :
CoeFun fun (x : ) => (X : C) →
Equations
• CategoryTheory.Coverage.instCoeFunForallSetPresieve = { coe := CategoryTheory.Coverage.covering }

Associate a coverage to any Grothendieck topology. If J is a Grothendieck topology, and K is the associated coverage, then a presieve S is a covering presieve for K if and only if the sieve that it generates is a covering sieve for J.

Equations
• = { covering := fun (X : C) => {S : | J.sieves X}, pullback := }
Instances For
theorem CategoryTheory.Coverage.ofGrothendieck_iff {C : Type u_2} [] {X : C} {S : } :
S .covering X J.sieves X
inductive CategoryTheory.Coverage.saturate {C : Type u_1} [] (K : ) (X : C) :

An auxiliary definition used to define the Grothendieck topology associated to a coverage. See Coverage.toGrothendieck.

• of: ∀ {C : Type u_1} [inst : ] {K : } (X : C), SK.covering X, K.saturate X
• top: ∀ {C : Type u_1} [inst : ] {K : } (X : C), K.saturate X
• transitive: ∀ {C : Type u_1} [inst : ] {K : } (X : C) (R S : ), K.saturate X R(∀ ⦃Y : C⦄ ⦃f : Y X⦄, R.arrows fK.saturate Y )K.saturate X S
Instances For
theorem CategoryTheory.Coverage.eq_top_pullback {C : Type u_2} [] {X : C} {Y : C} {S : } {T : } (h : S T) (f : Y X) (hf : S.arrows f) :
theorem CategoryTheory.Coverage.saturate_of_superset {C : Type u_1} [] (K : ) {X : C} {S : } {T : } (h : S T) (hS : K.saturate X S) :
K.saturate X T

The Grothendieck topology associated to a coverage K. It is defined inductively as follows:

1. If S is a covering presieve for K, 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 local character axiom of a Grothendieck topology.

The pullback compatibility condition for a coverage ensures that the associated Grothendieck topology is pullback stable, and so an additional constructor in the inductive construction is not needed.

Equations
• = { sieves := K.saturate, top_mem' := , pullback_stable' := , transitive' := }
Instances For
Equations
• CategoryTheory.Coverage.instPartialOrder =

The two constructions Coverage.toGrothendieck and Coverage.ofGrothendieck form a Galois insertion.

Equations
• One or more equations did not get rendered due to their size.
Instances For

An alternative characterization of the Grothendieck topology associated to a coverage K: it is the infimum of all Grothendieck topologies whose associated coverage contains K.

Equations
• CategoryTheory.Coverage.instSemilatticeSup =
@[simp]
theorem CategoryTheory.Coverage.sup_covering {C : Type u_1} [] (x : ) (y : ) (B : C) :
(x y).covering B = x.covering B y.covering B
theorem CategoryTheory.Coverage.mem_toGrothendieck_sieves_of_superset {C : Type u_1} [] (K : ) {X : C} {S : } {R : } (h : R S.arrows) (hR : R K.covering X) :
S .sieves X

Any sieve that contains a covering presieve for a coverage is a covering sieve for the associated Grothendieck topology.

theorem CategoryTheory.Presieve.isSheaf_coverage {C : Type u_2} [] (K : ) (P : ) :
∀ {X : C}, RK.covering X,

The main theorem of this file: Given a coverage K on C, a Type*-valued presheaf on C is a sheaf for K if and only if it is a sheaf for the associated Grothendieck topology.

theorem CategoryTheory.Presieve.isSheaf_sup {C : Type u_2} [] (K : ) (L : ) (P : ) :

A presheaf is a sheaf for the Grothendieck topology generated by a union of coverages iff it is a sheaf for the Grothendieck topology generated by each coverage separately.

theorem CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage {C : Type u_1} {D : Type u_4} [] [] (K : ) (P : ) :
∀ ⦃X : C⦄, RK.covering X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone .arrows.cocone.op))
theorem CategoryTheory.Presheaf.isSheaf_sup {C : Type u_1} {D : Type u_4} [] [] (K : ) (L : ) (P : ) :