Theory of sieves #
- For an object
X
of a categoryC
, aSieve X
is a set of morphisms toX
which is closed under left-composition. - The complete lattice structure on sieves is given, as well as the Galois insertion given by downward-closing.
- A
Sieve X
(functorially) induces a presheaf onC
together with a monomorphism to the yoneda embedding ofX
.
Tags #
sieve, pullback
A set of arrows all with codomain X
.
Instances For
Given a sieve S
on X : C
, its associated diagram S.diagram
is defined to be
the natural functor from the full subcategory of the over category C/X
consisting
of arrows in S
to C
.
Instances For
Given a sieve S
on X : C
, its associated cocone S.cocone
is defined to be
the natural cocone over the diagram defined above with cocone point X
.
Instances For
Given a set of arrows S
all with codomain X
, and a set of arrows with codomain Y
for each
f : Y ⟶ X
in S
, produce a set of arrows with codomain X
:
{ g ≫ f | (f : Y ⟶ X) ∈ S, (g : Z ⟶ Y) ∈ R f }
.
Instances For
- mk: ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X}, CategoryTheory.Presieve.singleton' f f
The singleton presieve.
Instances For
The singleton presieve.
Instances For
- mk: ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} [inst_1 : CategoryTheory.Limits.HasPullbacks C] {R : CategoryTheory.Presieve X} (Z : C) (h : Z ⟶ X), R h → CategoryTheory.Presieve.pullbackArrows f R CategoryTheory.Limits.pullback.snd
Pullback a set of arrows with given codomain along a fixed map, by taking the pullback in the
category.
This is not the same as the arrow set of Sieve.pullback
, but there is a relation between them
in pullbackArrows_comm
.
Instances For
- mk: ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (i : ι), CategoryTheory.Presieve.ofArrows Y f (f i)
Construct the presieve given by the family of arrows indexed by ι
.
Instances For
Given a presieve on F(X)
, we can define a presieve on X
by taking the preimage via F
.
Instances For
- has_pullbacks : ∀ {Y Z : C} {f : Y ⟶ X}, R f → ∀ {g : Z ⟶ X}, R g → CategoryTheory.Limits.HasPullback f g
For all arrows
f
andg
inR
, the pullback off
andg
exists.
Given a presieve R
on X
, the predicate R.hasPullbacks
means that for all arrows f
and
g
in R
, the pullback of f
and g
exists.
Instances
Given a presieve on X
, we can define a presieve on F(X)
(which is actually a sieve)
by taking the sieve generated by the image via F
.
Instances For
- preobj : C
an object in the source category
- premap : s.preobj ⟶ X
a map in the source category which has to be in the presieve
- lift : Y ⟶ F.obj s.preobj
the morphism which appear in the factorisation
- cover : S s.premap
the condition that
premap
is in the presieve - fac : f = CategoryTheory.CategoryStruct.comp s.lift (F.map s.premap)
the factorisation of the morphism
An auxiliary definition in order to fix the choice of the preimages between various definitions.
Instances For
The fixed choice of a preimage.
Instances For
- arrows : CategoryTheory.Presieve X
the underlying presieve
- downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, s.arrows f → ∀ (g : Z ⟶ Y), s.arrows (CategoryTheory.CategoryStruct.comp g f)
stability by precomposition
For an object X
of a category C
, a Sieve X
is a set of morphisms to X
which is closed under
left-composition.
Instances For
The supremum of a collection of sieves: the union of them all.
Instances For
The infimum of a collection of sieves: the intersection of them all.
Instances For
The union of two sieves is a sieve.
Instances For
The intersection of two sieves is a sieve.
Instances For
Sieves on an object X
form a complete lattice.
We generate this directly rather than using the galois insertion for nicer definitional properties.
The maximal sieve always exists.
Generate the smallest sieve containing the given set of arrows.
Instances For
Given a presieve on X
, and a sieve on each domain of an arrow in the presieve, we can bind to
produce a sieve on X
.
Instances For
Show that there is a galois insertion (generate, set_over).
Instances For
If the identity arrow is in a sieve, the sieve is maximal.
If an arrow set contains a split epi, it generates the maximal sieve.
Given a morphism h : Y ⟶ X
, send a sieve S on X to a sieve on Y
as the inverse image of S with _ ≫ h
.
That is, Sieve.pullback S h := (≫ h) '⁻¹ S
.
Instances For
Push a sieve R
on Y
forward along an arrow f : Y ⟶ X
: gf : Z ⟶ X
is in the sieve if gf
factors through some g : Z ⟶ Y
which is in R
.
Instances For
If f
is a monomorphism, the pushforward-pullback adjunction on sieves is coreflective.
Instances For
If f
is a split epi, the pushforward-pullback adjunction on sieves is reflective.
Instances For
If R
is a sieve, then the CategoryTheory.Presieve.functorPullback
of R
is actually a sieve.
Instances For
The sieve generated by the image of R
under F
.
Instances For
When F
is essentially surjective and full, the galois connection is a galois insertion.
Instances For
When F
is fully faithful, the galois connection is a galois coinsertion.
Instances For
A sieve induces a presheaf.
Instances For
If a sieve S is contained in a sieve T, then we have a morphism of presheaves on their induced presheaves.
Instances For
The natural inclusion from the functor induced by a sieve to the yoneda embedding.
Instances For
The presheaf induced by a sieve is a subobject of the yoneda embedding.
A natural transformation to a representable functor induces a sieve. This is the left inverse of
functorInclusion
, shown in sieveOfSubfunctor_functorInclusion
.