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.
• GrothendieckTopology.toCoverage 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:

• [Joh02]: Sketches of an Elephant, P. T. Johnstone: C2.1.
• nLab, Coverage

def CategoryTheory.Presieve.FactorsThruAlong {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (S : Presieve Y) (T : Presieve X) (f : Y ⟶ X) : Prop

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), T e ∧ CategoryTheory.CategoryStruct.comp i e = CategoryTheory.CategoryStruct.comp g f

theorem CategoryTheory.Presieve.FactorsThruAlong.pullbackArrows {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) (R : Presieve Y) [R.HasPullbacks f] : (Presieve.pullbackArrows f R).FactorsThruAlong R f

def CategoryTheory.Presieve.FactorsThru {C : Type u_1} [Category.{v_1, u_1} C] {X : C} (S T : Presieve X) : Prop

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 ∧ CategoryTheory.CategoryStruct.comp i e = g

@[simp]

theorem CategoryTheory.Presieve.factorsThruAlong_id {C : Type u_1} [Category.{v_1, u_1} C] {X : C} (S T : Presieve X) : S.FactorsThruAlong T (CategoryStruct.id X) ↔ S.FactorsThru T

theorem CategoryTheory.Presieve.factorsThru_of_le {C : Type u_1} [Category.{v_1, u_1} C] {X : C} (S T : Presieve X) (h : S ≤ T) : S.FactorsThru T

theorem CategoryTheory.Presieve.le_of_factorsThru_sieve {C : Type u_1} [Category.{v_1, u_1} C] {X : C} (S : Presieve X) (T : Sieve X) (h : S.FactorsThru T.arrows) : S ≤ T.arrows

theorem CategoryTheory.Presieve.factorsThru_top {C : Type u_1} [Category.{v_1, u_1} C] {X : C} (S : Presieve X) : S.FactorsThru ⊤

theorem CategoryTheory.Presieve.isSheafFor_of_factorsThru {C : Type u_2} [Category.{v_1, u_2} C] {X : C} {S T : Presieve X} (P : Functor Cᵒᵖ (Type u_1)) (H : S.FactorsThru T) (hS : IsSheafFor P S) (h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f) : IsSheafFor P T

structure CategoryTheory.Coverage (C : Type u_1) [Category.{v_1, u_1} C] extends CategoryTheory.Precoverage C : Type (max u_1 v_1)

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.

• coverings (X : C) : Set (Presieve X)
• pullback ⦃X Y : C⦄ (f : Y ⟶ X) (S : Presieve X) : S ∈ self.coverings X → ∃ T ∈ self.coverings 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.

theorem CategoryTheory.Coverage.ext {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {x y : Coverage C} (coverings : x.coverings = y.coverings) : x = y

theorem CategoryTheory.Coverage.ext_iff {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {x y : Coverage C} : x = y ↔ x.coverings = y.coverings

@[deprecated CategoryTheory.Precoverage.coverings (since := "2025-08-28")]

def CategoryTheory.Coverage.covering {C : Type u_1} [Category.{v_1, u_1} C] (self : Precoverage C) (X : C) : Set (Presieve X)

Alias of CategoryTheory.Precoverage.coverings.

Equations

• @CategoryTheory.Coverage.covering = @CategoryTheory.Precoverage.coverings

@[instance_reducible]

instance CategoryTheory.Coverage.instCoeFunForallSetPresieve {C : Type u_1} [Category.{v_1, u_1} C] : CoeFun (Coverage C) fun (x : Coverage C) => (X : C) → Set (Presieve X)

Equations

• CategoryTheory.Coverage.instCoeFunForallSetPresieve = { coe := fun (J : CategoryTheory.Coverage C) => J.coverings }

def CategoryTheory.GrothendieckTopology.toCoverage {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) : Coverage C

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

• J.toCoverage = { coverings := fun (X : C) => {S : CategoryTheory.Presieve X | CategoryTheory.Sieve.generate S ∈ J X}, pullback := ⋯ }

@[deprecated CategoryTheory.GrothendieckTopology.toCoverage (since := "2025-09-19")]

def CategoryTheory.Coverage.ofGrothendieck {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) : Coverage C

Alias of CategoryTheory.GrothendieckTopology.toCoverage.

---

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

• @CategoryTheory.Coverage.ofGrothendieck = @CategoryTheory.GrothendieckTopology.toCoverage

theorem CategoryTheory.GrothendieckTopology.mem_toCoverage_iff {C : Type u_1} [Category.{v_1, u_1} C] {X : C} {S : Presieve X} (J : GrothendieckTopology C) : S ∈ J.toCoverage.coverings X ↔ Sieve.generate S ∈ J X

@[deprecated CategoryTheory.GrothendieckTopology.mem_toCoverage_iff (since := "2025-09-19")]

theorem CategoryTheory.ofGrothendieck_iff {C : Type u_1} [Category.{v_1, u_1} C] {X : C} {S : Presieve X} (J : GrothendieckTopology C) : S ∈ J.toCoverage.coverings X ↔ Sieve.generate S ∈ J X

Alias of CategoryTheory.GrothendieckTopology.mem_toCoverage_iff.

inductive CategoryTheory.Coverage.Saturate {C : Type u_1} [Category.{v_1, u_1} C] (K : Coverage C) (X : C) : Sieve X → Prop

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

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

theorem CategoryTheory.Coverage.eq_top_pullback {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} {S T : Sieve X} (h : S ≤ T) (f : Y ⟶ X) (hf : S.arrows f) : Sieve.pullback f T = ⊤

theorem CategoryTheory.Coverage.saturate_of_superset {C : Type u_1} [Category.{v_1, u_1} C] (K : Coverage C) {X : C} {S T : Sieve X} (h : S ≤ T) (hS : K.Saturate X S) : K.Saturate X T

theorem CategoryTheory.Coverage.Saturate.pullback {C : Type u_1} [Category.{v_1, u_1} C] (K : Coverage C) {X Y : C} (f : Y ⟶ X) {S : Sieve X} (h : K.Saturate X S) : K.Saturate Y (Sieve.pullback f S)

theorem CategoryTheory.Coverage.saturate_iff_saturate_toPrecoverage {C : Type u_1} [Category.{v_1, u_1} C] (K : Coverage C) {X : C} {S : Sieve X} : K.Saturate X S ↔ K.Saturate X S

def CategoryTheory.Coverage.toGrothendieck {C : Type u_1} [Category.{v_1, u_1} C] (K : Coverage C) : GrothendieckTopology C

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

• K.toGrothendieck = K.toGrothendieck.copy K.Saturate ⋯

theorem CategoryTheory.Coverage.mem_toGrothendieck {C : Type u_1} [Category.{v_1, u_1} C] {K : Coverage C} {X : C} {S : Sieve X} : S ∈ K.toGrothendieck X ↔ K.Saturate X S

@[instance_reducible]

instance CategoryTheory.Coverage.instPartialOrder {C : Type u_1} [Category.{v_1, u_1} C] : PartialOrder (Coverage C)

Equations

• CategoryTheory.Coverage.instPartialOrder = { le := fun (A B : CategoryTheory.Coverage C) => A.coverings ≤ B.coverings, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

def CategoryTheory.Coverage.gi (C : Type u_1) [Category.{v_1, u_1} C] : GaloisInsertion toGrothendieck GrothendieckTopology.toCoverage

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

Equations

• CategoryTheory.Coverage.gi C = { choice := fun (K : CategoryTheory.Coverage C) (x : K.toGrothendieck.toCoverage ≤ K) => K.toGrothendieck, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

theorem CategoryTheory.Coverage.toGrothendieck_eq_sInf {C : Type u_1} [Category.{v_1, u_1} C] (K : Coverage C) : K.toGrothendieck = sInf {J : GrothendieckTopology C | K ≤ J.toCoverage}

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.

@[instance_reducible]

instance CategoryTheory.Coverage.instSemilatticeSup {C : Type u_1} [Category.{v_1, u_1} C] : SemilatticeSup (Coverage C)

Equations

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

@[simp]

theorem CategoryTheory.Coverage.sup_covering {C : Type u_1} [Category.{v_1, u_1} C] (x y : Coverage C) (B : C) : (x ⊔ y).coverings B = x.coverings B ∪ y.coverings B

theorem CategoryTheory.Coverage.mem_toGrothendieck_sieves_of_superset {C : Type u_1} [Category.{v_1, u_1} C] (K : Coverage C) {X : C} {S : Sieve X} {R : Presieve X} (h : R ≤ S.arrows) (hR : R ∈ K.coverings X) : S ∈ K.toGrothendieck X

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

def CategoryTheory.Pretopology.toCoverage {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] (J : Pretopology C) : Coverage C

Any pretopology is a coverage.

Equations

• J.toCoverage = { toPrecoverage := J.toPrecoverage, pullback := ⋯ }

@[simp]

theorem CategoryTheory.Pretopology.mem_toCoverage {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] (J : Pretopology C) {X : C} (S : Presieve X) : S ∈ J.toCoverage.coverings X ↔ S ∈ J.coverings X

theorem CategoryTheory.Pretopology.toGrothendieck_toCoverage {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] (J : Pretopology C) : J.toCoverage.toGrothendieck = J.toGrothendieck

def CategoryTheory.Precoverage.toCoverage {C : Type u_1} [Category.{v_1, u_1} C] (J : Precoverage C) [J.HasPullbacks] [J.IsStableUnderBaseChange] : Coverage C

A precoverage with pullbacks defines a coverage.

Equations

• J.toCoverage = { toPrecoverage := J, pullback := ⋯ }

@[simp]

theorem CategoryTheory.Precoverage.toCoverage_toPrecoverage {C : Type u_1} [Category.{v_1, u_1} C] (J : Precoverage C) [J.HasPullbacks] [J.IsStableUnderBaseChange] : J.toCoverage.toPrecoverage = J

theorem CategoryTheory.Precoverage.toGrothendieck_toCoverage {C : Type u_1} [Category.{v_1, u_1} C] {J : Precoverage C} [J.HasPullbacks] [J.IsStableUnderBaseChange] : J.toCoverage.toGrothendieck = J.toGrothendieck

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

The induced coverage by a Grothendieck topology as a precoverage.

Equations

• J.toPrecoverage = J.toCoverage.toPrecoverage

theorem CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) {S : C} (R : Presieve S) : R ∈ J.toPrecoverage.coverings S ↔ Sieve.generate R ∈ J S

instance CategoryTheory.GrothendieckTopology.instHasIsosToPrecoverage {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) : J.toPrecoverage.HasIsos

instance CategoryTheory.GrothendieckTopology.instIsStableUnderCompositionToPrecoverage {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) : J.toPrecoverage.IsStableUnderComposition

instance CategoryTheory.GrothendieckTopology.instIsStableUnderBaseChangeToPrecoverage {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) : J.toPrecoverage.IsStableUnderBaseChange

theorem CategoryTheory.Precoverage.toGrothendieck_le_iff_le_toPrecoverage {C : Type u_1} [Category.{v_1, u_1} C] {K : Precoverage C} {J : GrothendieckTopology C} [K.HasPullbacks] [K.IsStableUnderBaseChange] : K.toGrothendieck ≤ J ↔ K ≤ J.toPrecoverage

toGrothendieck and toPrecoverage form a Galois connection on the domains where they are defined.

theorem CategoryTheory.Coverage.toGrothendieck_toPrecoverage {C : Type u_1} [Category.{v_1, u_1} C] (J : Coverage C) : J.toGrothendieck = J.toGrothendieck

theorem CategoryTheory.Presieve.isSheaf_coverage {C : Type u_2} [Category.{v_1, u_2} C] (K : Coverage C) (P : Functor Cᵒᵖ (Type u_1)) : IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

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} [Category.{v_1, u_2} C] (K L : Coverage C) (P : Functor Cᵒᵖ (Type u_1)) : IsSheaf (K ⊔ L).toGrothendieck P ↔ IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck 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.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange {C : Type u_2} [Category.{v_1, u_2} C] {J : Precoverage C} [J.HasPullbacks] [J.IsStableUnderBaseChange] (P : Functor Cᵒᵖ (Type u_1)) : Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R

theorem CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small {C : Type u_2} [Category.{v_1, u_2} C] {J : Precoverage C} [J.IsStableUnderBaseChange] [J.HasPullbacks] [J.Small] (P : Functor Cᵒᵖ (Type u_1)) : Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀

theorem CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (K : Coverage C) (P : Functor Cᵒᵖ D) : IsSheaf K.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (Limits.IsLimit (P.mapCone (Sieve.generate R).arrows.cocone.op))

theorem CategoryTheory.Presheaf.isSheaf_sup {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (K L : Coverage C) (P : Functor Cᵒᵖ D) : IsSheaf (K ⊔ L).toGrothendieck P ↔ IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P