Sieves attached to subpresheaves

Given a subpresheaf G of a presheaf of types F : Cᵒᵖ ⥤ Type w and a section s : F.obj U, we define a sieve G.sieveOfSection s : Sieve (unop U) and the associated compatible family of elements with values in G.toFunctor.

def CategoryTheory.Subfunctor.sieveOfSection {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subfunctor F) {U : Cᵒᵖ} (s : F.obj U) : Sieve (Opposite.unop U)

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.

Equations

• G.sieveOfSection s = { arrows := fun (V : C) (f : V ⟶ Opposite.unop U) => (CategoryTheory.ConcreteCategory.hom (F.map f.op)) s ∈ G.obj (Opposite.op V), downward_closed := ⋯ }

@[simp]

theorem CategoryTheory.Subfunctor.sieveOfSection_apply {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subfunctor F) {U : Cᵒᵖ} (s : F.obj U) (V : C) (f : V ⟶ Opposite.unop U) : (G.sieveOfSection s).arrows f = ((ConcreteCategory.hom (F.map f.op)) s ∈ G.obj (Opposite.op V))

def CategoryTheory.Subfunctor.familyOfElementsOfSection {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subfunctor F) {U : Cᵒᵖ} (s : F.obj U) : Presieve.FamilyOfElements G.toFunctor (G.sieveOfSection 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

Equations

• G.familyOfElementsOfSection s i hi = ⟨(CategoryTheory.ConcreteCategory.hom (F.map i.op)) s, hi⟩

theorem CategoryTheory.Subfunctor.family_of_elements_compatible {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subfunctor F) {U : Cᵒᵖ} (s : F.obj U) : (G.familyOfElementsOfSection s).Compatible