Documentation

Mathlib.CategoryTheory.Sites.Coverage

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.

References #

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

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

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
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.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.coveringx = y

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), 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} [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 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.

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

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

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

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

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.

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
@[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

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

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.

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.