Documentation

Mathlib.CategoryTheory.Sites.Subsheaf

Subsheaf of types #

We define the sub(pre)sheaf of a type valued presheaf.

Main results #

A subpresheaf of a presheaf consists of a subset of F.obj U for every U, compatible with the restriction maps F.map i.

  • obj : (U : Cᵒᵖ) → Set (F.obj U)

    If G is a sub-presheaf of F, then the sections of G on U forms a subset of sections of F on U.

  • map : ∀ {U V : Cᵒᵖ} (i : U V), self.obj U F.map i ⁻¹' self.obj V

    If G is a sub-presheaf of F and i : U ⟶ V, then for each G-sections on U x, F i x is in F(V).

Instances For

    If G is a sub-presheaf of F and i : U ⟶ V, then for each G-sections on U x, F i x is in F(V).

    Equations
    • CategoryTheory.GrothendieckTopology.instPartialOrderSubpresheaf = PartialOrder.lift CategoryTheory.GrothendieckTopology.Subpresheaf.obj
    Equations
    • CategoryTheory.GrothendieckTopology.instTopSubpresheaf = { top := { obj := fun (U : Cᵒᵖ) => , map := } }
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf_map_coe {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (U : Cᵒᵖ) (V : Cᵒᵖ) (i : U V) (x : (G.obj U)) :
    (G.toPresheaf.map i x) = F.map i x

    The subpresheaf as a presheaf.

    Equations
    • G.toPresheaf = { obj := fun (U : Cᵒᵖ) => (G.obj U), map := fun (U V : Cᵒᵖ) (i : U V) (x : (G.obj U)) => F.map i x, , map_id := , map_comp := }
    Instances For

      The inclusion of a subpresheaf to the original presheaf.

      Equations
      • G = { app := fun (U : Cᵒᵖ) (x : G.toPresheaf.obj U) => x, naturality := }
      Instances For

        The inclusion of a subpresheaf to a larger subpresheaf

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.Subpresheaf.lift_app_coe {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (f : F' F) (hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x G.obj U) (U : Cᵒᵖ) (x : F'.obj U) :
          ((G.lift f hf).app U x) = f.app U x

          If the image of a morphism falls in a subpresheaf, then the morphism factors through it.

          Equations
          • G.lift f hf = { app := fun (U : Cᵒᵖ) (x : F'.obj U) => f.app U x, , naturality := }
          Instances For
            @[simp]
            theorem CategoryTheory.GrothendieckTopology.Subpresheaf.sieveOfSection_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) {U : Cᵒᵖ} (s : F.obj U) (V : C) (f : V U.unop) :
            (G.sieveOfSection s).arrows f = (F.map f.op s G.obj { unop := V })

            Given a subpresheaf G of F, an F-section s on U, we may define a sieve of U consisting of all f : V ⟶ U such that the restriction of s along f is in G.

            Equations
            • G.sieveOfSection s = { arrows := fun (V : C) (f : V U.unop) => F.map f.op s G.obj { unop := V }, downward_closed := }
            Instances For

              Given an F-section s on U and a subpresheaf G, we may define a family of elements in G consisting of the restrictions of s

              Equations
              • G.familyOfElementsOfSection s i hi = F.map i.op s, hi
              Instances For
                theorem CategoryTheory.GrothendieckTopology.Subpresheaf.nat_trans_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (f : F' G.toPresheaf) {U : Cᵒᵖ} {V : Cᵒᵖ} (i : U V) (x : F'.obj U) :
                (f.app V (F'.map i x)) = F.map i (f.app U x)

                The sheafification of a subpresheaf as a subpresheaf. Note that this is a sheaf only when the whole presheaf is a sheaf.

                Equations
                Instances For

                  The lift of a presheaf morphism onto the sheafification subpresheaf.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    The image presheaf of a morphism, whose components are the set-theoretic images.

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.GrothendieckTopology.toImagePresheafSheafify_app_coe {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F' F) (X : Cᵒᵖ) :
                      ∀ (a : F'.obj X), ((J.toImagePresheafSheafify f).app X a) = f.app X a

                      The image sheaf of a morphism between sheaves, defined to be the sheafification of image_presheaf.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        A morphism factors through the image sheaf.

                        Equations
                        Instances For

                          The inclusion of the image sheaf to the target.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            The mono factorization given by image_sheaf for a morphism.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              The mono factorization given by image_sheaf for a morphism is an image.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For