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.

References

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

TODO

• define coends

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.multicospanIndexEnd_R {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) : (CategoryTheory.Limits.multicospanIndexEnd F).R = CategoryTheory.Arrow J

@[simp]

theorem CategoryTheory.Limits.multicospanIndexEnd_L {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) : (CategoryTheory.Limits.multicospanIndexEnd F).L = J

@[simp]

theorem CategoryTheory.Limits.multicospanIndexEnd_fstTo {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : CategoryTheory.Arrow J) : (CategoryTheory.Limits.multicospanIndexEnd F).fstTo f = f.left

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.multicospanIndexEnd_sndTo {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : CategoryTheory.Arrow J) : (CategoryTheory.Limits.multicospanIndexEnd F).sndTo f = f.right

@[simp]

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

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

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.

@[reducible, inline]

abbrev CategoryTheory.Limits.Wedge {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.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

• CategoryTheory.Limits.Wedge F = CategoryTheory.Limits.Multifork (CategoryTheory.Limits.multicospanIndexEnd F)

@[simp]

theorem CategoryTheory.Limits.Wedge.mk_pt {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (pt : C) (π : (j : J) → pt ⟶ (F.obj (Opposite.op j)).obj j) (hπ : ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) = CategoryTheory.CategoryStruct.comp (π j) ((F.map f.op).app j)) : (CategoryTheory.Limits.Wedge.mk pt π hπ).pt = pt

@[reducible, inline]

abbrev CategoryTheory.Limits.Wedge.mk {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (pt : C) (π : (j : J) → pt ⟶ (F.obj (Opposite.op j)).obj j) (hπ : ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) = CategoryTheory.CategoryStruct.comp (π j) ((F.map f.op).app j)) : CategoryTheory.Limits.Wedge F

Constructor for wedges.

Equations

• CategoryTheory.Limits.Wedge.mk pt π hπ = CategoryTheory.Limits.Multifork.ofι (CategoryTheory.Limits.multicospanIndexEnd F) pt π ⋯

@[simp]

theorem CategoryTheory.Limits.Wedge.mk_ι {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (pt : C) (π : (j : J) → pt ⟶ (F.obj (Opposite.op j)).obj j) (hπ : ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) = CategoryTheory.CategoryStruct.comp (π j) ((F.map f.op).app j)) (j : J) : CategoryTheory.Limits.Multifork.ι (CategoryTheory.Limits.Wedge.mk pt π hπ) j = π j

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

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

theorem CategoryTheory.Limits.Wedge.IsLimit.hom_ext {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F} (hc : CategoryTheory.Limits.IsLimit c) {X : C} {f : X ⟶ c.pt} {g : X ⟶ c.pt} (h : ∀ (j : (CategoryTheory.Limits.multicospanIndexEnd F).L), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Multifork.ι c j) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.Multifork.ι c j)) : f = g

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

Construct a morphism to the end from its universal property.

Equations

• CategoryTheory.Limits.Wedge.IsLimit.lift hc f hf = CategoryTheory.Limits.Multifork.IsLimit.lift hc f ⋯

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Wedge.IsLimit.lift_ι {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F} (hc : CategoryTheory.Limits.IsLimit c) {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Wedge.IsLimit.lift hc f hf) (CategoryTheory.Limits.Multifork.ι c j) = f j

@[reducible, inline]

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

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

Equations

• CategoryTheory.Limits.HasEnd F = CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.Limits.multicospanIndexEnd F)

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

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

Equations

• CategoryTheory.Limits.end_ F = CategoryTheory.Limits.multiequalizer (CategoryTheory.Limits.multicospanIndexEnd F)

noncomputable def CategoryTheory.Limits.end_.π {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) [CategoryTheory.Limits.HasEnd F] (j : J) : CategoryTheory.Limits.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

• CategoryTheory.Limits.end_.π F j = CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.Limits.multicospanIndexEnd F) j

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

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

theorem CategoryTheory.Limits.hom_ext_iff {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [CategoryTheory.Limits.HasEnd F] {X : C} {f : X ⟶ CategoryTheory.Limits.end_ F} {g : X ⟶ CategoryTheory.Limits.end_ F} : f = g ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.end_.π F j) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.end_.π F j)

theorem CategoryTheory.Limits.hom_ext {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [CategoryTheory.Limits.HasEnd F] {X : C} {f : X ⟶ CategoryTheory.Limits.end_ F} {g : X ⟶ CategoryTheory.Limits.end_ F} (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.end_.π F j) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.end_.π F j)) : f = g

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

Constructor for morphisms to the end of a functor.

Equations

• CategoryTheory.Limits.end_.lift f hf = CategoryTheory.Limits.Wedge.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.multicospanIndexEnd F).multicospan) f hf

@[simp]

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

@[simp]

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