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.

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

• CategoryTheory.Subfunctor.ofSection x = { obj := fun (U : Cᵒᵖ) => {u : F.obj U | ∃ (f : X ⟶ U), (CategoryTheory.ConcreteCategory.hom (F.map f)) x = u}, map := ⋯ }

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}

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

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

@[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)

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)

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)

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)

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)