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.

source
def CategoryTheory.Subpresheaf.ofSection {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ} (x : F.obj X) :
Subpresheaf F

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

Equations
Instances For
    source
    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}
    source
    theorem CategoryTheory.Subpresheaf.mem_ofSection_obj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ} (x : F.obj X) :
    x ∈ (ofSection x).obj X
    source
    @[simp]
    theorem CategoryTheory.Subpresheaf.ofSection_le_iff {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ} (x : F.obj X) (G : Subpresheaf F) :
    ofSection x ≤ G ↔ x ∈ G.obj X
    source
    @[simp]
    theorem CategoryTheory.Subpresheaf.ofSection_image {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ} (x : F.obj X) {F' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') :
    (ofSection x).image f = ofSection (f.app X x)
    source
    theorem CategoryTheory.Subpresheaf.ofSection_eq_range {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type v)} {X : Cᵒᵖ} (x : F.obj X) :
    ofSection x = range (yonedaEquiv.symm x)
    source
    theorem CategoryTheory.Subpresheaf.range_eq_ofSection {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type v)} {X : C} (f : yoneda.obj X ⟶ F) :
    range f = ofSection (yonedaEquiv f)
    source
    theorem CategoryTheory.Subpresheaf.ofSection_eq_range' {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type (max v w))} {X : Cᵒᵖ} (x : F.obj X) :
    ofSection x = range ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x)
    source
    theorem CategoryTheory.Subpresheaf.range_eq_ofSection' {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type (max v w))} {X : C} (f : (yoneda.obj X).comp uliftFunctor.{w, v} ⟶ F) :
    range f = ofSection ((yonedaCompUliftFunctorEquiv F X) f)