Sheafification of subpresheafs for precoverages

Let K be a precoverage. In this file we define the K-sheafification of a subpresheaf. More generally, for a family of subsets 𝒮 of sections of a sheaf F, we construct the smallest subsheaf of F containing 𝒮.

Main declarations

• CategoryTheory.Precoverage.subsheafify: K-sheafification of family of sets 𝒮 in a presheaf F. This is only a sheaf if F itself is a sheaf.
• CategoryTheory.Precoverage.small_subsheafify_of_small: If all the sets in the family 𝒮 are small, then the K-sheafification is again small.

TODOs

• Relate Precoverage.subsheafify K with Subfunctor.sheafify for the Grothendieck topology Precoverage.toGrothendieck K.

inductive CategoryTheory.Precoverage.SubsheafClosure {C : Type u} [Category.{v, u} C] (K : Precoverage C) {F : Functor Cᵒᵖ (Type w)} (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))) (Z : C) : F.obj (Opposite.op Z) → Prop

Closure of a family of elements of a presheaf under restriction and gluing of sections over coverings in K.

• base {C : Type u} [Category.{v, u} C] {K : Precoverage C} {F : Functor Cᵒᵖ (Type w)} {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))} {Z : C} {a : F.obj (Opposite.op Z)} : a ∈ 𝒮 Z → K.SubsheafClosure 𝒮 Z a

  Element of the initial family.

• restrict {C : Type u} [Category.{v, u} C] {K : Precoverage C} {F : Functor Cᵒᵖ (Type w)} {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))} {Z W : C} (h : Z ⟶ W) {a : F.obj (Opposite.op W)} : K.SubsheafClosure 𝒮 W a → K.SubsheafClosure 𝒮 Z ((ConcreteCategory.hom (F.map h.op)) a)

  Restriction of an element in the closure along a morphism.

• amalgamate {C : Type u} [Category.{v, u} C] {K : Precoverage C} {F : Functor Cᵒᵖ (Type w)} {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))} {Z : C} {R : Presieve Z} (hR : R ∈ K.coverings Z) {y : Presieve.FamilyOfElements F R} (hy : y.Compatible) (hmem : ∀ ⦃W : C⦄ (r : W ⟶ Z) (hr : R r), K.SubsheafClosure 𝒮 W (y r hr)) {t : F.obj (Opposite.op Z)} (ht : y.IsAmalgamation t) : K.SubsheafClosure 𝒮 Z t

  Gluing of sections in the closure.

def CategoryTheory.Precoverage.subsheafify {C : Type u} [Category.{v, u} C] (K : Precoverage C) {F : Functor Cᵒᵖ (Type w)} (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))) : Subfunctor F

The K-sheafification of a family of sets 𝒮 in F: If F is a sheaf for K, this is the smallest subsheaf of F containing 𝒮.

Equations

• K.subsheafify 𝒮 = { obj := fun (U : Cᵒᵖ) => {x : F.obj U | K.SubsheafClosure 𝒮 (Opposite.unop U) x}, map := ⋯ }

@[simp]

theorem CategoryTheory.Precoverage.subsheafify_obj {C : Type u} [Category.{v, u} C] (K : Precoverage C) {F : Functor Cᵒᵖ (Type w)} (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))) (U : Cᵒᵖ) : (K.subsheafify 𝒮).obj U = {x : F.obj U | K.SubsheafClosure 𝒮 (Opposite.unop U) x}

theorem CategoryTheory.Precoverage.isSheafFor_subsheafify {C : Type u} [Category.{v, u} C] {K : Precoverage C} {F : Functor Cᵒᵖ (Type w)} (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))) {X : C} {R : Presieve X} (h : R ∈ K.coverings X) (h' : Presieve.IsSheafFor F R) : Presieve.IsSheafFor (K.subsheafify 𝒮).toFunctor R

If F is a sheaf for R and R ∈ K X, then the K-sheafification of 𝒮 is a sheaf for R.

theorem CategoryTheory.Precoverage.small_subsheafify_of_small {C : Type u} [Category.{v, u} C] {K : Precoverage C} {F : Functor Cᵒᵖ (Type w)} (hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R) (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))) (h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)) : FunctorToTypes.Small.{max u v, w, v, u} (K.subsheafify 𝒮).toFunctor

If 𝒮 Z is max u v-small for every Z, then the subsheaf generated by 𝒮 Z has max u v-small sections.