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.

Equations
Instances For
    Equations
    • CategoryTheory.instCompleteLatticePresieve = id inferInstance
    Equations
    • CategoryTheory.Presieve.instInhabited = { default := }
    @[reducible, inline]

    The full subcategory of the over category C/X consisting of arrows which belong to a presieve on X.

    Equations
    Instances For
      @[reducible, inline]
      abbrev CategoryTheory.Presieve.categoryMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Presieve X) {Y : C} (f : Y X) (hf : P f) :
      P.category

      Construct an object of P.category.

      Equations
      Instances For
        @[reducible, inline]

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

          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
          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 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 }.

            Equations
            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 fCategoryTheory.Presieve Y} {g : Z Y} (h₁ : S f) (h₂ : R h₁ 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

                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_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 f HC) (k : Y : C⦄ → (f : Y X) → (H : CategoryTheory.Presieve.ofArrows Z g f) → (i : j f H) → W f H i Y) :
                    ((CategoryTheory.Presieve.ofArrows Z g).bind fun (Y : C) (f : Y X) (H : CategoryTheory.Presieve.ofArrows Z g f) => CategoryTheory.Presieve.ofArrows (W f H) (k f H)) = CategoryTheory.Presieve.ofArrows (fun (i : (i : ι) × j (g i) ) => W (g i.fst) i.snd) fun (ij : (i : ι) × j (g i) ) => CategoryTheory.CategoryStruct.comp (k (g ij.fst) ij.snd) (g ij.fst)
                    theorem CategoryTheory.Presieve.ofArrows_surj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ιC} (f : (i : ι) → Y i X) {Z : C} (g : Z X) (hg : CategoryTheory.Presieve.ofArrows Y f g) :
                    ∃ (i : ι) (h : Y i = Z), g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ) (f i)

                    Given a presieve on F(X), we can define a presieve on X by taking the preimage via F.

                    Equations
                    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
                        theorem CategoryTheory.Presieve.hasPullbacks.has_pullbacks {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Presieve X} [self : R.hasPullbacks] {Y : C} {Z : C} {f : Y X} :
                        R f∀ {g : Z X}, R gCategoryTheory.Limits.HasPullback f g

                        For all arrows f and g in R, the pullback of f and g exists.

                        instance CategoryTheory.Presieve.instHasPullbackOfHasPullbacksOfArrows {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type v₂} {X : αC} {B : C} (π : (a : α) → X a B) [(CategoryTheory.Presieve.ofArrows X π).hasPullbacks] (a : α) (b : α) :
                        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
                        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₂)

                          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 fixed choice of a preimage.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            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
                                @[simp]
                                theorem CategoryTheory.Sieve.downward_closed {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (self : CategoryTheory.Sieve X) {Y : C} {Z : C} {f : Y X} :
                                self.arrows f∀ (g : Z Y), self.arrows (CategoryTheory.CategoryStruct.comp g f)

                                stability by precomposition

                                Equations
                                • CategoryTheory.Sieve.instCoeFunPresieve = { coe := CategoryTheory.Sieve.arrows }
                                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.

                                Equations
                                Instances For

                                  The infimum of a collection of sieves: the intersection of them all.

                                  Equations
                                  Instances For

                                    The union of two sieves is a sieve.

                                    Equations
                                    • S.union R = { arrows := fun (Y : C) (f : Y X) => S.arrows f R.arrows f, downward_closed := }
                                    Instances For

                                      The intersection of two sieves is a sieve.

                                      Equations
                                      • S.inter R = { arrows := fun (Y : C) (f : Y X) => S.arrows f R.arrows f, downward_closed := }
                                      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

                                        The maximal sieve always exists.

                                        Equations
                                        • CategoryTheory.Sieve.sieveInhabited = { default := }
                                        @[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 SSs, S.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 : CategoryTheory.Sieve X) (_ : S Ss), 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
                                        @[simp]
                                        theorem CategoryTheory.Sieve.generate_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X) (Z : C) (f : Z X) :
                                        (CategoryTheory.Sieve.generate R).arrows f = ∃ (Y : C) (h : Z Y) (g : Y X), R g CategoryTheory.CategoryStruct.comp h g = f

                                        Generate the smallest sieve containing the given set of arrows.

                                        Equations
                                        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 fCategoryTheory.Sieve Y) :
                                          (CategoryTheory.Sieve.bind S R).arrows = S.bind fun (Y : C) (f : Y X) (h : S f) => (R 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 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.

                                          Equations
                                          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).

                                            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.

                                              @[simp]
                                              theorem CategoryTheory.Sieve.comp_mem_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (i : X Y) (f : Y Z) [CategoryTheory.IsIso i] (S : CategoryTheory.Sieve Z) :
                                              S.arrows (CategoryTheory.CategoryStruct.comp i f) S.arrows f
                                              @[reducible, inline]
                                              abbrev CategoryTheory.Sieve.ofArrows {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : IC) (f : (i : I) → Y i X) :

                                              The sieve of X generated by family of morphisms Y i ⟶ X.

                                              Equations
                                              Instances For
                                                theorem CategoryTheory.Sieve.ofArrows_mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : IC) (f : (i : I) → Y i X) (i : I) :
                                                theorem CategoryTheory.Sieve.mem_ofArrows_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : IC) (f : (i : I) → Y i X) {W : C} (g : W X) :
                                                (CategoryTheory.Sieve.ofArrows Y f).arrows g ∃ (i : I) (a : W Y i), g = CategoryTheory.CategoryStruct.comp a (f i)

                                                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
                                                Instances For
                                                  theorem CategoryTheory.Sieve.mem_ofObjects_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (Y : IC) {Z : C} {X : C} (g : Z X) :
                                                  (CategoryTheory.Sieve.ofObjects Y X).arrows g ∃ (i : I), Nonempty (Z Y i)
                                                  @[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.

                                                  Equations
                                                  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) :
                                                    (CategoryTheory.Sieve.pushforward f R).arrows gf = ∃ (g : Z Y), CategoryTheory.CategoryStruct.comp g f = gf R.arrows g

                                                    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
                                                    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 fCategoryTheory.Sieve Y) (f : Y X) (h : S 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 fCategoryTheory.Sieve Y) (f : Y X) (h : S f) :

                                                      If f is a monomorphism, the pushforward-pullback adjunction on sieves is coreflective.

                                                      Equations
                                                      Instances For

                                                        If f is a split epi, the pushforward-pullback adjunction on sieves is reflective.

                                                        Equations
                                                        Instances For

                                                          If R is a sieve, then the CategoryTheory.Presieve.functorPullback of R is actually a sieve.

                                                          Equations
                                                          Instances For

                                                            The sieve generated by the image of R under F.

                                                            Equations
                                                            Instances For

                                                              When F is essentially surjective and full, the galois connection is a galois insertion.

                                                              Equations
                                                              Instances For

                                                                When F is fully faithful, the galois connection is a galois coinsertion.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem CategoryTheory.Sieve.mem_functorPushforward_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : D} {S : CategoryTheory.Sieve X} {e : C D} {f : Y e.functor.obj X} :
                                                                  (CategoryTheory.Sieve.functorPushforward e.functor S).arrows f S.arrows (CategoryTheory.CategoryStruct.comp (e.inverse.map f) (e.unitInv.app X))
                                                                  @[simp]
                                                                  theorem CategoryTheory.Sieve.mem_functorPushforward_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {Y : C} {X : D} {S : CategoryTheory.Sieve X} {e : C D} {f : Y e.inverse.obj X} :
                                                                  (CategoryTheory.Sieve.functorPushforward e.inverse S).arrows f S.arrows (CategoryTheory.CategoryStruct.comp (e.functor.map f) (e.counit.app X))
                                                                  @[simp]
                                                                  theorem CategoryTheory.Sieve.functor_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (Y : Cᵒᵖ) :
                                                                  S.functor.obj Y = { g : Opposite.unop Y X // S.arrows g }
                                                                  @[simp]
                                                                  theorem CategoryTheory.Sieve.functor_map_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) :
                                                                  ∀ {X_1 Y : Cᵒᵖ} (f : X_1 Y) (g : { g : Opposite.unop X_1 X // S.arrows g }), (S.functor.map f g) = CategoryTheory.CategoryStruct.comp f.unop g

                                                                  A sieve induces a presheaf.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem CategoryTheory.Sieve.natTransOfLe_app_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {T : CategoryTheory.Sieve X} (h : S T) (Y : Cᵒᵖ) (f : S.functor.obj Y) :
                                                                    ((CategoryTheory.Sieve.natTransOfLe h).app Y f) = f
                                                                    def CategoryTheory.Sieve.natTransOfLe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {T : CategoryTheory.Sieve X} (h : S T) :
                                                                    S.functor T.functor

                                                                    If a sieve S is contained in a sieve T, then we have a morphism of presheaves on their induced presheaves.

                                                                    Equations
                                                                    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 : S.functor.obj Y) :
                                                                      S.functorInclusion.app Y f = f
                                                                      def CategoryTheory.Sieve.functorInclusion {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) :
                                                                      S.functor CategoryTheory.yoneda.obj X

                                                                      The natural inclusion from the functor induced by a sieve to the yoneda embedding.

                                                                      Equations
                                                                      • S.functorInclusion = { app := fun (Y : Cᵒᵖ) (f : S.functor.obj Y) => f, naturality := }
                                                                      Instances For

                                                                        The presheaf induced by a sieve is a subobject of the yoneda embedding.

                                                                        Equations
                                                                        • =
                                                                        @[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 : R.obj (Opposite.op Y)), f.app (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.

                                                                        Equations
                                                                        Instances For