Subsheaf of types

We define the subsheaf of a type-valued presheaf.

Main results

• CategoryTheory.Subfunctor.sheafify : The sheafification of a subpresheaf as a subpresheaf. Note that this is a sheaf only when the whole sheaf is.
• CategoryTheory.Subfunctor.sheafify_isSheaf : The sheafification is a sheaf
• CategoryTheory.Subfunctor.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.imageFactorization.

theorem CategoryTheory.Subfunctor.isSeparated {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subfunctor F) {J : GrothendieckTopology C} (h : Presieve.IsSeparated J F) : Presieve.IsSeparated J G.toFunctor

Every subpresheaf of a separated presheaf is itself separated.

@[deprecated CategoryTheory.Subfunctor.isSeparated (since := "2025-12-11")]

theorem CategoryTheory.Subpresheaf.isSeparated {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subfunctor F) {J : GrothendieckTopology C} (h : Presieve.IsSeparated J F) : Presieve.IsSeparated J G.toFunctor

Alias of CategoryTheory.Subfunctor.isSeparated.

---

Every subpresheaf of a separated presheaf is itself separated.

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

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

@[deprecated CategoryTheory.Subfunctor.sheafify (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.sheafify.

---

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

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

@[deprecated CategoryTheory.Subfunctor.le_sheafify (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.le_sheafify.

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

@[deprecated CategoryTheory.Subfunctor.eq_sheafify (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.eq_sheafify.

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

@[deprecated CategoryTheory.Subfunctor.sheafify_isSheaf (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.sheafify_isSheaf.

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

@[deprecated CategoryTheory.Subfunctor.eq_sheafify_iff (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.eq_sheafify_iff.

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

@[deprecated CategoryTheory.Subfunctor.isSheaf_iff (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.isSheaf_iff.

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

@[deprecated CategoryTheory.Subfunctor.sheafify_sheafify (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.sheafify_sheafify.

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

The lift of a presheaf morphism onto the sheafification subpresheaf.

@[deprecated CategoryTheory.Subfunctor.sheafifyLift (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.sheafifyLift.

---

The lift of a presheaf morphism onto the sheafification subpresheaf.

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

@[deprecated CategoryTheory.Subfunctor.to_sheafifyLift (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.to_sheafifyLift.

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

@[deprecated CategoryTheory.Subfunctor.to_sheafify_lift_unique (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.to_sheafify_lift_unique.

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

@[deprecated CategoryTheory.Subfunctor.sheafify_le (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.sheafify_le.

def CategoryTheory.Subfunctor.toRangeSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) : F' ⟶ (sheafify J (range f)).toFunctor

A morphism factors through the sheafification of the image presheaf.

@[simp]

theorem CategoryTheory.Subfunctor.toRangeSheafify_app_coe {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) (X : Cᵒᵖ) (a✝ : F'.obj X) : ↑((toRangeSheafify J f).app X a✝) = ↑((toRange f).app X a✝)

@[deprecated CategoryTheory.Subfunctor.toRangeSheafify (since := "2025-12-11")]

def CategoryTheory.Subpresheaf.toRangeSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) : F' ⟶ (Subfunctor.sheafify J (Subfunctor.range f)).toFunctor

Alias of CategoryTheory.Subfunctor.toRangeSheafify.

---

A morphism factors through the sheafification of the image presheaf.

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

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

@[simp]

theorem CategoryTheory.Sheaf.image_obj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F F' : Sheaf J (Type w)} (f : F ⟶ F') : (image f).obj = (Subfunctor.sheafify J (Subfunctor.range f.hom)).toFunctor

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

A morphism factors through the image sheaf.

@[simp]

theorem CategoryTheory.Sheaf.toImage_hom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F F' : Sheaf J (Type w)} (f : F ⟶ F') : (toImage f).hom = Subfunctor.toRangeSheafify J f.hom

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

The inclusion of the image sheaf to the target.

@[simp]

theorem CategoryTheory.Sheaf.imageι_hom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F F' : Sheaf J (Type w)} (f : F ⟶ F') : (imageι f).hom = (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι

@[simp]

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

@[simp]

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

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

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

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

The mono factorization given by image_sheaf for a morphism.

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

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

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