Documentation

Mathlib.CategoryTheory.Subfunctor.Image

The image of a subfunctor #

Given a morphism of type-valued functors p : F' ⟶ F, we define its range Subfunctor.range p. More generally, if G' : Subfunctor F', we define G'.image p : Subfunctor F as the image of G' by f, and if G : Subfunctor F, we define its preimage G.preimage f : Subfunctor F'.

source
def CategoryTheory.Subfunctor.range {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :
Subfunctor F

The range of a morphism of type-valued functors, as a subfunctor of the target.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.Subfunctor.range_obj {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) (U : C) :
    (range p).obj U = Set.range (p.app U)
    source
    theorem CategoryTheory.Subfunctor.range_id {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) :
    range (CategoryStruct.id F) = ⊤
    source
    @[simp]
    theorem CategoryTheory.Subfunctor.range_ι {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (G : Subfunctor F) :
    range G.ι = G
    source
    def CategoryTheory.Subfunctor.lift {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (f : F' ⟶ F) {G : Subfunctor F} (hf : range f ≤ G) :
    F' ⟶ G.toFunctor

    If the image of a morphism falls in a subfunctor, then the morphism factors through it.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Subfunctor.lift_app_coe {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (f : F' ⟶ F) {G : Subfunctor F} (hf : range f ≤ G) (U : C) (x : F'.obj U) :
      ↑((lift f hf).app U x) = f.app U x
      source
      @[simp]
      theorem CategoryTheory.Subfunctor.lift_ι {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (f : F' ⟶ F) {G : Subfunctor F} (hf : range f ≤ G) :
      CategoryStruct.comp (lift f hf) G.ι = f
      source
      @[simp]
      theorem CategoryTheory.Subfunctor.lift_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (f : F' ⟶ F) {G : Subfunctor F} (hf : range f ≤ G) {Z : Functor C (Type w)} (h : F ⟶ Z) :
      CategoryStruct.comp (lift f hf) (CategoryStruct.comp G.ι h) = CategoryStruct.comp f h
      source
      def CategoryTheory.Subfunctor.toRange {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :
      F' ⟶ (range p).toFunctor

      Given a morphism p : F' ⟶ F of type-valued functors, this is the morphism from F' to its range.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Subfunctor.toRange_ι {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :
        CategoryStruct.comp (toRange p) (range p).ι = p
        source
        @[simp]
        theorem CategoryTheory.Subfunctor.toRange_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) {Z : Functor C (Type w)} (h : F ⟶ Z) :
        CategoryStruct.comp (toRange p) (CategoryStruct.comp (range p).ι h) = CategoryStruct.comp p h
        source
        theorem CategoryTheory.Subfunctor.toRange_app_val {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) {i : C} (x : F'.obj i) :
        ↑((toRange p).app i x) = p.app i x
        source
        @[simp]
        theorem CategoryTheory.Subfunctor.range_toRange {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :
        range (toRange p) = ⊤
        source
        theorem CategoryTheory.Subfunctor.epi_iff_range_eq_top {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :
        Epi p ↔ range p = ⊤
        source
        theorem CategoryTheory.Subfunctor.range_eq_top {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) [Epi p] :
        range p = ⊤
        source
        instance CategoryTheory.Subfunctor.instEpiFunctorTypeToRange {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :
        Epi (toRange p)
        source
        instance CategoryTheory.Subfunctor.instIsIsoFunctorTypeToRangeOfMono {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) [Mono p] :
        IsIso (toRange p)
        source
        theorem CategoryTheory.Subfunctor.range_comp_le {C : Type u} [Category.{v, u} C] {F F' F'' : Functor C (Type w)} (f : F ⟶ F') (g : F' ⟶ F'') :
        range (CategoryStruct.comp f g) ≤ range g
        source
        def CategoryTheory.Subfunctor.image {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (f : F ⟶ F') :
        Subfunctor F'

        The image of a subfunctor by a morphism of type-valued functors.

        Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Subfunctor.image_obj {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (f : F ⟶ F') (i : C) :
          (G.image f).obj i = f.app i '' G.obj i
          source
          theorem CategoryTheory.Subfunctor.image_top {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (f : F ⟶ F') :
          ⊤.image f = range f
          source
          @[simp]
          theorem CategoryTheory.Subfunctor.image_iSup {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} {ι : Type u_1} (G : ι → Subfunctor F) (f : F ⟶ F') :
          (⨆ (i : ι), G i).image f = ⨆ (i : ι), (G i).image f
          source
          theorem CategoryTheory.Subfunctor.image_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor C (Type w)} (G : Subfunctor F) (f : F ⟶ F') (g : F' ⟶ F'') :
          G.image (CategoryStruct.comp f g) = (G.image f).image g
          source
          theorem CategoryTheory.Subfunctor.range_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor C (Type w)} (f : F ⟶ F') (g : F' ⟶ F'') :
          range (CategoryStruct.comp f g) = (range f).image g
          source
          def CategoryTheory.Subfunctor.preimage {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) :
          Subfunctor F'

          The preimage of a subfunctor by a morphism of type-valued functors.

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Subfunctor.preimage_obj {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) (n : C) :
            (G.preimage p).obj n = p.app n ⁻¹' G.obj n
            source
            @[simp]
            theorem CategoryTheory.Subfunctor.preimage_id {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (G : Subfunctor F) :
            G.preimage (CategoryStruct.id F) = G
            source
            theorem CategoryTheory.Subfunctor.preimage_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor C (Type w)} (G : Subfunctor F) (f : F'' ⟶ F') (g : F' ⟶ F) :
            G.preimage (CategoryStruct.comp f g) = (G.preimage g).preimage f
            source
            theorem CategoryTheory.Subfunctor.image_le_iff {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (f : F ⟶ F') (G' : Subfunctor F') :
            G.image f ≤ G' ↔ G ≤ G'.preimage f
            source
            def CategoryTheory.Subfunctor.fromPreimage {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) :
            (G.preimage p).toFunctor ⟶ G.toFunctor

            Given a morphism p : F' ⟶ F of type-valued functors and G : Subfunctor F, this is the morphism from the preimage of G by p to G.

            Equations
            Instances For
              source
              theorem CategoryTheory.Subfunctor.fromPreimage_ι {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) :
              CategoryStruct.comp (G.fromPreimage p) G.ι = CategoryStruct.comp (G.preimage p).ι p
              source
              theorem CategoryTheory.Subfunctor.fromPreimage_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) {Z : Functor C (Type w)} (h : F ⟶ Z) :
              CategoryStruct.comp (G.fromPreimage p) (CategoryStruct.comp G.ι h) = CategoryStruct.comp (G.preimage p).ι (CategoryStruct.comp p h)
              source
              theorem CategoryTheory.Subfunctor.preimage_eq_top_iff {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) :
              G.preimage p = ⊤ ↔ range p ≤ G
              source
              @[simp]
              theorem CategoryTheory.Subfunctor.preimage_image_of_epi {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) [hp : Epi p] :
              (G.preimage p).image p = G
              source
              @[deprecated CategoryTheory.Subfunctor.range (since := "2025-12-11")]
              def CategoryTheory.Subfunctor.Subpresheaf.range {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :
              Subfunctor F

              Alias of CategoryTheory.Subfunctor.range.

              The range of a morphism of type-valued functors, as a subfunctor of the target.

              Equations
              Instances For
                source
                @[deprecated CategoryTheory.Subfunctor.range_id (since := "2025-12-11")]
                theorem CategoryTheory.Subfunctor.Subpresheaf.range_id {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) :
                Subfunctor.range (CategoryStruct.id F) = ⊤

                Alias of CategoryTheory.Subfunctor.range_id.

                source
                @[deprecated CategoryTheory.Subfunctor.range_ι (since := "2025-12-11")]
                theorem CategoryTheory.Subfunctor.Subpresheaf.range_ι {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (G : Subfunctor F) :
                Subfunctor.range G.ι = G

                Alias of CategoryTheory.Subfunctor.range_ι.

                source
                @[deprecated CategoryTheory.Subfunctor.lift (since := "2025-12-11")]
                def CategoryTheory.Subfunctor.Subpresheaf.lift {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (f : F' ⟶ F) {G : Subfunctor F} (hf : Subfunctor.range f ≤ G) :
                F' ⟶ G.toFunctor

                Alias of CategoryTheory.Subfunctor.lift.

                If the image of a morphism falls in a subfunctor, then the morphism factors through it.

                Equations
                Instances For
                  source
                  @[deprecated CategoryTheory.Subfunctor.lift_ι (since := "2025-12-11")]
                  theorem CategoryTheory.Subfunctor.Subpresheaf.lift_ι {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (f : F' ⟶ F) {G : Subfunctor F} (hf : Subfunctor.range f ≤ G) :
                  CategoryStruct.comp (Subfunctor.lift f hf) G.ι = f

                  Alias of CategoryTheory.Subfunctor.lift_ι.

                  source
                  @[deprecated CategoryTheory.Subfunctor.toRange (since := "2025-12-11")]
                  def CategoryTheory.Subfunctor.Subpresheaf.toRange {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :
                  F' ⟶ (Subfunctor.range p).toFunctor

                  Alias of CategoryTheory.Subfunctor.toRange.

                  Given a morphism p : F' ⟶ F of type-valued functors, this is the morphism from F' to its range.

                  Equations
                  Instances For
                    source
                    @[deprecated CategoryTheory.Subfunctor.toRange_ι (since := "2025-12-11")]
                    theorem CategoryTheory.Subfunctor.Subpresheaf.toRange_ι {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :
                    CategoryStruct.comp (Subfunctor.toRange p) (Subfunctor.range p).ι = p

                    Alias of CategoryTheory.Subfunctor.toRange_ι.

                    source
                    @[deprecated CategoryTheory.Subfunctor.toRange_app_val (since := "2025-12-11")]
                    theorem CategoryTheory.Subfunctor.Subpresheaf.toRange_app_val {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) {i : C} (x : F'.obj i) :
                    ↑((Subfunctor.toRange p).app i x) = p.app i x

                    Alias of CategoryTheory.Subfunctor.toRange_app_val.

                    source
                    @[deprecated CategoryTheory.Subfunctor.range_toRange (since := "2025-12-11")]
                    theorem CategoryTheory.Subfunctor.Subpresheaf.range_toRange {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :
                    Subfunctor.range (Subfunctor.toRange p) = ⊤

                    Alias of CategoryTheory.Subfunctor.range_toRange.

                    source
                    @[deprecated CategoryTheory.Subfunctor.epi_iff_range_eq_top (since := "2025-12-11")]
                    theorem CategoryTheory.Subfunctor.Subpresheaf.epi_iff_range_eq_top {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :
                    Epi p ↔ Subfunctor.range p = ⊤

                    Alias of CategoryTheory.Subfunctor.epi_iff_range_eq_top.

                    source
                    @[deprecated CategoryTheory.Subfunctor.range_eq_top (since := "2025-12-11")]
                    theorem CategoryTheory.Subfunctor.Subpresheaf.range_eq_top {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) [Epi p] :
                    Subfunctor.range p = ⊤

                    Alias of CategoryTheory.Subfunctor.range_eq_top.

                    source
                    @[deprecated CategoryTheory.Subfunctor.range_comp_le (since := "2025-12-11")]
                    theorem CategoryTheory.Subfunctor.Subpresheaf.range_comp_le {C : Type u} [Category.{v, u} C] {F F' F'' : Functor C (Type w)} (f : F ⟶ F') (g : F' ⟶ F'') :
                    Subfunctor.range (CategoryStruct.comp f g) ≤ Subfunctor.range g

                    Alias of CategoryTheory.Subfunctor.range_comp_le.

                    source
                    @[deprecated CategoryTheory.Subfunctor.image (since := "2025-12-11")]
                    def CategoryTheory.Subfunctor.Subpresheaf.image {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (f : F ⟶ F') :
                    Subfunctor F'

                    Alias of CategoryTheory.Subfunctor.image.

                    The image of a subfunctor by a morphism of type-valued functors.

                    Equations
                    Instances For
                      source
                      @[deprecated CategoryTheory.Subfunctor.image_top (since := "2025-12-11")]
                      theorem CategoryTheory.Subfunctor.Subpresheaf.image_top {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (f : F ⟶ F') :
                      ⊤.image f = Subfunctor.range f

                      Alias of CategoryTheory.Subfunctor.image_top.

                      source
                      @[deprecated CategoryTheory.Subfunctor.image_iSup (since := "2025-12-11")]
                      theorem CategoryTheory.Subfunctor.Subpresheaf.image_iSup {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} {ι : Type u_1} (G : ι → Subfunctor F) (f : F ⟶ F') :
                      (⨆ (i : ι), G i).image f = ⨆ (i : ι), (G i).image f

                      Alias of CategoryTheory.Subfunctor.image_iSup.

                      source
                      @[deprecated CategoryTheory.Subfunctor.image_comp (since := "2025-12-11")]
                      theorem CategoryTheory.Subfunctor.Subpresheaf.image_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor C (Type w)} (G : Subfunctor F) (f : F ⟶ F') (g : F' ⟶ F'') :
                      G.image (CategoryStruct.comp f g) = (G.image f).image g

                      Alias of CategoryTheory.Subfunctor.image_comp.

                      source
                      @[deprecated CategoryTheory.Subfunctor.range_comp (since := "2025-12-11")]
                      theorem CategoryTheory.Subfunctor.Subpresheaf.range_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor C (Type w)} (f : F ⟶ F') (g : F' ⟶ F'') :
                      Subfunctor.range (CategoryStruct.comp f g) = (Subfunctor.range f).image g

                      Alias of CategoryTheory.Subfunctor.range_comp.

                      source
                      @[deprecated CategoryTheory.Subfunctor.preimage (since := "2025-12-11")]
                      def CategoryTheory.Subfunctor.Subpresheaf.preimage {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) :
                      Subfunctor F'

                      Alias of CategoryTheory.Subfunctor.preimage.

                      The preimage of a subfunctor by a morphism of type-valued functors.

                      Equations
                      Instances For
                        source
                        @[deprecated CategoryTheory.Subfunctor.preimage_id (since := "2025-12-11")]
                        theorem CategoryTheory.Subfunctor.Subpresheaf.preimage_id {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (G : Subfunctor F) :
                        G.preimage (CategoryStruct.id F) = G

                        Alias of CategoryTheory.Subfunctor.preimage_id.

                        source
                        @[deprecated CategoryTheory.Subfunctor.preimage_comp (since := "2025-12-11")]
                        theorem CategoryTheory.Subfunctor.Subpresheaf.preimage_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor C (Type w)} (G : Subfunctor F) (f : F'' ⟶ F') (g : F' ⟶ F) :
                        G.preimage (CategoryStruct.comp f g) = (G.preimage g).preimage f

                        Alias of CategoryTheory.Subfunctor.preimage_comp.

                        source
                        @[deprecated CategoryTheory.Subfunctor.image_le_iff (since := "2025-12-11")]
                        theorem CategoryTheory.Subfunctor.Subpresheaf.image_le_iff {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (f : F ⟶ F') (G' : Subfunctor F') :
                        G.image f ≤ G' ↔ G ≤ G'.preimage f

                        Alias of CategoryTheory.Subfunctor.image_le_iff.

                        source
                        @[deprecated CategoryTheory.Subfunctor.fromPreimage (since := "2025-12-11")]
                        def CategoryTheory.Subfunctor.Subpresheaf.fromPreimage {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) :
                        (G.preimage p).toFunctor ⟶ G.toFunctor

                        Alias of CategoryTheory.Subfunctor.fromPreimage.

                        Given a morphism p : F' ⟶ F of type-valued functors and G : Subfunctor F, this is the morphism from the preimage of G by p to G.

                        Equations
                        Instances For
                          source
                          @[deprecated CategoryTheory.Subfunctor.fromPreimage_ι (since := "2025-12-11")]
                          theorem CategoryTheory.Subfunctor.Subpresheaf.fromPreimage_ι {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) :
                          CategoryStruct.comp (G.fromPreimage p) G.ι = CategoryStruct.comp (G.preimage p).ι p

                          Alias of CategoryTheory.Subfunctor.fromPreimage_ι.

                          source
                          @[deprecated CategoryTheory.Subfunctor.preimage_eq_top_iff (since := "2025-12-11")]
                          theorem CategoryTheory.Subfunctor.Subpresheaf.preimage_eq_top_iff {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) :
                          G.preimage p = ⊤ ↔ Subfunctor.range p ≤ G

                          Alias of CategoryTheory.Subfunctor.preimage_eq_top_iff.

                          source
                          @[deprecated CategoryTheory.Subfunctor.preimage_image_of_epi (since := "2025-12-11")]
                          theorem CategoryTheory.Subfunctor.Subpresheaf.preimage_image_of_epi {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) [hp : Epi p] :
                          (G.preimage p).image p = G

                          Alias of CategoryTheory.Subfunctor.preimage_image_of_epi.