Subsheaf of types

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

Main results

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

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

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

Equations

• CategoryTheory.Subpresheaf.sheafify J G = { obj := fun (U : Cᵒᵖ) => {s : F.obj U | G.sieveOfSection s ∈ J (Opposite.unop U)}, map := ⋯ }

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

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

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

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

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

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

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

The lift of a presheaf morphism onto the sheafification subpresheaf.

Equations

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

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

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

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

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

A morphism factors through the sheafification of the image presheaf.

Equations

• CategoryTheory.toImagePresheafSheafify J f = CategoryTheory.CategoryStruct.comp (CategoryTheory.toImagePresheaf f) (CategoryTheory.Subpresheaf.homOfLe ⋯)

@[simp]

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

def CategoryTheory.imageSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F 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.

Equations

• CategoryTheory.imageSheaf f = { val := (CategoryTheory.Subpresheaf.sheafify J (CategoryTheory.imagePresheaf f.val)).toPresheaf, cond := ⋯ }

@[simp]

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

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

A morphism factors through the image sheaf.

Equations

• CategoryTheory.toImageSheaf f = { val := CategoryTheory.toImagePresheafSheafify J f.val }

@[simp]

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

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

The inclusion of the image sheaf to the target.

Equations

• CategoryTheory.imageSheafι f = { val := (CategoryTheory.Subpresheaf.sheafify J (CategoryTheory.imagePresheaf f.val)).ι }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

The mono factorization given by image_sheaf for a morphism.

Equations

• CategoryTheory.imageMonoFactorization f = CategoryTheory.Limits.MonoFactorisation.mk (CategoryTheory.imageSheaf f) (CategoryTheory.imageSheafι f) (CategoryTheory.toImageSheaf f) ⋯

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

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.

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