Ends and coends in Type

This file constructs explicit ends and coends in Type and provides ChosenEnds and ChosenCoends instances using these constructions.

inductive CategoryTheory.Limits.Types.coendRel {J : Type u} [Category.{v, u} J] (F : Functor Jᵒᵖ (Functor J (Type (max w u)))) : (j : J) × (F.obj (Opposite.op j)).obj j → (j : J) × (F.obj (Opposite.op j)).obj j → Prop

The relation on the sigma type (W : J) × (F.obj (op W)).obj W used to construct explicit coends in Type. Two terms ⟨j, x⟩ and ⟨j', x'⟩ are related if and only if there is a morphism f : j ⟶ j' in J and an element y : (F.obj (op j')).obj j such that (F.map f.op).app j y = x and (F.obj _).map f y = x', see coendRel_iff below.

• mk {J : Type u} [Category.{v, u} J] {F : Functor Jᵒᵖ (Functor J (Type (max w u)))} {j j' : J} (f : j ⟶ j') (x : (F.obj (Opposite.op j')).obj j) : coendRel F ⟨j, (TypeCat.Hom.hom ((F.map f.op).app j)) x⟩ ⟨j', (TypeCat.Hom.hom ((F.obj (Opposite.op j')).map f)) x⟩

theorem CategoryTheory.Limits.Types.coendRel_iff {J : Type u} [Category.{v, u} J] (F : Functor Jᵒᵖ (Functor J (Type (max w u)))) (j j' : J) (x : (F.obj (Opposite.op j)).obj j) (x' : (F.obj (Opposite.op j')).obj j') : coendRel F ⟨j, x⟩ ⟨j', x'⟩ ↔ ∃ (f : j ⟶ j') (y : (F.obj (Opposite.op j')).obj j), (ConcreteCategory.hom ((F.map f.op).app j)) y = x ∧ (ConcreteCategory.hom ((F.obj (Opposite.op j')).map f)) y = x'

@[reducible, inline]

abbrev CategoryTheory.Limits.Types.coend {J : Type u} [Category.{v, u} J] (F : Functor Jᵒᵖ (Functor J (Type (max w u)))) : Type (max w u)

The coend of a bifunctor valued in Type, defined as a quotient.

Equations

• CategoryTheory.Limits.Types.coend F = Quot (CategoryTheory.Limits.Types.coendRel F)

def CategoryTheory.Limits.Types.coend.ι {J : Type u} [Category.{v, u} J] (F : Functor Jᵒᵖ (Functor J (Type (max w u)))) (j : J) : (F.obj (Opposite.op j)).obj j ⟶ coend F

Given F : Jᵒᵖ ⥤ J ⥤ Type*, this is the inclusion (F.obj (op j)).obj j ⟶ coend F for any j : J, which sends x to Quot.mk _ ⟨j, x⟩

Equations

• CategoryTheory.Limits.Types.coend.ι F j = TypeCat.ofHom fun (x : (F.obj (Opposite.op j)).obj j) => Quot.mk (CategoryTheory.Limits.Types.coendRel F) ⟨j, x⟩

theorem CategoryTheory.Limits.Types.coend.condition {J : Type u} [Category.{v, u} J] {F : Functor Jᵒᵖ (Functor J (Type (max w u)))} {j j' : J} (f : j ⟶ j') : CategoryStruct.comp ((F.map f.op).app j) (ι F j) = CategoryStruct.comp ((F.obj (Opposite.op j')).map f) (ι F j')

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

def CategoryTheory.Limits.Types.cowedge {J : Type u} [Category.{v, u} J] (F : Functor Jᵒᵖ (Functor J (Type (max w u)))) : Cowedge F

The cowedge corresponding to the explicit coend in Type

Equations

• CategoryTheory.Limits.Types.cowedge F = CategoryTheory.Limits.Cowedge.mk (CategoryTheory.Limits.Types.coend F) (CategoryTheory.Limits.Types.coend.ι F) ⋯

def CategoryTheory.Limits.Types.cowedgeIsColimit {J : Type u} [Category.{v, u} J] (F : Functor Jᵒᵖ (Functor J (Type (max w u)))) : IsColimit (cowedge F)

The cowedge corresponding to the explicit coend in Type is colimiting.

Equations

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

@[implicit_reducible]

instance CategoryTheory.Limits.instChosenCoendsType : ChosenCoends.{v, u, max u w, max (u + 1) (w + 1)} (Type (max w u))

A ChosenCoends instance on Type given by the explicit quotient construction above.

Equations

• CategoryTheory.Limits.instChosenCoendsType = { cowedge := CategoryTheory.Limits.Types.cowedge, isCoend := CategoryTheory.Limits.Types.cowedgeIsColimit }

theorem CategoryTheory.Limits.Types.chosenCoend_def {J : Type u} [Category.{v, u} J] {F : Functor Jᵒᵖ (Functor J (Type (max w u)))} : chosenCoend F = Quot (coendRel F)

theorem CategoryTheory.Limits.chosenCoend.ι_apply {J : Type u} [Category.{v, u} J] {F : Functor Jᵒᵖ (Functor J (Type (max w u)))} (j : J) (x : (F.obj (Opposite.op j)).obj j) : (ConcreteCategory.hom (ι F j)) x = Quot.mk (Types.coendRel F) ⟨j, x⟩

theorem CategoryTheory.Limits.chosenCoend.desc_apply {J : Type u} [Category.{v, u} J] {F : Functor Jᵒᵖ (Functor J (Type (max w u)))} {X : Type (max w u)} (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)) (x : chosenCoend F) : (ConcreteCategory.hom (desc f hf)) x = Quot.lift (fun (j : (j : J) × (F.obj (Opposite.op j)).obj j) => (ConcreteCategory.hom (f j.fst)) j.snd) ⋯ x

theorem CategoryTheory.Limits.chosenCoend.map_apply {J : Type u} [Category.{v, u} J] {F G : Functor Jᵒᵖ (Functor J (Type (max w u)))} (f : F ⟶ G) (x : chosenCoend F) : (ConcreteCategory.hom (map f)) x = Quot.lift (fun (x : (j : J) × (F.obj (Opposite.op j)).obj j) => Quot.mk (Types.coendRel G) ⟨x.fst, (ConcreteCategory.hom ((f.app (Opposite.op x.fst)).app x.fst)) x.snd⟩) ⋯ x

@[reducible, inline]

abbrev CategoryTheory.Limits.Types.end_ {J : Type u} [Category.{v, u} J] (F : Functor Jᵒᵖ (Functor J (Type (max w u)))) : Type (max w u)

The end of a bifunctor valued in Type, defined as the subtype of compatible families.

Equations

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

def CategoryTheory.Limits.Types.end_.π {J : Type u} [Category.{v, u} J] (F : Functor Jᵒᵖ (Functor J (Type (max w u)))) (j : J) : end_ F ⟶ (F.obj (Opposite.op j)).obj j

Given F : Jᵒᵖ ⥤ J ⥤ Type*, this is the projection end_ F ⟶ (F.obj (op j)).obj j for any j : J, which sends x to x.1 j.

Equations

• CategoryTheory.Limits.Types.end_.π F j = TypeCat.ofHom fun (x : CategoryTheory.Limits.Types.end_ F) => ↑x j

theorem CategoryTheory.Limits.Types.end_.condition {J : Type u} [Category.{v, u} J] {F : Functor Jᵒᵖ (Functor J (Type (max w u)))} {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.Types.end_.condition_assoc {J : Type u} [Category.{v, u} J] {F : Functor Jᵒᵖ (Functor J (Type (max w u)))} {i j : J} (f : i ⟶ j) {Z : Type (max w u)} (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)

def CategoryTheory.Limits.Types.wedge {J : Type u} [Category.{v, u} J] (F : Functor Jᵒᵖ (Functor J (Type (max w u)))) : Wedge F

The wedge corresponding to the explicit end in Type.

Equations

• CategoryTheory.Limits.Types.wedge F = CategoryTheory.Limits.Wedge.mk (CategoryTheory.Limits.Types.end_ F) (CategoryTheory.Limits.Types.end_.π F) ⋯

def CategoryTheory.Limits.Types.wedgeIsLimit {J : Type u} [Category.{v, u} J] (F : Functor Jᵒᵖ (Functor J (Type (max w u)))) : IsLimit (wedge F)

The wedge corresponding to the explicit end in Type is limiting.

Equations

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

@[implicit_reducible]

instance CategoryTheory.Limits.instChosenEndsType : ChosenEnds.{v, u, max u w, max (u + 1) (w + 1)} (Type (max w u))

A ChosenEnds instance on Type given by the explicit subtype construction above.

Equations

• CategoryTheory.Limits.instChosenEndsType = { wedge := CategoryTheory.Limits.Types.wedge, isEnd := CategoryTheory.Limits.Types.wedgeIsLimit }

theorem CategoryTheory.Limits.Types.chosenEnd_def {J : Type u} [Category.{v, u} J] {F : Functor Jᵒᵖ (Functor J (Type (max w u)))} : chosenEnd F = end_ F

theorem CategoryTheory.Limits.chosenEnd.π_apply {J : Type u} [Category.{v, u} J] {F : Functor Jᵒᵖ (Functor J (Type (max w u)))} (j : J) (x : Types.end_ F) : (ConcreteCategory.hom (π F j)) x = ↑x j

theorem CategoryTheory.Limits.chosenEnd.lift_apply {J : Type u} [Category.{v, u} J] {F : Functor Jᵒᵖ (Functor J (Type (max w u)))} {X : Type (max w u)} (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 : X) : (ConcreteCategory.hom (lift f hf)) x = ⟨fun (j : J) => (ConcreteCategory.hom (f j)) x, ⋯⟩

theorem CategoryTheory.Limits.chosenEnd.map_apply {J : Type u} [Category.{v, u} J] {F G : Functor Jᵒᵖ (Functor J (Type (max w u)))} (f : F ⟶ G) (x : Types.end_ F) : (ConcreteCategory.hom (map f)) x = ⟨fun (j : J) => (ConcreteCategory.hom ((f.app (Opposite.op j)).app j)) (↑x j), ⋯⟩