Documentation

Mathlib.CategoryTheory.Sites.Sieves

Theory of sieves #

Tags #

sieve, pullback

def CategoryTheory.Presieve {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) :
Type (max u₁ v₁)

A set of arrows all with codomain X.

Instances For
    @[inline, reducible]

    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
      @[inline, reducible]

      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
        def CategoryTheory.Presieve.bind {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Presieve X) (R : Y : C⦄ → f : Y X⦄ → S Y fCategoryTheory.Presieve Y) :

        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
          @[simp]
          theorem CategoryTheory.Presieve.bind_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : Y X) {S : CategoryTheory.Presieve X} {R : Y : C⦄ → f : Y X⦄ → S Y fCategoryTheory.Presieve Y} {g : Z Y} (h₁ : S Y f) (h₂ : R Y f h₁ Z g) :
          inductive CategoryTheory.Presieve.singleton' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Y X) ⦃Y : C :
          (Y X) → Prop

          The singleton presieve.

          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.

              Instances For
                inductive CategoryTheory.Presieve.ofArrows {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} (Y : ιC) (f : (i : ι) → Y i X) :

                Construct the presieve given by the family of arrows indexed by ι.

                Instances For
                  theorem CategoryTheory.Presieve.ofArrows_pullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Y X) [CategoryTheory.Limits.HasPullbacks C] {ι : Type u_1} (Z : ιC) (g : (i : ι) → Z i X) :
                  theorem CategoryTheory.Presieve.ofArrows_bind {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} (Z : ιC) (g : (i : ι) → Z i X) (j : Y : C⦄ → (f : Y X) → CategoryTheory.Presieve.ofArrows Z g fType u_2) (W : Y : C⦄ → (f : Y X) → (H : CategoryTheory.Presieve.ofArrows Z g f) → j Y f HC) (k : Y : C⦄ → (f : Y X) → (H : CategoryTheory.Presieve.ofArrows Z g f) → (i : j Y f H) → W Y f H i Y) :
                  (CategoryTheory.Presieve.bind (CategoryTheory.Presieve.ofArrows Z g) fun Y f H => CategoryTheory.Presieve.ofArrows (W Y f H) (k Y f H)) = CategoryTheory.Presieve.ofArrows (fun i => W (Z i.fst) (g i.fst) (_ : CategoryTheory.Presieve.ofArrows Z g (g i.fst)) i.snd) fun ij => CategoryTheory.CategoryStruct.comp (k (Z ij.fst) (g ij.fst) (_ : CategoryTheory.Presieve.ofArrows Z g (g ij.fst)) ij.snd) (g ij.fst)

                  Given a presieve on F(X), we can define a presieve on X by taking the preimage via 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.

                    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
                        structure CategoryTheory.Presieve.FunctorPushforwardStructure {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (S : CategoryTheory.Presieve X) {Y : D} (f : Y F.obj X) :
                        Type (max (max u₁ v₁) v₂)
                        • 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
                          structure CategoryTheory.Sieve {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) :
                          Type (max u₁ v₁)

                          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
                            theorem CategoryTheory.Sieve.arrows_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Sieve X} {S : CategoryTheory.Sieve X} :
                            R.arrows = S.arrowsR = S
                            theorem CategoryTheory.Sieve.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Sieve X} {S : CategoryTheory.Sieve X} (h : ∀ ⦃Y : C⦄ (f : Y X), R.arrows f S.arrows f) :
                            R = S
                            theorem CategoryTheory.Sieve.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Sieve X} {S : CategoryTheory.Sieve X} :
                            R = S ∀ ⦃Y : C⦄ (f : Y X), R.arrows f S.arrows f

                            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.

                                    @[simp]
                                    theorem CategoryTheory.Sieve.sInf_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Ss : Set (CategoryTheory.Sieve X)} {Y : C} (f : Y X) :
                                    (sInf Ss).arrows f ∀ (S : CategoryTheory.Sieve X), S SsS.arrows f
                                    @[simp]
                                    theorem CategoryTheory.Sieve.sSup_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Ss : Set (CategoryTheory.Sieve X)} {Y : C} (f : Y X) :
                                    (sSup Ss).arrows f S x, S.arrows f
                                    @[simp]
                                    theorem CategoryTheory.Sieve.inter_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Sieve X} {S : CategoryTheory.Sieve X} {Y : C} (f : Y X) :
                                    (R S).arrows f R.arrows f S.arrows f
                                    @[simp]
                                    theorem CategoryTheory.Sieve.union_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Sieve X} {S : CategoryTheory.Sieve X} {Y : C} (f : Y X) :
                                    (R S).arrows f R.arrows f S.arrows f
                                    @[simp]
                                    theorem CategoryTheory.Sieve.top_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Y X) :
                                    .arrows f

                                    Generate the smallest sieve containing the given set of arrows.

                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.Sieve.bind_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Presieve X) (R : Y : C⦄ → f : Y X⦄ → S Y fCategoryTheory.Sieve Y) :
                                      (CategoryTheory.Sieve.bind S R).arrows = CategoryTheory.Presieve.bind S fun Y f h => (R Y f h).arrows
                                      def CategoryTheory.Sieve.bind {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Presieve X) (R : Y : C⦄ → f : Y X⦄ → S Y fCategoryTheory.Sieve Y) :

                                      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
                                        def CategoryTheory.Sieve.giGenerate {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} :
                                        GaloisInsertion CategoryTheory.Sieve.generate CategoryTheory.Sieve.arrows

                                        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.

                                          @[simp]
                                          theorem CategoryTheory.Sieve.pullback_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (h : Y X) (S : CategoryTheory.Sieve X) (Y : C) (sl : Y Y) :

                                          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
                                            @[simp]
                                            theorem CategoryTheory.Sieve.pushforward_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Y X) (R : CategoryTheory.Sieve Y) (Z : C) (gf : Z X) :

                                            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
                                              theorem CategoryTheory.Sieve.pushforward_le_bind_of_mem {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (S : CategoryTheory.Presieve X) (R : Y : C⦄ → f : Y X⦄ → S Y fCategoryTheory.Sieve Y) (f : Y X) (h : S Y f) :
                                              theorem CategoryTheory.Sieve.le_pullback_bind {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (S : CategoryTheory.Presieve X) (R : Y : C⦄ → f : Y X⦄ → S Y fCategoryTheory.Sieve Y) (f : Y X) (h : S Y f) :

                                              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

                                                  The sieve generated by the image of R under F.

                                                  Instances For
                                                    @[simp]
                                                    @[simp]
                                                    theorem CategoryTheory.Sieve.functor_map_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) :
                                                    ∀ {X Y : Cᵒᵖ} (f : X Y) (g : { g // S.arrows g }), ↑((CategoryTheory.Sieve.functor S).map f g) = CategoryTheory.CategoryStruct.comp f.unop g

                                                    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
                                                        @[simp]
                                                        theorem CategoryTheory.Sieve.functorInclusion_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (Y : Cᵒᵖ) (f : (CategoryTheory.Sieve.functor S).obj Y) :
                                                        Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types (CategoryTheory.Sieve.functor S) (CategoryTheory.yoneda.obj X) (CategoryTheory.Sieve.functorInclusion S) Y f = f

                                                        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.

                                                          @[simp]
                                                          theorem CategoryTheory.Sieve.sieveOfSubfunctor_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : R CategoryTheory.yoneda.obj X) (Y : C) (g : Y X) :
                                                          (CategoryTheory.Sieve.sieveOfSubfunctor f).arrows g = t, Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types R (CategoryTheory.yoneda.obj X) f (Opposite.op Y) t = g

                                                          A natural transformation to a representable functor induces a sieve. This is the left inverse of functorInclusion, shown in sieveOfSubfunctor_functorInclusion.

                                                          Instances For