Documentation

Mathlib.CategoryTheory.Subpresheaf.OfSection

The subpresheaf generated by a section #

Given a presheaf of types F : Cᵒᵖ ⥤ Type w and a section x : F.obj X, we define Subpresheaf.ofSection x : Subpresheaf F as the subpresheaf of F generated by x.

The subpresheaf of F : Cᵒᵖ ⥤ Type w that is generated by a section x : F.obj X.

Equations
Instances For
    theorem CategoryTheory.Subpresheaf.ofSection_obj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ} (x : F.obj X) (U : Cᵒᵖ) :
    (ofSection x).obj U = {u : F.obj U | ∃ (f : X U), F.map f x = u}
    @[simp]