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
Instances For

    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
    Instances For
      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
        Instances For

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

          Instances For
            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
            Instances For

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