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

• https://ncatlab.org/nlab/show/end

def CategoryTheory.Limits.multicospanShapeEnd (J : Type u) [Category.{v, u} J] : MulticospanShape

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

@[simp]

theorem CategoryTheory.Limits.multicospanShapeEnd_snd (J : Type u) [Category.{v, u} J] (f : Arrow J) : (multicospanShapeEnd J).snd f = f.right

@[simp]

theorem CategoryTheory.Limits.multicospanShapeEnd_fst (J : Type u) [Category.{v, u} J] (f : Arrow J) : (multicospanShapeEnd J).fst f = f.left

@[simp]

theorem CategoryTheory.Limits.multicospanShapeEnd_R (J : Type u) [Category.{v, u} J] : (multicospanShapeEnd J).R = Arrow J

@[simp]

theorem CategoryTheory.Limits.multicospanShapeEnd_L (J : Type u) [Category.{v, u} J] : (multicospanShapeEnd J).L = J

def CategoryTheory.Limits.multispanShapeCoend (J : Type u) [Category.{v, u} J] : MultispanShape

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

@[simp]

theorem CategoryTheory.Limits.multispanShapeCoend_snd (J : Type u) [Category.{v, u} J] (f : Arrow J) : (multispanShapeCoend J).snd f = f.right

@[simp]

theorem CategoryTheory.Limits.multispanShapeCoend_R (J : Type u) [Category.{v, u} J] : (multispanShapeCoend J).R = J

@[simp]

theorem CategoryTheory.Limits.multispanShapeCoend_L (J : Type u) [Category.{v, u} J] : (multispanShapeCoend J).L = Arrow J

@[simp]

theorem CategoryTheory.Limits.multispanShapeCoend_fst (J : Type u) [Category.{v, u} J] (f : Arrow J) : (multispanShapeCoend J).fst f = f.left

def CategoryTheory.Limits.multicospanIndexEnd {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) : MulticospanIndex (multicospanShapeEnd J) C

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

@[simp]

theorem CategoryTheory.Limits.multicospanIndexEnd_snd {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (f : (multicospanShapeEnd J).R) : (multicospanIndexEnd F).snd f = (F.map f.hom.op).app f.right

@[simp]

theorem CategoryTheory.Limits.multicospanIndexEnd_right {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (f : (multicospanShapeEnd J).R) : (multicospanIndexEnd F).right f = (F.obj (Opposite.op f.left)).obj f.right

@[simp]

theorem CategoryTheory.Limits.multicospanIndexEnd_fst {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (f : (multicospanShapeEnd J).R) : (multicospanIndexEnd F).fst f = (F.obj (Opposite.op f.left)).map f.hom

@[simp]

theorem CategoryTheory.Limits.multicospanIndexEnd_left {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (j : (multicospanShapeEnd J).L) : (multicospanIndexEnd F).left j = (F.obj (Opposite.op j)).obj j

def CategoryTheory.Limits.multispanIndexCoend {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) : MultispanIndex (multispanShapeCoend J) C

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

@[simp]

theorem CategoryTheory.Limits.multispanIndexCoend_fst {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (f : (multispanShapeCoend J).L) : (multispanIndexCoend F).fst f = (F.map f.hom.op).app f.left

@[simp]

theorem CategoryTheory.Limits.multispanIndexCoend_right {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (j : (multispanShapeCoend J).R) : (multispanIndexCoend F).right j = (F.obj (Opposite.op j)).obj j

@[simp]

theorem CategoryTheory.Limits.multispanIndexCoend_left {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (f : (multispanShapeCoend J).L) : (multispanIndexCoend F).left f = (F.obj (Opposite.op f.right)).obj f.left

@[simp]

theorem CategoryTheory.Limits.multispanIndexCoend_snd {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (f : (multispanShapeCoend J).L) : (multispanIndexCoend F).snd f = (F.obj (Opposite.op f.right)).map f.hom

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

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 cat_disch) : W₁ ≅ W₂

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

@[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 cat_disch) : (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 cat_disch) : (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) (hπ : ∀ ⦃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)) : Wedge F

Constructor for wedges.

@[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) (hπ : ∀ ⦃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 π hπ).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) (hπ : ∀ ⦃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 π hπ) j = π j

theorem CategoryTheory.Limits.Wedge.condition {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} (c : Wedge F) {i j : J} (f : i ⟶ j) : CategoryStruct.comp (Multifork.ι c i) ((F.obj (Opposite.op i)).map f) = CategoryStruct.comp (Multifork.ι c j) ((F.map f.op).app j)

theorem CategoryTheory.Limits.Wedge.condition_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} (c : Wedge F) {i j : J} (f : i ⟶ j) {Z : C} (h : (F.obj (Opposite.op i)).obj j ⟶ Z) : CategoryStruct.comp (Multifork.ι c i) (CategoryStruct.comp ((F.obj (Opposite.op i)).map f) h) = CategoryStruct.comp (Multifork.ι c j) (CategoryStruct.comp ((F.map f.op).app j) h)

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.

@[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) : CategoryStruct.comp (lift hc f hf) (Multifork.ι c j) = f 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) : CategoryStruct.comp (lift hc f hf) (CategoryStruct.comp (Multifork.ι c j) h) = CategoryStruct.comp (f j) h

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

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 cat_disch) : W₁ ≅ W₂

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

@[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 cat_disch) : (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 cat_disch) : (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) (hι : ∀ ⦃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)) : Cowedge F

Constructor for cowedges.

@[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) (hι : ∀ ⦃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 ι hι).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) (hι : ∀ ⦃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 ι hι) j = ι j

theorem CategoryTheory.Limits.Cowedge.condition {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} (c : Cowedge F) {i j : J} (f : i ⟶ j) : CategoryStruct.comp ((F.map f.op).app i) (Multicofork.π c i) = CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (Multicofork.π c j)

theorem CategoryTheory.Limits.Cowedge.condition_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} (c : Cowedge F) {i j : J} (f : i ⟶ j) {Z : C} (h : c.pt ⟶ Z) : CategoryStruct.comp ((F.map f.op).app i) (CategoryStruct.comp (Multicofork.π c i) h) = CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (CategoryStruct.comp (Multicofork.π c j) h)

theorem CategoryTheory.Limits.Cowedge.IsColimit.hom_ext {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 g : c.pt ⟶ X} (h : ∀ (j : (multispanShapeCoend J).R), CategoryStruct.comp (Multicofork.π c j) f = CategoryStruct.comp (Multicofork.π c j) g) : f = g

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.

@[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) : CategoryStruct.comp (Multicofork.π c j) (desc hc f hf) = f 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) : CategoryStruct.comp (Multicofork.π c j) (CategoryStruct.comp (desc hc f hf) h) = CategoryStruct.comp (f j) h

@[reducible, inline]

abbrev CategoryTheory.Limits.HasEnd {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) : Prop

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

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.

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.

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) : CategoryStruct.comp (π F i) ((F.obj (Opposite.op i)).map f) = CategoryStruct.comp (π F j) ((F.map f.op).app 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) : CategoryStruct.comp (π F i) (CategoryStruct.comp ((F.obj (Opposite.op i)).map f) h) = CategoryStruct.comp (π F j) (CategoryStruct.comp ((F.map f.op).app j) h)

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.

@[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) : CategoryStruct.comp (lift f hf) (CategoryStruct.comp (π F j) h) = CategoryStruct.comp (f j) h

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') : end_ F ⟶ end_ F'

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

@[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) : CategoryStruct.comp (map f) (π F' j) = CategoryStruct.comp (π F j) ((f.app (Opposite.op j)).app 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) : CategoryStruct.comp (map f) (CategoryStruct.comp (π F' j) h) = CategoryStruct.comp (π F j) (CategoryStruct.comp ((f.app (Opposite.op j)).app j) h)

@[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'') : CategoryStruct.comp (map f) (map g) = map (CategoryStruct.comp f g)

@[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) : CategoryStruct.comp (map f) (CategoryStruct.comp (map g) h) = CategoryStruct.comp (map (CategoryStruct.comp f g)) h

@[simp]

theorem CategoryTheory.Limits.end_.map_id {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasEnd F] : map (CategoryStruct.id F) = CategoryStruct.id (end_ F)

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] : Functor (Functor Jᵒᵖ (Functor J C)) C

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

@[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✝) : (endFunctor J C).map f = end_.map f

@[reducible, inline]

abbrev CategoryTheory.Limits.HasCoend {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) : Prop

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

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.

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) : (F.obj (Opposite.op j)).obj j ⟶ coend F

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

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) : CategoryStruct.comp ((F.map f.op).app i) (ι F i) = CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (ι F j)

theorem CategoryTheory.Limits.coend.condition_assoc {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) {Z : C} (h : coend F ⟶ Z) : CategoryStruct.comp ((F.map f.op).app i) (CategoryStruct.comp (ι F i) h) = CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (CategoryStruct.comp (ι F j) h)

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)) : coend F ⟶ X

Constructor for morphisms to the coend of a functor.

@[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) : CategoryStruct.comp (ι F j) (CategoryStruct.comp (desc f hf) h) = CategoryStruct.comp (f j) h

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') : coend F ⟶ coend F'

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

@[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) : CategoryStruct.comp (ι F j) (map f) = CategoryStruct.comp ((f.app (Opposite.op j)).app j) (ι F' 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) : CategoryStruct.comp (ι F j) (CategoryStruct.comp (map f) h) = CategoryStruct.comp ((f.app (Opposite.op j)).app j) (CategoryStruct.comp (ι F' j) h)

@[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'') : CategoryStruct.comp (map f) (map g) = map (CategoryStruct.comp f g)

@[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) : CategoryStruct.comp (map f) (CategoryStruct.comp (map g) h) = CategoryStruct.comp (map (CategoryStruct.comp f g)) h

@[simp]

theorem CategoryTheory.Limits.coend.map_id {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} [HasCoend F] : map (CategoryStruct.id F) = CategoryStruct.id (coend F)

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] : Functor (Functor Jᵒᵖ (Functor J C)) C

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

@[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✝) : (coendFunctor J C).map f = coend.map f

@[simp]

theorem CategoryTheory.Limits.coendFunctor_obj (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)) : (coendFunctor J C).obj F = coend F