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} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (S : CategoryTheory.Presieve Y) (T : CategoryTheory.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

def CategoryTheory.Presieve.FactorsThru {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} (S : CategoryTheory.Presieve X) (T : CategoryTheory.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_2} [CategoryTheory.Category.{u_1, u_2} C] {X : C} (S : CategoryTheory.Presieve X) (T : CategoryTheory.Presieve X) : S.FactorsThruAlong T (CategoryTheory.CategoryStruct.id X) ↔ S.FactorsThru T

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

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

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

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

theorem CategoryTheory.Coverage.ext_iff {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} (x y : CategoryTheory.Coverage C), x = y ↔ x.covering = y.covering

theorem CategoryTheory.Coverage.ext {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} (x y : CategoryTheory.Coverage C), x.covering = y.covering → x = y

structure CategoryTheory.Coverage (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : 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) → Set (CategoryTheory.Presieve X)

  The collection of covering presieves for an object X.

• pullback : ∀ ⦃X Y : C⦄ (f : Y ⟶ X), ∀ S ∈ self.covering X, ∃ T ∈ self.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.

theorem CategoryTheory.Coverage.pullback {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (self : CategoryTheory.Coverage C) ⦃X : C⦄ ⦃Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Presieve X) : S ∈ self.covering X → ∃ T ∈ self.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} [CategoryTheory.Category.{u_2, u_1} C] : CoeFun (CategoryTheory.Coverage C) fun (x : CategoryTheory.Coverage C) => (X : C) → Set (CategoryTheory.Presieve X)

Equations

• CategoryTheory.Coverage.instCoeFunForallSetPresieve = { coe := CategoryTheory.Coverage.covering }

def CategoryTheory.Coverage.ofGrothendieck (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (J : CategoryTheory.GrothendieckTopology C) : CategoryTheory.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

• CategoryTheory.Coverage.ofGrothendieck C J = { covering := fun (X : C) => {S : CategoryTheory.Presieve X | CategoryTheory.Sieve.generate S ∈ J.sieves X}, pullback := ⋯ }

theorem CategoryTheory.Coverage.ofGrothendieck_iff {C : Type u_2} [CategoryTheory.Category.{u_1, u_2} C] {X : C} {S : CategoryTheory.Presieve X} (J : CategoryTheory.GrothendieckTopology C) : S ∈ (CategoryTheory.Coverage.ofGrothendieck C J).covering X ↔ CategoryTheory.Sieve.generate S ∈ J.sieves X

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

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

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

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

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

def CategoryTheory.Coverage.toGrothendieck (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (K : CategoryTheory.Coverage C) : CategoryTheory.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

• CategoryTheory.Coverage.toGrothendieck C K = { sieves := K.Saturate, top_mem' := ⋯, pullback_stable' := ⋯, transitive' := ⋯ }

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

Equations

• CategoryTheory.Coverage.instPartialOrder = PartialOrder.mk ⋯

def CategoryTheory.Coverage.gi (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : GaloisInsertion (CategoryTheory.Coverage.toGrothendieck C) (CategoryTheory.Coverage.ofGrothendieck C)

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.

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

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 CategoryTheory.Coverage.instSemilatticeSup {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] : SemilatticeSup (CategoryTheory.Coverage C)

Equations

• CategoryTheory.Coverage.instSemilatticeSup = SemilatticeSup.mk ⋯ ⋯ ⋯

@[simp]

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

theorem CategoryTheory.Coverage.mem_toGrothendieck_sieves_of_superset {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (K : CategoryTheory.Coverage C) {X : C} {S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X} (h : R ≤ S.arrows) (hR : R ∈ K.covering X) : S ∈ (CategoryTheory.Coverage.toGrothendieck C K).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} [CategoryTheory.Category.{u_3, u_2} C] (K : CategoryTheory.Coverage C) (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C K) P ↔ ∀ {X : C}, ∀ R ∈ K.covering X, CategoryTheory.Presieve.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} [CategoryTheory.Category.{u_3, u_2} C] (K : CategoryTheory.Coverage C) (L : CategoryTheory.Coverage C) (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (K ⊔ L)) P ↔ CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C K) P ∧ CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C 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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Category.{u_3, u_4} D] (K : CategoryTheory.Coverage C) (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.Coverage.toGrothendieck C K) P ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.covering X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op))

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