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 onC
.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
: GivenK : Coverage C
with associated Grothendieck topologyJ
, aType*
-valued presheaf onC
is a sheaf forK
if and only if it is a sheaf forJ
.
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
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.
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
.
Instances For
- covering : (X : C) → Set (CategoryTheory.Presieve X)
The collection of covering presieves for an object
X
. - pullback : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Presieve X), S ∈ CategoryTheory.Coverage.covering s X → ∃ T, T ∈ CategoryTheory.Coverage.covering s Y ∧ CategoryTheory.Presieve.FactorsThruAlong T S f
Given any covering sieve
S
onX
and a morphismf : Y ⟶ X
, there exists some covering sieveT
onY
such thatT
factors throughS
alongf
.
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
.
Instances For
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
.
Instances For
- of: ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {K : CategoryTheory.Coverage C} (X : C) (S : CategoryTheory.Presieve X), S ∈ CategoryTheory.Coverage.covering K X → CategoryTheory.Coverage.saturate K X (CategoryTheory.Sieve.generate S)
- top: ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {K : CategoryTheory.Coverage C} (X : C), CategoryTheory.Coverage.saturate K 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), CategoryTheory.Coverage.saturate K X R → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → CategoryTheory.Coverage.saturate K Y (CategoryTheory.Sieve.pullback f S)) → CategoryTheory.Coverage.saturate K X S
An auxiliary definition used to define the Grothendieck topology associated to a
coverage. See Coverage.toGrothendieck
.
Instances For
The Grothendieck topology associated to a coverage K
.
It is defined inductively as follows:
- If
S
is a covering presieve forK
, then the sieve generated byS
is a covering sieve for the associated Grothendieck topology. - The top sieves are in the associated Grothendieck topology.
- 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.
Instances For
The two constructions Coverage.toGrothendieck
and Coverage.ofGrothendieck
form
a Galois insertion.
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
.
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.