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.

Instances For
    @[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 : ↑(CategoryTheory.GrothendieckTopology.Subpresheaf.obj G U)) :
    ↑((CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G).map i x) = Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor U V i x
    @[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), Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' F f U x CategoryTheory.GrothendieckTopology.Subpresheaf.obj G U) (U : Cᵒᵖ) (x : F'.obj U) :
    ↑(Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G) (CategoryTheory.GrothendieckTopology.Subpresheaf.lift G f hf) U x) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' F f U x

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

    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) :
      (CategoryTheory.GrothendieckTopology.Subpresheaf.sieveOfSection G s).arrows f = (Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor (Opposite.op U.unop) (Opposite.op V) f.op s CategoryTheory.GrothendieckTopology.Subpresheaf.obj G (Opposite.op 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.

      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' CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G) {U : Cᵒᵖ} {V : Cᵒᵖ} (i : U V) (x : F'.obj U) :
        ↑(Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G) f V (Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F'.toPrefunctor U V i x)) = Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor U V i ↑(Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G) f U x)

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

        Instances For

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

          Instances For

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

            Instances For

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

              Instances For