Documentation

Mathlib.CategoryTheory.Subpresheaf.Sieves

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.

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

    Equations
    Instances For