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
🔸 coverage
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
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      @[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
      📐 coverage
      @[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
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      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
      🔸 coverage
      @[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
          📐 coverage
          @[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
          📐 coverage
          @[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
          📐 coverage
          @[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
          📐 coverage
          @[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
          📐 coverage
          @[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
          📐 coverage
          @[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
          📐 coverage
          @[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'.