Subsheaf of types

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

Main results

• CategoryTheory.GrothendieckTopology.Subpresheaf : A subpresheaf of a presheaf of types.
• CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify : The sheafification of a subpresheaf as a subpresheaf. Note that this is a sheaf only when the whole sheaf is.
• CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify_isSheaf : The sheafification is a sheaf
• CategoryTheory.GrothendieckTopology.Subpresheaf.sheafifyLift : The descent of a map into a sheaf to the sheafification.
• CategoryTheory.GrothendieckTopology.imageSheaf : The image sheaf of a morphism.
• CategoryTheory.GrothendieckTopology.imageFactorization : The image sheaf as a limits.image_factorization.

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.ext {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (x y : CategoryTheory.GrothendieckTopology.Subpresheaf F), x.obj = y.obj → x = y

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.ext_iff {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (x y : CategoryTheory.GrothendieckTopology.Subpresheaf F), x = y ↔ x.obj = y.obj

structure CategoryTheory.GrothendieckTopology.Subpresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) : Type (max u w)

• 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), CategoryTheory.GrothendieckTopology.Subpresheaf.obj s U ⊆ F.map i ⁻¹' CategoryTheory.GrothendieckTopology.Subpresheaf.obj s 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).

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

instance CategoryTheory.GrothendieckTopology.instPartialOrderSubpresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} : PartialOrder (CategoryTheory.GrothendieckTopology.Subpresheaf F)

instance CategoryTheory.GrothendieckTopology.instTopSubpresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} : Top (CategoryTheory.GrothendieckTopology.Subpresheaf F)

instance CategoryTheory.GrothendieckTopology.instNonemptySubpresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} : Nonempty (CategoryTheory.GrothendieckTopology.Subpresheaf F)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (U : Cᵒᵖ) : (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G).obj U = ↑(CategoryTheory.GrothendieckTopology.Subpresheaf.obj G U)

@[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

def CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) : CategoryTheory.Functor Cᵒᵖ (Type w)

The subpresheaf as a presheaf.

instance CategoryTheory.GrothendieckTopology.instCoeHeadObjOppositeToQuiverToCategoryStructOppositeTypeToQuiverToCategoryStructTypesToPrefunctorToPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) {U : Cᵒᵖ} : CoeHead ((CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G).obj U) (F.obj U)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (U : Cᵒᵖ) (x : (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G).obj U) : Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G) F (CategoryTheory.GrothendieckTopology.Subpresheaf.ι G) U x = ↑x

def CategoryTheory.GrothendieckTopology.Subpresheaf.ι {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) : CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G ⟶ F

The inclusion of a subpresheaf to the original presheaf.

instance CategoryTheory.GrothendieckTopology.instMonoFunctorOppositeOppositeTypeTypesCategoryToPresheafι {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) : CategoryTheory.Mono (CategoryTheory.GrothendieckTopology.Subpresheaf.ι G)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe_app_coe {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {G : CategoryTheory.GrothendieckTopology.Subpresheaf F} {G' : CategoryTheory.GrothendieckTopology.Subpresheaf F} (h : G ≤ G') (U : Cᵒᵖ) (x : (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G).obj U) : ↑((CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe h).app U x) = ↑x

def CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {G : CategoryTheory.GrothendieckTopology.Subpresheaf F} {G' : CategoryTheory.GrothendieckTopology.Subpresheaf F} (h : G ≤ G') : CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G ⟶ CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G'

The inclusion of a subpresheaf to a larger subpresheaf

instance CategoryTheory.GrothendieckTopology.instMonoFunctorOppositeOppositeTypeTypesCategoryToPresheafHomOfLe {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {G : CategoryTheory.GrothendieckTopology.Subpresheaf F} {G' : CategoryTheory.GrothendieckTopology.Subpresheaf F} (h : G ≤ G') : CategoryTheory.Mono (CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe h)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {G : CategoryTheory.GrothendieckTopology.Subpresheaf F} {G' : CategoryTheory.GrothendieckTopology.Subpresheaf F} (h : G ≤ G') {Z : CategoryTheory.Functor Cᵒᵖ (Type w)} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Subpresheaf.ι G') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Subpresheaf.ι G) h

@[simp]

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {G : CategoryTheory.GrothendieckTopology.Subpresheaf F} {G' : CategoryTheory.GrothendieckTopology.Subpresheaf F} (h : G ≤ G') : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe h) (CategoryTheory.GrothendieckTopology.Subpresheaf.ι G') = CategoryTheory.GrothendieckTopology.Subpresheaf.ι G

instance CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeOppositeTypeTypesCategoryToPresheafTopSubpresheafInstTopSubpresheafι {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} : CategoryTheory.IsIso (CategoryTheory.GrothendieckTopology.Subpresheaf.ι ⊤)

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.eq_top_iff_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) : G = ⊤ ↔ CategoryTheory.IsIso (CategoryTheory.GrothendieckTopology.Subpresheaf.ι G)

@[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

def CategoryTheory.GrothendieckTopology.Subpresheaf.lift {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) : F' ⟶ CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.lift_ι_assoc {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) {Z : CategoryTheory.Functor Cᵒᵖ (Type w)} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Subpresheaf.lift G f hf) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Subpresheaf.ι G) h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.lift_ι {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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Subpresheaf.lift G f hf) (CategoryTheory.GrothendieckTopology.Subpresheaf.ι G) = f

@[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))

def CategoryTheory.GrothendieckTopology.Subpresheaf.sieveOfSection {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) : CategoryTheory.Sieve U.unop

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.

def CategoryTheory.GrothendieckTopology.Subpresheaf.familyOfElementsOfSection {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) : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G) (CategoryTheory.GrothendieckTopology.Subpresheaf.sieveOfSection G s).arrows

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

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.family_of_elements_compatible {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) : CategoryTheory.Presieve.FamilyOfElements.Compatible (CategoryTheory.GrothendieckTopology.Subpresheaf.familyOfElementsOfSection G s)

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)

def CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) : CategoryTheory.GrothendieckTopology.Subpresheaf F

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

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.le_sheafify {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) : G ≤ CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.eq_sheafify {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (h : CategoryTheory.Presieve.IsSheaf J F) (hG : CategoryTheory.Presieve.IsSheaf J (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G)) : G = CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify_isSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (hF : CategoryTheory.Presieve.IsSheaf J F) : CategoryTheory.Presieve.IsSheaf J (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G))

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.eq_sheafify_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (h : CategoryTheory.Presieve.IsSheaf J F) : G = CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G ↔ CategoryTheory.Presieve.IsSheaf J (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G)

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.isSheaf_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (h : CategoryTheory.Presieve.IsSheaf J F) : CategoryTheory.Presieve.IsSheaf J (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G) ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), CategoryTheory.GrothendieckTopology.Subpresheaf.sieveOfSection G s ∈ CategoryTheory.GrothendieckTopology.sieves J U.unop → s ∈ CategoryTheory.GrothendieckTopology.Subpresheaf.obj G U

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify_sheafify {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (h : CategoryTheory.Presieve.IsSheaf J F) : CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G) = CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G

noncomputable def CategoryTheory.GrothendieckTopology.Subpresheaf.sheafifyLift {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (f : CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G ⟶ F') (h : CategoryTheory.Presieve.IsSheaf J F') : CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G) ⟶ F'

The lift of a presheaf morphism onto the sheafification subpresheaf.

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.to_sheafifyLift {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (f : CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G ⟶ F') (h : CategoryTheory.Presieve.IsSheaf J F') : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe (_ : G ≤ CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G)) (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafifyLift G f h) = f

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.to_sheafify_lift_unique {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (h : CategoryTheory.Presieve.IsSheaf J F') (l₁ : CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G) ⟶ F') (l₂ : CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G) ⟶ F') (e : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe (_ : G ≤ CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G)) l₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe (_ : G ≤ CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G)) l₂) : l₁ = l₂

theorem CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify_le {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F) (G' : CategoryTheory.GrothendieckTopology.Subpresheaf F) (h : G ≤ G') (hF : CategoryTheory.Presieve.IsSheaf J F) (hG' : CategoryTheory.Presieve.IsSheaf J (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf G')) : CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G ≤ G'

@[simp]

theorem CategoryTheory.GrothendieckTopology.imagePresheaf_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) (U : Cᵒᵖ) : CategoryTheory.GrothendieckTopology.Subpresheaf.obj (CategoryTheory.GrothendieckTopology.imagePresheaf f) U = Set.range (f.app U)

def CategoryTheory.GrothendieckTopology.imagePresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) : CategoryTheory.GrothendieckTopology.Subpresheaf F

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.top_subpresheaf_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (U : Cᵒᵖ) : CategoryTheory.GrothendieckTopology.Subpresheaf.obj ⊤ U = ⊤

@[simp]

theorem CategoryTheory.GrothendieckTopology.imagePresheaf_id {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} : CategoryTheory.GrothendieckTopology.imagePresheaf (CategoryTheory.CategoryStruct.id F) = ⊤

@[simp]

theorem CategoryTheory.GrothendieckTopology.toImagePresheaf_app_coe {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) (U : Cᵒᵖ) (x : F'.obj U) : ↑(Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf (CategoryTheory.GrothendieckTopology.imagePresheaf f)) (CategoryTheory.GrothendieckTopology.toImagePresheaf f) U x) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' F f U x

def CategoryTheory.GrothendieckTopology.toImagePresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) : F' ⟶ CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf (CategoryTheory.GrothendieckTopology.imagePresheaf f)

A morphism factors through the image presheaf.

@[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), ↑(Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' (CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf f))) (CategoryTheory.GrothendieckTopology.toImagePresheafSheafify J f) X a) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' F f X a

def CategoryTheory.GrothendieckTopology.toImagePresheafSheafify {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) : F' ⟶ CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf f))

A morphism factors through the sheafification of the image presheaf.

@[simp]

theorem CategoryTheory.GrothendieckTopology.toImagePresheaf_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) {Z : CategoryTheory.Functor Cᵒᵖ (Type w)} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toImagePresheaf f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Subpresheaf.ι (CategoryTheory.GrothendieckTopology.imagePresheaf f)) h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.GrothendieckTopology.toImagePresheaf_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toImagePresheaf f) (CategoryTheory.GrothendieckTopology.Subpresheaf.ι (CategoryTheory.GrothendieckTopology.imagePresheaf f)) = f

theorem CategoryTheory.GrothendieckTopology.imagePresheaf_comp_le {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} {F'' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f₁ : F ⟶ F') (f₂ : F' ⟶ F'') : CategoryTheory.GrothendieckTopology.imagePresheaf (CategoryTheory.CategoryStruct.comp f₁ f₂) ≤ CategoryTheory.GrothendieckTopology.imagePresheaf f₂

instance CategoryTheory.GrothendieckTopology.isIso_toImagePresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ TypeMax} {F' : CategoryTheory.Functor Cᵒᵖ TypeMax} (f : F ⟶ F') [hf : CategoryTheory.Mono f] : CategoryTheory.IsIso (CategoryTheory.GrothendieckTopology.toImagePresheaf f)

@[simp]

theorem CategoryTheory.GrothendieckTopology.imageSheaf_val {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J (Type w)} {F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') : (CategoryTheory.GrothendieckTopology.imageSheaf f).val = CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf f.val))

def CategoryTheory.GrothendieckTopology.imageSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J (Type w)} {F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') : CategoryTheory.Sheaf J (Type w)

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.toImageSheaf_val {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J (Type w)} {F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') : (CategoryTheory.GrothendieckTopology.toImageSheaf f).val = CategoryTheory.GrothendieckTopology.toImagePresheafSheafify J f.val

def CategoryTheory.GrothendieckTopology.toImageSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J (Type w)} {F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') : F ⟶ CategoryTheory.GrothendieckTopology.imageSheaf f

A morphism factors through the image sheaf.

@[simp]

theorem CategoryTheory.GrothendieckTopology.imageSheafι_val {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J (Type w)} {F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') : (CategoryTheory.GrothendieckTopology.imageSheafι f).val = CategoryTheory.GrothendieckTopology.Subpresheaf.ι (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf f.val))

def CategoryTheory.GrothendieckTopology.imageSheafι {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J (Type w)} {F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') : CategoryTheory.GrothendieckTopology.imageSheaf f ⟶ F'

The inclusion of the image sheaf to the target.

@[simp]

theorem CategoryTheory.GrothendieckTopology.toImageSheaf_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J (Type w)} {F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') {Z : CategoryTheory.Sheaf J (Type w)} (h : F' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toImageSheaf f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.imageSheafι f) h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.GrothendieckTopology.toImageSheaf_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J (Type w)} {F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toImageSheaf f) (CategoryTheory.GrothendieckTopology.imageSheafι f) = f

instance CategoryTheory.GrothendieckTopology.instMonoSheafTypeTypesInstCategorySheafImageSheafImageSheafι {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J (Type w)} {F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') : CategoryTheory.Mono (CategoryTheory.GrothendieckTopology.imageSheafι f)

instance CategoryTheory.GrothendieckTopology.instEpiSheafTypeTypesInstCategorySheafImageSheafToImageSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J (Type w)} {F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') : CategoryTheory.Epi (CategoryTheory.GrothendieckTopology.toImageSheaf f)

def CategoryTheory.GrothendieckTopology.imageMonoFactorization {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J (Type w)} {F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') : CategoryTheory.Limits.MonoFactorisation f

The mono factorization given by image_sheaf for a morphism.

noncomputable def CategoryTheory.GrothendieckTopology.imageFactorization {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Sheaf J TypeMax} {F' : CategoryTheory.Sheaf J TypeMax} (f : F ⟶ F') : CategoryTheory.Limits.ImageFactorisation f

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

instance CategoryTheory.GrothendieckTopology.instHasImagesSheafTypeTypesInstCategorySheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} : CategoryTheory.Limits.HasImages (CategoryTheory.Sheaf J (Type (max v u)))