Chosen Coends

This file defines a typeclass ChosenCoends which contains the data of a chosen coend in C for each functor Jᵒᵖ ⥤ J ⥤ C.

class CategoryTheory.Limits.ChosenCoendsOfShape (J : Type u_1) [Category.{v_1, u_1} J] (C : Type u_2) [Category.{v_2, u_2} C] : Type (max (max (max u_1 u_2) v_1) v_2)

The data of chosen coends of shape J in C.

• cowedge (F : Functor Jᵒᵖ (Functor J C)) : Cowedge F

  The chosen cowedge for each functor Jᵒᵖ ⥤ J ⥤ C.

• isCoend (F : Functor Jᵒᵖ (Functor J C)) : IsColimit (cowedge F)

  The chosen cowedge is colimiting.

@[reducible, inline]

abbrev CategoryTheory.Limits.ChosenCoends (C : Type u_1) [Category.{v_1, u_1} C] : Type (max (max (max (max (max (max (u + 1) (v + 1)) u) u_1) v_1) u) v)

The data of chosen coends in C.

Equations

• CategoryTheory.Limits.ChosenCoends.{?u.16, ?u.15, ?u.14, ?u.13} C = ({J : Type ?u.15} → [inst : CategoryTheory.Category.{?u.16, ?u.15} J] → CategoryTheory.Limits.ChosenCoendsOfShape J C)

def CategoryTheory.Limits.chosenCoend {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] (F : Functor Jᵒᵖ (Functor J C)) [ChosenCoendsOfShape J C] : C

The chosen coend of a functor Jᵒᵖ ⥤ J ⥤ C.

Equations

• CategoryTheory.Limits.chosenCoend F = (CategoryTheory.Limits.ChosenCoendsOfShape.cowedge F).pt

def CategoryTheory.Limits.chosenCoend.ι {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] (F : Functor Jᵒᵖ (Functor J C)) [ChosenCoendsOfShape J C] (j : J) : (F.obj (Opposite.op j)).obj j ⟶ chosenCoend F

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

Equations

• CategoryTheory.Limits.chosenCoend.ι F j = CategoryTheory.Limits.Multicofork.π (CategoryTheory.Limits.ChosenCoendsOfShape.cowedge F) j

theorem CategoryTheory.Limits.chosenCoend.condition {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] (F : Functor Jᵒᵖ (Functor J C)) [ChosenCoendsOfShape J C] {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.chosenCoend.condition_assoc {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] (F : Functor Jᵒᵖ (Functor J C)) [ChosenCoendsOfShape J C] {i j : J} (f : i ⟶ j) {Z : C} (h : chosenCoend 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.chosenCoend.hom_ext {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenCoendsOfShape J C] {X : C} {f g : chosenCoend F ⟶ X} (h : ∀ (j : J), CategoryStruct.comp (ι F j) f = CategoryStruct.comp (ι F j) g) : f = g

Morphisms out of the chosen coend are determined by their composites with chosenCoend.ι.

theorem CategoryTheory.Limits.chosenCoend.hom_ext_iff {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenCoendsOfShape J C] {X : C} {f g : chosenCoend F ⟶ X} : f = g ↔ ∀ (j : J), CategoryStruct.comp (ι F j) f = CategoryStruct.comp (ι F j) g

def CategoryTheory.Limits.chosenCoend.desc {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenCoendsOfShape J 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)) : chosenCoend F ⟶ X

Constructor for morphisms out of the chosen coend of a functor.

Equations

• CategoryTheory.Limits.chosenCoend.desc f hf = CategoryTheory.Limits.Cowedge.IsColimit.desc (CategoryTheory.Limits.ChosenCoendsOfShape.isCoend F) f hf

@[simp]

theorem CategoryTheory.Limits.chosenCoend.ι_desc {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenCoendsOfShape J 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 (ι F j) (desc f hf) = f j

@[simp]

theorem CategoryTheory.Limits.chosenCoend.ι_desc_assoc {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenCoendsOfShape J 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 (ι F j) (CategoryStruct.comp (desc f hf) h) = CategoryStruct.comp (f j) h

def CategoryTheory.Limits.chosenCoend.map {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenCoendsOfShape J C] {G : Functor Jᵒᵖ (Functor J C)} (f : F ⟶ G) : chosenCoend F ⟶ chosenCoend G

A natural transformation of bifunctors induces a map on chosen coends.

Equations

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

@[simp]

theorem CategoryTheory.Limits.chosenCoend.ι_map {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenCoendsOfShape J C] {G : Functor Jᵒᵖ (Functor J C)} (f : F ⟶ G) (j : J) : CategoryStruct.comp (ι F j) (map f) = CategoryStruct.comp ((f.app (Opposite.op j)).app j) (ι G j)

@[simp]

theorem CategoryTheory.Limits.chosenCoend.ι_map_assoc {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenCoendsOfShape J C] {G : Functor Jᵒᵖ (Functor J C)} (f : F ⟶ G) (j : J) {Z : C} (h : chosenCoend G ⟶ Z) : CategoryStruct.comp (ι F j) (CategoryStruct.comp (map f) h) = CategoryStruct.comp ((f.app (Opposite.op j)).app j) (CategoryStruct.comp (ι G j) h)

@[simp]

theorem CategoryTheory.Limits.chosenCoend.map_id {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenCoendsOfShape J C] : map (CategoryStruct.id F) = CategoryStruct.id (chosenCoend F)

@[simp]

theorem CategoryTheory.Limits.chosenCoend.map_comp {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenCoendsOfShape J C] {G H : Functor Jᵒᵖ (Functor J C)} (f : F ⟶ G) (g : G ⟶ H) : CategoryStruct.comp (map f) (map g) = map (CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.Limits.chosenCoend.map_comp_assoc {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenCoendsOfShape J C] {G H : Functor Jᵒᵖ (Functor J C)} (f : F ⟶ G) (g : G ⟶ H) {Z : C} (h : chosenCoend H ⟶ Z) : CategoryStruct.comp (map f) (CategoryStruct.comp (map g) h) = CategoryStruct.comp (map (CategoryStruct.comp f g)) h

def CategoryTheory.Limits.chosenCoendFunctor {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] [ChosenCoendsOfShape J C] : Functor (Functor Jᵒᵖ (Functor J C)) C

The chosen coend construction as a functor out of the bifunctor category.

Equations

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

@[simp]

theorem CategoryTheory.Limits.chosenCoendFunctor_obj {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] [ChosenCoendsOfShape J C] (F : Functor Jᵒᵖ (Functor J C)) : chosenCoendFunctor.obj F = chosenCoend F

@[simp]

theorem CategoryTheory.Limits.chosenCoendFunctor_map {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} J] [ChosenCoendsOfShape J C] {X✝ Y✝ : Functor Jᵒᵖ (Functor J C)} (f : X✝ ⟶ Y✝) : chosenCoendFunctor.map f = chosenCoend.map f