Chosen ends and coends

This file defines typeclasses ChosenCoendsOfShape and ChosenEndsOfShape which contain the data of a chosen coend and end in C for each functor Jᵒᵖ ⥤ J ⥤ C of a fixed shape J. It also provides ChosenCoends and ChosenEnds abbreviations for chosen coends and ends of all shapes.

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.4, ?u.3, ?u.2, ?u.1} C = ({J : Type ?u.3} → [inst : CategoryTheory.Category.{?u.4, ?u.3} 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_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

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

class CategoryTheory.Limits.ChosenEndsOfShape (J : Type u_3) [Category.{v_3, u_3} J] (C : Type u_4) [Category.{v_4, u_4} C] : Type (max (max (max u_3 u_4) v_3) v_4)

The data of chosen ends of shape J in C.

• wedge (F : Functor Jᵒᵖ (Functor J C)) : Wedge F

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

• isEnd (F : Functor Jᵒᵖ (Functor J C)) : IsLimit (wedge F)

  The chosen wedge is limiting.

@[reducible, inline]

abbrev CategoryTheory.Limits.ChosenEnds (C : Type u_3) [Category.{v_3, u_3} C] : Type (max (max (max (max (max (max (u + 1) (v + 1)) u) u_3) v_3) u) v)

The data of chosen ends in C.

Equations

• CategoryTheory.Limits.ChosenEnds.{?u.4, ?u.3, ?u.2, ?u.1} C = ({J : Type ?u.3} → [inst : CategoryTheory.Category.{?u.4, ?u.3} J] → CategoryTheory.Limits.ChosenEndsOfShape J C)

def CategoryTheory.Limits.chosenEnd {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] (F : Functor Jᵒᵖ (Functor J C)) [ChosenEndsOfShape J C] : C

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

Equations

• CategoryTheory.Limits.chosenEnd F = (CategoryTheory.Limits.ChosenEndsOfShape.wedge F).pt

def CategoryTheory.Limits.chosenEnd.π {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] (F : Functor Jᵒᵖ (Functor J C)) [ChosenEndsOfShape J C] (j : J) : chosenEnd F ⟶ (F.obj (Opposite.op j)).obj j

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

Equations

• CategoryTheory.Limits.chosenEnd.π F j = CategoryTheory.Limits.Multifork.ι (CategoryTheory.Limits.ChosenEndsOfShape.wedge F) j

theorem CategoryTheory.Limits.chosenEnd.condition {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] (F : Functor Jᵒᵖ (Functor J C)) [ChosenEndsOfShape J C] {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.chosenEnd.condition_assoc {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] (F : Functor Jᵒᵖ (Functor J C)) [ChosenEndsOfShape J C] {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.chosenEnd.hom_ext {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenEndsOfShape J C] {X : C} {f g : X ⟶ chosenEnd F} (h : ∀ (j : J), CategoryStruct.comp f (π F j) = CategoryStruct.comp g (π F j)) : f = g

Morphisms into the chosen end are determined by their composites with chosenEnd.π.

theorem CategoryTheory.Limits.chosenEnd.hom_ext_iff {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenEndsOfShape J C] {X : C} {f g : X ⟶ chosenEnd F} : f = g ↔ ∀ (j : J), CategoryStruct.comp f (π F j) = CategoryStruct.comp g (π F j)

def CategoryTheory.Limits.chosenEnd.lift {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenEndsOfShape J 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 ⟶ chosenEnd F

Constructor for morphisms into the chosen end of a functor.

Equations

• CategoryTheory.Limits.chosenEnd.lift f hf = CategoryTheory.Limits.Wedge.IsLimit.lift (CategoryTheory.Limits.ChosenEndsOfShape.isEnd F) f hf

@[simp]

theorem CategoryTheory.Limits.chosenEnd.lift_π {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenEndsOfShape J 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 f hf) (π F j) = f j

@[simp]

theorem CategoryTheory.Limits.chosenEnd.lift_π_assoc {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenEndsOfShape J 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 : (F.obj (Opposite.op j)).obj j ⟶ Z) : CategoryStruct.comp (lift f hf) (CategoryStruct.comp (π F j) h) = CategoryStruct.comp (f j) h

def CategoryTheory.Limits.chosenEnd.map {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenEndsOfShape J C] {G : Functor Jᵒᵖ (Functor J C)} (f : F ⟶ G) : chosenEnd F ⟶ chosenEnd G

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.chosenEnd.map_π {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenEndsOfShape J C] {G : Functor Jᵒᵖ (Functor J C)} (f : F ⟶ G) (j : J) : CategoryStruct.comp (map f) (π G j) = CategoryStruct.comp (π F j) ((f.app (Opposite.op j)).app j)

@[simp]

theorem CategoryTheory.Limits.chosenEnd.map_π_assoc {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenEndsOfShape J C] {G : Functor Jᵒᵖ (Functor J C)} (f : F ⟶ G) (j : J) {Z : C} (h : (G.obj (Opposite.op j)).obj j ⟶ Z) : CategoryStruct.comp (map f) (CategoryStruct.comp (π G j) h) = CategoryStruct.comp (π F j) (CategoryStruct.comp ((f.app (Opposite.op j)).app j) h)

@[simp]

theorem CategoryTheory.Limits.chosenEnd.map_id {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenEndsOfShape J C] : map (CategoryStruct.id F) = CategoryStruct.id (chosenEnd F)

@[simp]

theorem CategoryTheory.Limits.chosenEnd.map_comp {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenEndsOfShape 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.chosenEnd.map_comp_assoc {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] {F : Functor Jᵒᵖ (Functor J C)} [ChosenEndsOfShape J C] {G H : Functor Jᵒᵖ (Functor J C)} (f : F ⟶ G) (g : G ⟶ H) {Z : C} (h : chosenEnd H ⟶ Z) : CategoryStruct.comp (map f) (CategoryStruct.comp (map g) h) = CategoryStruct.comp (map (CategoryStruct.comp f g)) h

def CategoryTheory.Limits.chosenEndFunctor {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] [ChosenEndsOfShape J C] : Functor (Functor Jᵒᵖ (Functor J C)) C

The chosen end 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.chosenEndFunctor_obj {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] [ChosenEndsOfShape J C] (F : Functor Jᵒᵖ (Functor J C)) : chosenEndFunctor.obj F = chosenEnd F

@[simp]

theorem CategoryTheory.Limits.chosenEndFunctor_map {J : Type u_3} {C : Type u_4} [Category.{v_3, u_4} C] [Category.{v_4, u_3} J] [ChosenEndsOfShape J C] {X✝ Y✝ : Functor Jᵒᵖ (Functor J C)} (f : X✝ ⟶ Y✝) : chosenEndFunctor.map f = chosenEnd.map f