Documentation

Mathlib.CategoryTheory.Subfunctor.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 Subfunctor.ofSection x : Subfunctor F as the subpresheaf of F generated by x.

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

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

Equations
Instances For
    source
    theorem CategoryTheory.Subfunctor.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), (ConcreteCategory.hom (F.map f)) x = u}
    source
    theorem CategoryTheory.Subfunctor.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.Subfunctor.ofSection_le_iff {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ} (x : F.obj X) (G : Subfunctor F) :
    ofSection x ≤ G ↔ x ∈ G.obj X
    source
    @[simp]
    theorem CategoryTheory.Subfunctor.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 ((ConcreteCategory.hom (f.app X)) x)
    source
    theorem CategoryTheory.Subfunctor.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.Subfunctor.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.Subfunctor.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 (uliftYonedaEquiv.symm x)
    source
    theorem CategoryTheory.Subfunctor.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 (uliftYonedaEquiv f)