Documentation

Mathlib.CategoryTheory.Limits.Shapes.End

Ends and coends #

In this file, given a functor F : Jᵒᵖ ⥤ J ⥤ C, we define its end end_ F, which is a suitable multiequalizer of the objects (F.obj (op j)).obj j for all j : J. For this shape of limits, cones are named wedges: the corresponding type is Wedge F.

We also introduce coend F as multicoequalizers of (F.obj (op j)).obj j for all j : J. In this cases, cocones are named cowedges.

References #

The shape of multiequalizer diagrams involved in the definition of ends.

Equations
Instances For

    The shape of multicoequalizer diagrams involved in the definition of coends.

    Equations
    Instances For

      Given F : Jᵒᵖ ⥤ J ⥤ C, this is the multicospan index which shall be used to define the end of F.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Given F : Jᵒᵖ ⥤ J ⥤ C, this is the multispan used to define the coend of F.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[reducible, inline]
          abbrev CategoryTheory.Limits.Wedge {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) :
          Type (max (max (max u v) u') v')

          Given F : Jᵒᵖ ⥤ J ⥤ C, a wedge for F is a type of cones (specifically the type of multiforks for multicospanIndexEnd F): the point of universal of these wedges shall be the end of F.

          Equations
          Instances For
            def CategoryTheory.Limits.Wedge.ext {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {W₁ W₂ : Wedge F} (e : W₁.pt W₂.pt) (he : ∀ (j : J), Multifork.ι W₁ j = CategoryStruct.comp e.hom (Multifork.ι W₂ j) := by aesop_cat) :
            W₁ W₂

            A variant of CategoryTheory.Limits.Cones.ext specialized to produce isomorphisms of wedges.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.Limits.Wedge.ext_hom_hom {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {W₁ W₂ : Wedge F} (e : W₁.pt W₂.pt) (he : ∀ (j : J), Multifork.ι W₁ j = CategoryStruct.comp e.hom (Multifork.ι W₂ j) := by aesop_cat) :
              (ext e he).hom.hom = e.hom
              @[simp]
              theorem CategoryTheory.Limits.Wedge.ext_inv_hom {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {W₁ W₂ : Wedge F} (e : W₁.pt W₂.pt) (he : ∀ (j : J), Multifork.ι W₁ j = CategoryStruct.comp e.hom (Multifork.ι W₂ j) := by aesop_cat) :
              (ext e he).inv.hom = e.inv
              @[reducible, inline]
              abbrev CategoryTheory.Limits.Wedge.mk {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} (pt : C) (π : (j : J) → pt (F.obj (Opposite.op j)).obj j) ( : ∀ ⦃i j : J⦄ (f : i j), CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) = CategoryStruct.comp (π j) ((F.map f.op).app j)) :

              Constructor for wedges.

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.Limits.Wedge.mk_pt {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} (pt : C) (π : (j : J) → pt (F.obj (Opposite.op j)).obj j) ( : ∀ ⦃i j : J⦄ (f : i j), CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) = CategoryStruct.comp (π j) ((F.map f.op).app j)) :
                (mk pt π ).pt = pt
                @[simp]
                theorem CategoryTheory.Limits.Wedge.mk_ι {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} (pt : C) (π : (j : J) → pt (F.obj (Opposite.op j)).obj j) ( : ∀ ⦃i j : J⦄ (f : i j), CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) = CategoryStruct.comp (π j) ((F.map f.op).app j)) (j : J) :
                Multifork.ι (mk pt π ) j = π j
                theorem CategoryTheory.Limits.Wedge.IsLimit.hom_ext {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {c : Wedge F} (hc : IsLimit c) {X : C} {f g : X c.pt} (h : ∀ (j : (multicospanShapeEnd J).L), CategoryStruct.comp f (Multifork.ι c j) = CategoryStruct.comp g (Multifork.ι c j)) :
                f = g
                def CategoryTheory.Limits.Wedge.IsLimit.lift {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {c : Wedge F} (hc : IsLimit c) {X : C} (f : (j : J) → X (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryStruct.comp (f j) ((F.map g.op).app j)) :
                X c.pt

                Construct a morphism to the end from its universal property.

                Equations
                Instances For
                  @[simp]
                  theorem CategoryTheory.Limits.Wedge.IsLimit.lift_ι {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {c : Wedge F} (hc : IsLimit c) {X : C} (f : (j : J) → X (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryStruct.comp (f j) ((F.map g.op).app j)) (j : J) :
                  @[simp]
                  theorem CategoryTheory.Limits.Wedge.IsLimit.lift_ι_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {c : Wedge F} (hc : IsLimit c) {X : C} (f : (j : J) → X (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryStruct.comp (f j) ((F.map g.op).app j)) (j : J) {Z : C} (h : (multicospanIndexEnd F).left j Z) :
                  @[reducible, inline]
                  abbrev CategoryTheory.Limits.Cowedge {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) :
                  Type (max (max (max u v) u') v')

                  Given F : Jᵒᵖ ⥤ J ⥤ C, a cowedge for F is a type of cocones (specifically the type of multicoforks for multispanIndexCoend F): the point of a universal cowedge is the coend of F.

                  Equations
                  Instances For
                    def CategoryTheory.Limits.Cowedge.ext {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {W₁ W₂ : Cowedge F} (e : W₁.pt W₂.pt) (he : ∀ (j : J), CategoryStruct.comp (Multicofork.π W₁ j) e.hom = Multicofork.π W₂ j := by aesop_cat) :
                    W₁ W₂

                    A variant of CategoryTheory.Limits.Cocones.ext specialized to produce isomorphisms of cowedges.

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Limits.Cowedge.ext_inv_hom {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {W₁ W₂ : Cowedge F} (e : W₁.pt W₂.pt) (he : ∀ (j : J), CategoryStruct.comp (Multicofork.π W₁ j) e.hom = Multicofork.π W₂ j := by aesop_cat) :
                      (ext e he).inv.hom = e.inv
                      @[simp]
                      theorem CategoryTheory.Limits.Cowedge.ext_hom_hom {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {W₁ W₂ : Cowedge F} (e : W₁.pt W₂.pt) (he : ∀ (j : J), CategoryStruct.comp (Multicofork.π W₁ j) e.hom = Multicofork.π W₂ j := by aesop_cat) :
                      (ext e he).hom.hom = e.hom
                      @[reducible, inline]
                      abbrev CategoryTheory.Limits.Cowedge.mk {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} (pt : C) (ι : (j : J) → (F.obj (Opposite.op j)).obj j pt) ( : ∀ ⦃i j : J⦄ (f : i j), CategoryStruct.comp ((F.map f.op).app i) (ι i) = CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (ι j)) :

                      Constructor for cowedges.

                      Equations
                      Instances For
                        @[simp]
                        theorem CategoryTheory.Limits.Cowedge.mk_pt {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} (pt : C) (ι : (j : J) → (F.obj (Opposite.op j)).obj j pt) ( : ∀ ⦃i j : J⦄ (f : i j), CategoryStruct.comp ((F.map f.op).app i) (ι i) = CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (ι j)) :
                        (mk pt ι ).pt = pt
                        @[simp]
                        theorem CategoryTheory.Limits.Cowedge.mk_π {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} (pt : C) (ι : (j : J) → (F.obj (Opposite.op j)).obj j pt) ( : ∀ ⦃i j : J⦄ (f : i j), CategoryStruct.comp ((F.map f.op).app i) (ι i) = CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (ι j)) (j : J) :
                        Multicofork.π (mk pt ι ) j = ι j
                        def CategoryTheory.Limits.Cowedge.IsColimit.desc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {c : Cowedge F} (hc : IsColimit c) {X : C} (f : (j : J) → (F.obj (Opposite.op j)).obj j X) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp ((F.map g.op).app i) (f i) = CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)) :
                        c.pt X

                        Construct a morphism from the coend using its universal property.

                        Equations
                        Instances For
                          @[simp]
                          theorem CategoryTheory.Limits.Cowedge.IsColimit.π_desc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {c : Cowedge F} (hc : IsColimit c) {X : C} (f : (j : J) → (F.obj (Opposite.op j)).obj j X) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp ((F.map g.op).app i) (f i) = CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)) (j : J) :
                          @[simp]
                          theorem CategoryTheory.Limits.Cowedge.IsColimit.π_desc_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} {c : Cowedge F} (hc : IsColimit c) {X : C} (f : (j : J) → (F.obj (Opposite.op j)).obj j X) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp ((F.map g.op).app i) (f i) = CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)) (j : J) {Z : C} (h : X Z) :
                          @[reducible, inline]

                          Given F : Jᵒᵖ ⥤ J ⥤ C, this property asserts the existence of the end of F.

                          Equations
                          Instances For
                            noncomputable def CategoryTheory.Limits.end_ {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) [HasEnd F] :
                            C

                            The end of a functor F : Jᵒᵖ ⥤ J ⥤ C.

                            Equations
                            Instances For
                              noncomputable def CategoryTheory.Limits.end_.π {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) [HasEnd F] (j : J) :
                              end_ F (F.obj (Opposite.op j)).obj j

                              Given F : Jᵒᵖ ⥤ J ⥤ C, this is the projection end_ F ⟶ (F.obj (op j)).obj j for any j : J.

                              Equations
                              Instances For
                                theorem CategoryTheory.Limits.end_.condition {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) [HasEnd F] {i j : J} (f : i j) :
                                theorem CategoryTheory.Limits.end_.condition_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) [HasEnd F] {i j : J} (f : i j) {Z : C} (h : (F.obj (Opposite.op i)).obj j Z) :
                                theorem CategoryTheory.Limits.end_.hom_ext {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] {X : C} {f g : X end_ F} (h : ∀ (j : J), CategoryStruct.comp f (π F j) = CategoryStruct.comp g (π F j)) :
                                f = g
                                theorem CategoryTheory.Limits.end_.hom_ext_iff {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] {X : C} {f g : X end_ F} :
                                f = g ∀ (j : J), CategoryStruct.comp f (π F j) = CategoryStruct.comp g (π F j)
                                @[deprecated CategoryTheory.Limits.end_.hom_ext (since := "2025-06-06")]
                                theorem CategoryTheory.Limits.hom_ext {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] {X : C} {f g : X end_ F} (h : ∀ (j : J), CategoryStruct.comp f (end_.π F j) = CategoryStruct.comp g (end_.π F j)) :
                                f = g

                                Alias of CategoryTheory.Limits.end_.hom_ext.

                                noncomputable def CategoryTheory.Limits.end_.lift {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] {X : C} (f : (j : J) → X (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryStruct.comp (f j) ((F.map g.op).app j)) :
                                X end_ F

                                Constructor for morphisms to the end of a functor.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.Limits.end_.lift_π {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] {X : C} (f : (j : J) → X (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryStruct.comp (f j) ((F.map g.op).app j)) (j : J) :
                                  CategoryStruct.comp (lift f hf) (π F j) = f j
                                  @[simp]
                                  theorem CategoryTheory.Limits.end_.lift_π_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] {X : C} (f : (j : J) → X (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryStruct.comp (f j) ((F.map g.op).app j)) (j : J) {Z : C} (h : (F.obj (Opposite.op j)).obj j Z) :
                                  noncomputable def CategoryTheory.Limits.end_.map {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] {F' : Functor Jᵒᵖ (Functor J C)} [HasEnd F'] (f : F F') :

                                  A natural transformation of functors F ⟶ F' induces a map end_ F ⟶ end_ F'.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.Limits.end_.map_π {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] {F' : Functor Jᵒᵖ (Functor J C)} [HasEnd F'] (f : F F') (j : J) :
                                    @[simp]
                                    theorem CategoryTheory.Limits.end_.map_π_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] {F' : Functor Jᵒᵖ (Functor J C)} [HasEnd F'] (f : F F') (j : J) {Z : C} (h : (F'.obj (Opposite.op j)).obj j Z) :
                                    @[simp]
                                    theorem CategoryTheory.Limits.end_.map_comp {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] {F' : Functor Jᵒᵖ (Functor J C)} [HasEnd F'] (f : F F') {F'' : Functor Jᵒᵖ (Functor J C)} [HasEnd F''] (g : F' F'') :
                                    @[simp]
                                    theorem CategoryTheory.Limits.end_.map_comp_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] {F' : Functor Jᵒᵖ (Functor J C)} [HasEnd F'] (f : F F') {F'' : Functor Jᵒᵖ (Functor J C)} [HasEnd F''] (g : F' F'') {Z : C} (h : end_ F'' Z) :
                                    noncomputable def CategoryTheory.Limits.endFunctor (J : Type u) [Category.{v, u} J] (C : Type u') [Category.{v', u'} C] [∀ (F : Functor Jᵒᵖ (Functor J C)), HasEnd F] :

                                    If all bifunctors Jᵒᵖ ⥤ J ⥤ C have an end, then the construction F ↦ end_ F defines a functor (Jᵒᵖ ⥤ J ⥤ C) ⥤ C.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.Limits.endFunctor_obj (J : Type u) [Category.{v, u} J] (C : Type u') [Category.{v', u'} C] [∀ (F : Functor Jᵒᵖ (Functor J C)), HasEnd F] (F : Functor Jᵒᵖ (Functor J C)) :
                                      (endFunctor J C).obj F = end_ F
                                      @[simp]
                                      theorem CategoryTheory.Limits.endFunctor_map (J : Type u) [Category.{v, u} J] (C : Type u') [Category.{v', u'} C] [∀ (F : Functor Jᵒᵖ (Functor J C)), HasEnd F] {X✝ Y✝ : Functor Jᵒᵖ (Functor J C)} (f : X✝ Y✝) :
                                      @[reducible, inline]

                                      Given F : Jᵒᵖ ⥤ J ⥤ C, this property asserts the existence of the coend of F.

                                      Equations
                                      Instances For
                                        noncomputable def CategoryTheory.Limits.coend {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) [HasCoend F] :
                                        C

                                        The end of a functor F : Jᵒᵖ ⥤ J ⥤ C.

                                        Equations
                                        Instances For
                                          noncomputable def CategoryTheory.Limits.coend.ι {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) [HasCoend F] (j : J) :

                                          Given F : Jᵒᵖ ⥤ J ⥤ C, this is the inclusion (F.obj (op j)).obj j ⟶ coend F for any j : J.

                                          Equations
                                          Instances For
                                            theorem CategoryTheory.Limits.coend.condition {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) [HasCoend F] {i j : J} (f : i j) :
                                            theorem CategoryTheory.Limits.coend.hom_ext {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasCoend F] {X : C} {f g : coend F X} (h : ∀ (j : J), CategoryStruct.comp (ι F j) f = CategoryStruct.comp (ι F j) g) :
                                            f = g
                                            theorem CategoryTheory.Limits.coend.hom_ext_iff {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasCoend F] {X : C} {f g : coend F X} :
                                            f = g ∀ (j : J), CategoryStruct.comp (ι F j) f = CategoryStruct.comp (ι F j) g
                                            noncomputable def CategoryTheory.Limits.coend.desc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasCoend F] {X : C} (f : (j : J) → (F.obj (Opposite.op j)).obj j X) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp ((F.map g.op).app i) (f i) = CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)) :

                                            Constructor for morphisms to the coend of a functor.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem CategoryTheory.Limits.coend.ι_desc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasCoend F] {X : C} (f : (j : J) → (F.obj (Opposite.op j)).obj j X) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp ((F.map g.op).app i) (f i) = CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)) (j : J) :
                                              CategoryStruct.comp (ι F j) (desc f hf) = f j
                                              @[simp]
                                              theorem CategoryTheory.Limits.coend.ι_desc_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasCoend F] {X : C} (f : (j : J) → (F.obj (Opposite.op j)).obj j X) (hf : ∀ ⦃i j : J⦄ (g : i j), CategoryStruct.comp ((F.map g.op).app i) (f i) = CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)) (j : J) {Z : C} (h : X Z) :
                                              noncomputable def CategoryTheory.Limits.coend.map {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasCoend F] {F' : Functor Jᵒᵖ (Functor J C)} [HasCoend F'] (f : F F') :

                                              A natural transformation of functors F ⟶ F' induces a map coend F ⟶ coend F'.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem CategoryTheory.Limits.coend.ι_map {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasCoend F] {F' : Functor Jᵒᵖ (Functor J C)} [HasCoend F'] (f : F F') (j : J) :
                                                @[simp]
                                                theorem CategoryTheory.Limits.coend.ι_map_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasCoend F] {F' : Functor Jᵒᵖ (Functor J C)} [HasCoend F'] (f : F F') (j : J) {Z : C} (h : coend F' Z) :
                                                @[simp]
                                                theorem CategoryTheory.Limits.coend.map_comp {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasCoend F] {F' : Functor Jᵒᵖ (Functor J C)} [HasCoend F'] (f : F F') {F'' : Functor Jᵒᵖ (Functor J C)} [HasCoend F''] (g : F' F'') :
                                                @[simp]
                                                theorem CategoryTheory.Limits.coend.map_comp_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasCoend F] {F' : Functor Jᵒᵖ (Functor J C)} [HasCoend F'] (f : F F') {F'' : Functor Jᵒᵖ (Functor J C)} [HasCoend F''] (g : F' F'') {Z : C} (h : coend F'' Z) :
                                                noncomputable def CategoryTheory.Limits.coendFunctor (J : Type u) [Category.{v, u} J] (C : Type u') [Category.{v', u'} C] [∀ (F : Functor Jᵒᵖ (Functor J C)), HasCoend F] :

                                                If all bifunctors Jᵒᵖ ⥤ J ⥤ C have a coend, then the construction F ↦ coend F defines a functor (Jᵒᵖ ⥤ J ⥤ C) ⥤ C.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem CategoryTheory.Limits.coendFunctor_map (J : Type u) [Category.{v, u} J] (C : Type u') [Category.{v', u'} C] [∀ (F : Functor Jᵒᵖ (Functor J C)), HasCoend F] {X✝ Y✝ : Functor Jᵒᵖ (Functor J C)} (f : X✝ Y✝) :
                                                  @[simp]