# Documentation

Mathlib.CategoryTheory.Sites.Subsheaf

# 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 : } {F : } (x y : ), x.obj = y.objx = y
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.ext_iff {C : Type u} :
∀ {inst : } {F : } (x y : ), x = y x.obj = y.obj
structure CategoryTheory.GrothendieckTopology.Subpresheaf {C : Type u} (F : ) :
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),

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.

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf_map_coe {C : Type u} {F : } (U : Cᵒᵖ) (V : Cᵒᵖ) (i : U V) :
↑() = Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor U V i x

The subpresheaf as a presheaf.

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.ι_app {C : Type u} {F : } (U : Cᵒᵖ) (x : ) :
Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types () F () U x = x

The inclusion of a subpresheaf to the original presheaf.

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe_app_coe {C : Type u} {F : } (h : G G') (U : Cᵒᵖ) (x : ) :
↑() = x

The inclusion of a subpresheaf to a larger subpresheaf

Instances For
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.lift_app_coe {C : Type u} {F : } {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 ) (U : Cᵒᵖ) (x : F'.obj U) :
↑(Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' () () U x) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' F f U x
def CategoryTheory.GrothendieckTopology.Subpresheaf.lift {C : Type u} {F : } {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 ) :

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

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.lift_ι_assoc {C : Type u} {F : } {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 ) {Z : } (h : F Z) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.lift_ι {C : Type u} {F : } {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 ) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.sieveOfSection_apply {C : Type u} {F : } {U : Cᵒᵖ} (s : F.obj U) (V : C) (f : V U.unop) :
= (Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor (Opposite.op U.unop) () f.op s )

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

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

Instances For
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.nat_trans_naturality {C : Type u} {F : } {F' : } {U : Cᵒᵖ} {V : Cᵒᵖ} (i : U V) (x : F'.obj U) :
↑(Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' () 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' () 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
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.isSheaf_iff {C : Type u} {F : } (h : ) :
∀ (U : Cᵒᵖ) (s : F.obj U),
noncomputable def CategoryTheory.GrothendieckTopology.Subpresheaf.sheafifyLift {C : Type u} {F : } {F' : } (h : ) :

The lift of a presheaf morphism onto the sheafification subpresheaf.

Instances For
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.to_sheafify_lift_unique {C : Type u} {F : } {F' : } (h : ) (e : ) :
l₁ = l₂
@[simp]
theorem CategoryTheory.GrothendieckTopology.imagePresheaf_obj {C : Type u} {F : } {F' : } (f : F' F) (U : Cᵒᵖ) :
def CategoryTheory.GrothendieckTopology.imagePresheaf {C : Type u} {F : } {F' : } (f : F' F) :

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

Instances For
@[simp]
@[simp]
theorem CategoryTheory.GrothendieckTopology.toImagePresheaf_app_coe {C : Type u} {F : } {F' : } (f : F' F) (U : Cᵒᵖ) (x : F'.obj U) :
↑(Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' () () U x) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' F f U x
def CategoryTheory.GrothendieckTopology.toImagePresheaf {C : Type u} {F : } {F' : } (f : F' F) :

A morphism factors through the image presheaf.

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.toImagePresheafSheafify_app_coe {C : Type u} {F : } {F' : } (f : F' F) (X : Cᵒᵖ) :
∀ (a : F'.obj X), ↑(Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' () () X a) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types F' F f X a

A morphism factors through the sheafification of the image presheaf.

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.toImagePresheaf_ι_assoc {C : Type u} {F : } {F' : } (f : F' F) {Z : } (h : F Z) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.toImagePresheaf_ι {C : Type u} {F : } {F' : } (f : F' F) :
theorem CategoryTheory.GrothendieckTopology.imagePresheaf_comp_le {C : Type u} {F : } {F' : } {F'' : } (f₁ : F F') (f₂ : F' F'') :
instance CategoryTheory.GrothendieckTopology.isIso_toImagePresheaf {C : Type u} {F : } {F' : } (f : F F') [hf : ] :
@[simp]
theorem CategoryTheory.GrothendieckTopology.imageSheaf_val {C : Type u} {F : } {F' : } (f : F F') :
def CategoryTheory.GrothendieckTopology.imageSheaf {C : Type u} {F : } {F' : } (f : F F') :

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

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.toImageSheaf_val {C : Type u} {F : } {F' : } (f : F F') :
def CategoryTheory.GrothendieckTopology.toImageSheaf {C : Type u} {F : } {F' : } (f : F F') :

A morphism factors through the image sheaf.

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.imageSheafι_val {C : Type u} {F : } {F' : } (f : F F') :
def CategoryTheory.GrothendieckTopology.imageSheafι {C : Type u} {F : } {F' : } (f : F F') :

The inclusion of the image sheaf to the target.

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.toImageSheaf_ι_assoc {C : Type u} {F : } {F' : } (f : F F') {Z : } (h : F' Z) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.toImageSheaf_ι {C : Type u} {F : } {F' : } (f : F F') :

The mono factorization given by image_sheaf for a morphism.

Instances For
noncomputable def CategoryTheory.GrothendieckTopology.imageFactorization {C : Type u} {F : } {F' : } (f : F F') :

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

Instances For