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.

source

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) => F.map f.op s ∈ G.obj (Opposite.op V), downward_closed := ⋯ }

Instances For

source

@[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 = (F.map f.op s ∈ G.obj (Opposite.op V))

source

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 = ⟨F.map i.op s, hi⟩

Instances For

source

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

source

@[deprecated CategoryTheory.Subfunctor.sieveOfSection (since := "2025-12-11")]

def CategoryTheory.Subfunctor.Subpresheaf.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)

Alias of CategoryTheory.Subfunctor.sieveOfSection.

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