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
.
Equations
- CategoryTheory.Presieve X = (⦃Y : C⦄ → Set (Y ⟶ X))
Instances For
The full subcategory of the over category C/X
consisting of arrows which belong to a
presieve on X
.
Equations
- P.category = CategoryTheory.FullSubcategory fun (f : CategoryTheory.Over X) => P f.hom
Instances For
Construct an object of P.category
.
Equations
- P.categoryMk f hf = { obj := CategoryTheory.Over.mk f, property := hf }
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
.
Equations
- S.diagram = (CategoryTheory.fullSubcategoryInclusion fun (f : CategoryTheory.Over X) => S f.hom).comp (CategoryTheory.Over.forget X)
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
.
Equations
- S.cocone = CategoryTheory.Limits.Cocone.whisker (CategoryTheory.fullSubcategoryInclusion fun (f : CategoryTheory.Over X) => S f.hom) (CategoryTheory.Over.forgetCocone 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 }
.
Equations
Instances For
The singleton presieve.
- mk: ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X}, CategoryTheory.Presieve.singleton' f f
Instances For
The singleton presieve.
Instances For
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
.
- 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 h f)
Instances For
Construct the presieve given by the family of arrows indexed by ι
.
- 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)
Instances For
Given a presieve on F(X)
, we can define a presieve on X
by taking the preimage via F
.
Equations
- CategoryTheory.Presieve.functorPullback F R f = R (F.map f)
Instances For
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.
- 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.
Instances
For all arrows f
and g
in R
, the pullback of f
and g
exists.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
.
Equations
- CategoryTheory.Presieve.functorPushforward F S f = ∃ (Z : C) (g : Z ⟶ X) (h : Y ⟶ F.obj Z), S g ∧ f = CategoryTheory.CategoryStruct.comp h (F.map g)
Instances For
An auxiliary definition in order to fix the choice of the preimages between various definitions.
- preobj : C
an object in the source category
- premap : self.preobj ⟶ X
a map in the source category which has to be in the presieve
- lift : Y ⟶ F.obj self.preobj
the morphism which appear in the factorisation
- cover : S self.premap
the condition that
premap
is in the presieve - fac : f = CategoryTheory.CategoryStruct.comp self.lift (F.map self.premap)
the factorisation of the morphism
Instances For
the condition that premap
is in the presieve
the factorisation of the morphism
The fixed choice of a preimage.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For an object X
of a category C
, a Sieve X
is a set of morphisms to X
which is closed under
left-composition.
- arrows : CategoryTheory.Presieve X
the underlying presieve
- downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, self.arrows f → ∀ (g : Z ⟶ Y), self.arrows (CategoryTheory.CategoryStruct.comp g f)
stability by precomposition
Instances For
stability by precomposition
Equations
- CategoryTheory.Sieve.instCoeFunPresieve = { coe := CategoryTheory.Sieve.arrows }
The supremum of a collection of sieves: the union of them all.
Equations
- CategoryTheory.Sieve.sup 𝒮 = { arrows := fun (Y : C) => {f : Y ⟶ X | ∃ S ∈ 𝒮, S.arrows f}, downward_closed := ⋯ }
Instances For
The infimum of a collection of sieves: the intersection of them all.
Equations
- CategoryTheory.Sieve.inf 𝒮 = { arrows := fun (x : C) => {f : x ⟶ X | ∀ S ∈ 𝒮, S.arrows f}, downward_closed := ⋯ }
Instances For
The union of two sieves is a sieve.
Equations
Instances For
The intersection of two sieves is a sieve.
Equations
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.
Equations
- CategoryTheory.Sieve.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The maximal sieve always exists.
Generate the smallest sieve containing the given set of arrows.
Equations
- CategoryTheory.Sieve.generate R = { arrows := fun (Z : C) (f : Z ⟶ X) => ∃ (Y : C) (h : Z ⟶ Y) (g : Y ⟶ X), R g ∧ CategoryTheory.CategoryStruct.comp h g = f, downward_closed := ⋯ }
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
.
Equations
- CategoryTheory.Sieve.bind S R = { arrows := S.bind fun (Y : C) (f : Y ⟶ X) (h : S f) => (R h).arrows, downward_closed := ⋯ }
Instances For
Alias of CategoryTheory.Sieve.generate_le_iff
.
Show that there is a galois insertion (generate, set_over).
Equations
- One or more equations did not get rendered due to their size.
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.
The sieve of X
generated by family of morphisms Y i ⟶ X
.
Equations
Instances For
The sieve generated by two morphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sieve of X : C
that is generated by a family of objects Y : I → C
:
it consists of morphisms to X
which factor through at least one of the Y i
.
Equations
- CategoryTheory.Sieve.ofObjects Y X = { arrows := fun (Z : C) (x : Z ⟶ X) => ∃ (i : I), Nonempty (Z ⟶ Y i), downward_closed := ⋯ }
Instances For
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
.
Equations
- CategoryTheory.Sieve.pullback h S = { arrows := fun (Y_1 : C) (sl : Y_1 ⟶ Y) => S.arrows (CategoryTheory.CategoryStruct.comp sl h), downward_closed := ⋯ }
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
.
Equations
- CategoryTheory.Sieve.pushforward f R = { arrows := fun (Z : C) (gf : Z ⟶ X) => ∃ (g : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g f = gf ∧ R.arrows g, downward_closed := ⋯ }
Instances For
If f
is a monomorphism, the pushforward-pullback adjunction on sieves is coreflective.
Equations
- CategoryTheory.Sieve.galoisCoinsertionOfMono f = ⋯.toGaloisCoinsertion ⋯
Instances For
If f
is a split epi, the pushforward-pullback adjunction on sieves is reflective.
Equations
- CategoryTheory.Sieve.galoisInsertionOfIsSplitEpi f = ⋯.toGaloisInsertion ⋯
Instances For
If R
is a sieve, then the CategoryTheory.Presieve.functorPullback
of R
is actually a sieve.
Equations
- CategoryTheory.Sieve.functorPullback F R = { arrows := CategoryTheory.Presieve.functorPullback F R.arrows, downward_closed := ⋯ }
Instances For
The sieve generated by the image of R
under F
.
Equations
- CategoryTheory.Sieve.functorPushforward F R = { arrows := CategoryTheory.Presieve.functorPushforward F R.arrows, downward_closed := ⋯ }
Instances For
When F
is essentially surjective and full, the galois connection is a galois insertion.
Equations
- CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion F X = ⋯.toGaloisInsertion ⋯
Instances For
When F
is fully faithful, the galois connection is a galois coinsertion.
Equations
- CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion F X = ⋯.toGaloisCoinsertion ⋯
Instances For
A sieve induces a presheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If a sieve S is contained in a sieve T, then we have a morphism of presheaves on their induced presheaves.
Equations
- CategoryTheory.Sieve.natTransOfLe h = { app := fun (Y : Cᵒᵖ) (f : S.functor.obj Y) => ⟨↑f, ⋯⟩, naturality := ⋯ }
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.
Equations
- ⋯ = ⋯
A natural transformation to a representable functor induces a sieve. This is the left inverse of
functorInclusion
, shown in sieveOfSubfunctor_functorInclusion
.
Equations
- CategoryTheory.Sieve.sieveOfSubfunctor f = { arrows := fun (Y : C) (g : Y ⟶ X) => ∃ (t : R.obj (Opposite.op Y)), f.app (Opposite.op Y) t = g, downward_closed := ⋯ }
Instances For
Equations
- ⋯ = ⋯