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.toPresheaf.

def CategoryTheory.Subpresheaf.sieveOfSection {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf 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) => F.map f.op s ∈ G.obj (Opposite.op V), downward_closed := ⋯ }

@[simp]

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

def CategoryTheory.Subpresheaf.familyOfElementsOfSection {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) {U : Cᵒᵖ} (s : F.obj U) : Presieve.FamilyOfElements G.toPresheaf (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 = ⟨F.map i.op s, hi⟩

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