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
    Equations
    • CategoryTheory.GrothendieckTopology.instPartialOrderSubpresheaf = PartialOrder.lift CategoryTheory.GrothendieckTopology.Subpresheaf.obj
    Equations
    • CategoryTheory.GrothendieckTopology.instTopSubpresheaf = { top := { obj := fun (U : Cᵒᵖ) => , map := } }

    The subpresheaf as a presheaf.

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

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

      Equations
      Instances For

        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
        Instances For

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

          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

              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

                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