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), 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 (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)
    source
    @[deprecated CategoryTheory.Subfunctor.ofSection (since := "2025-12-11")]
    def CategoryTheory.Subfunctor.Subpresheaf.ofSection {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ} (x : F.obj X) :
    Subfunctor F

    Alias of CategoryTheory.Subfunctor.ofSection.

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

    Equations
    Instances For
      source
      @[deprecated CategoryTheory.Subfunctor.mem_ofSection_obj (since := "2025-12-11")]
      theorem CategoryTheory.Subfunctor.Subpresheaf.mem_ofSection_obj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ} (x : F.obj X) :
      x ∈ (Subfunctor.ofSection x).obj X

      Alias of CategoryTheory.Subfunctor.mem_ofSection_obj.

      source
      @[deprecated CategoryTheory.Subfunctor.ofSection_le_iff (since := "2025-12-11")]
      theorem CategoryTheory.Subfunctor.Subpresheaf.ofSection_le_iff {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ} (x : F.obj X) (G : Subfunctor F) :
      Subfunctor.ofSection x ≤ G ↔ x ∈ G.obj X

      Alias of CategoryTheory.Subfunctor.ofSection_le_iff.

      source
      @[deprecated CategoryTheory.Subfunctor.ofSection_image (since := "2025-12-11")]
      theorem CategoryTheory.Subfunctor.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') :
      (Subfunctor.ofSection x).image f = Subfunctor.ofSection (f.app X x)

      Alias of CategoryTheory.Subfunctor.ofSection_image.

      source
      @[deprecated CategoryTheory.Subfunctor.ofSection_eq_range (since := "2025-12-11")]
      theorem CategoryTheory.Subfunctor.Subpresheaf.ofSection_eq_range {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type v)} {X : Cᵒᵖ} (x : F.obj X) :
      Subfunctor.ofSection x = Subfunctor.range (yonedaEquiv.symm x)

      Alias of CategoryTheory.Subfunctor.ofSection_eq_range.

      source
      @[deprecated CategoryTheory.Subfunctor.range_eq_ofSection (since := "2025-12-11")]
      theorem CategoryTheory.Subfunctor.Subpresheaf.range_eq_ofSection {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type v)} {X : C} (f : yoneda.obj X ⟶ F) :
      Subfunctor.range f = Subfunctor.ofSection (yonedaEquiv f)

      Alias of CategoryTheory.Subfunctor.range_eq_ofSection.

      source
      @[deprecated CategoryTheory.Subfunctor.ofSection_eq_range' (since := "2025-12-11")]
      theorem CategoryTheory.Subfunctor.Subpresheaf.ofSection_eq_range' {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type (max v w))} {X : Cᵒᵖ} (x : F.obj X) :
      Subfunctor.ofSection x = Subfunctor.range (uliftYonedaEquiv.symm x)

      Alias of CategoryTheory.Subfunctor.ofSection_eq_range'.

      source
      @[deprecated CategoryTheory.Subfunctor.range_eq_ofSection' (since := "2025-12-11")]
      theorem CategoryTheory.Subfunctor.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) :
      Subfunctor.range f = Subfunctor.ofSection (uliftYonedaEquiv f)

      Alias of CategoryTheory.Subfunctor.range_eq_ofSection'.