Composition of Profunctors

This file defines composition of profunctors. Given profunctors P : C ⥤ Dᵒᵖ ⥤ Type and Q : D ⥤ Eᵒᵖ ⥤ Type, the composite P.comp Q is the profunctor C ⥤ Eᵒᵖ ⥤ Type given on objects X : C and Y : E by the coend ∫ d, P X d × Q d Y, where d ranges over objects of D.

Main Definitions

(All in the namespace CategoryTheory.Profunctor)

• comp : Composition of profunctors.
• whiskerLeft : Left whiskering of a natural transformation of profunctors.
• whiskerRight : Right whiskering of a natural transformation of profunctors.
• leftUnitor : The left unitor isomorphism Profunctor.id.comp P ≅ P.
• rightUnitor : The right unitor isomorphism P.comp Profunctor.id ≅ P.
• associator : The associator isomorphism (P.comp Q).comp R ≅ P.comp (Q.comp R).

These satisfy the coherence laws for a bicategory, see the file Mathlib.CategoryTheory.Profunctor.Bicategory.

@[implicit_reducible]

def CategoryTheory.Profunctor.compDiagram {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) (X : C) (Y : E) : Functor Dᵒᵖ (Functor D (Type (max w w')))

The bifunctor whose coend defines the composite of two profunctors.

Equations

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

@[simp]

theorem CategoryTheory.Profunctor.compDiagram_obj_map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) (X : C) (Y : E) (U : Dᵒᵖ) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : ((P.compDiagram Q X Y).obj U).map f = TypeCat.ofHom (Prod.map id ⇑(ConcreteCategory.hom ((Q.map f).app (Opposite.op Y))))

@[simp]

theorem CategoryTheory.Profunctor.compDiagram_map_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) (X : C) (Y : E) {X✝ Y✝ : Dᵒᵖ} (g : X✝ ⟶ Y✝) (U : D) : ((P.compDiagram Q X Y).map g).app U = TypeCat.ofHom (Prod.map (⇑(ConcreteCategory.hom ((P.obj X).map g))) id)

@[simp]

theorem CategoryTheory.Profunctor.compDiagram_obj_obj {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) (X : C) (Y : E) (U : Dᵒᵖ) (V : D) : ((P.compDiagram Q X Y).obj U).obj V = ((P.obj X).obj U × (Q.obj V).obj (Opposite.op Y))

def CategoryTheory.Profunctor.compDiagramMap {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) {X X' : C} {Y Y' : E} (f : X ⟶ X') (g : Y ⟶ Y') : P.compDiagram Q X Y' ⟶ P.compDiagram Q X' Y

The map on composition diagrams induced by morphisms in the outer variables.

Equations

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

@[simp]

theorem CategoryTheory.Profunctor.compDiagramMap_app_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) {X X' : C} {Y Y' : E} (f : X ⟶ X') (g : Y ⟶ Y') (d : Dᵒᵖ) (d' : D) : ((P.compDiagramMap Q f g).app d).app d' = TypeCat.ofHom (Prod.map ⇑(ConcreteCategory.hom ((P.map f).app d)) ⇑(ConcreteCategory.hom ((Q.obj d').map g.op)))

@[simp]

theorem CategoryTheory.Profunctor.compDiagramMap_id {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) (X : C) (Y : E) : P.compDiagramMap Q (CategoryStruct.id X) (CategoryStruct.id Y) = CategoryStruct.id (P.compDiagram Q X Y)

@[simp]

theorem CategoryTheory.Profunctor.compDiagramMap_comp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : E} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) : P.compDiagramMap Q (CategoryStruct.comp f f') (CategoryStruct.comp g g') = CategoryStruct.comp (P.compDiagramMap Q f g') (P.compDiagramMap Q f' g)

@[implicit_reducible]

def CategoryTheory.Profunctor.univComp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] [Limits.ChosenCoends.{v, u, max w w', max (w + 1) (w' + 1)} (Type (max w w'))] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) : Profunctor.{max w w', v_1, v_2, u_1, u_2} C E

Composition of profunctors using a chosen coend construction.

Equations

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

@[simp]

theorem CategoryTheory.Profunctor.univComp_obj_map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] [Limits.ChosenCoends.{v, u, max w w', max (w + 1) (w' + 1)} (Type (max w w'))] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) (X : C) {X✝ Y✝ : Eᵒᵖ} (f : X✝ ⟶ Y✝) : ((P.univComp Q).obj X).map f = Limits.chosenCoend.map (P.compDiagramMap Q (CategoryStruct.id X) f.unop)

@[simp]

theorem CategoryTheory.Profunctor.univComp_map_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] [Limits.ChosenCoends.{v, u, max w w', max (w + 1) (w' + 1)} (Type (max w w'))] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) {X✝ Y✝ : C} (g : X✝ ⟶ Y✝) (X : Eᵒᵖ) : ((P.univComp Q).map g).app X = Limits.chosenCoend.map (P.compDiagramMap Q g (CategoryStruct.id (Opposite.unop X)))

@[simp]

theorem CategoryTheory.Profunctor.univComp_obj_obj {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] [Limits.ChosenCoends.{v, u, max w w', max (w + 1) (w' + 1)} (Type (max w w'))] (P : Profunctor.{w, v_1, v, u_1, u} C D) (Q : Profunctor.{w', v, v_2, u, u_2} D E) (X : C) (Y : Eᵒᵖ) : ((P.univComp Q).obj X).obj Y = Limits.chosenCoend (P.compDiagram Q X (Opposite.unop Y))

@[implicit_reducible]

def CategoryTheory.Profunctor.comp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{max u w, v_1, v, u_1, u} C D) (Q : Profunctor.{max u w, v, v_2, u, u_2} D E) : Profunctor.{max u w, v_1, v_2, u_1, u_2} C E

Composition of profunctors in the standard universe configuration.

Equations

• P.comp Q = P.univComp Q

@[simp]

theorem CategoryTheory.Profunctor.comp_map_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{max u w, v_1, v, u_1, u} C D) (Q : Profunctor.{max u w, v, v_2, u, u_2} D E) {X✝ Y✝ : C} (g : X✝ ⟶ Y✝) (X : Eᵒᵖ) : ((P.comp Q).map g).app X = Limits.chosenCoend.map (P.compDiagramMap Q g (CategoryStruct.id (Opposite.unop X)))

@[simp]

theorem CategoryTheory.Profunctor.comp_obj_map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{max u w, v_1, v, u_1, u} C D) (Q : Profunctor.{max u w, v, v_2, u, u_2} D E) (X : C) {X✝ Y✝ : Eᵒᵖ} (f : X✝ ⟶ Y✝) : ((P.comp Q).obj X).map f = Limits.chosenCoend.map (P.compDiagramMap Q (CategoryStruct.id X) f.unop)

@[simp]

theorem CategoryTheory.Profunctor.comp_obj_obj {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u} [Category.{v, u} D] {E : Type u_2} [Category.{v_2, u_2} E] (P : Profunctor.{max u w, v_1, v, u_1, u} C D) (Q : Profunctor.{max u w, v, v_2, u, u_2} D E) (X : C) (Y : Eᵒᵖ) : ((P.comp Q).obj X).obj Y = Limits.chosenCoend (P.compDiagram Q X (Opposite.unop Y))

def CategoryTheory.Profunctor.whiskerLeft {C D E : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] (P : Profunctor.{max u w, v_1, v_2, u, u} C D) {Q R : Profunctor.{max u w, v_2, v_3, u, u} D E} (f : Q ⟶ R) : P.comp Q ⟶ P.comp R

Left whiskering of a natural transformation of profunctors.

Equations

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

@[simp]

theorem CategoryTheory.Profunctor.whiskerLeft_app_app {C D E : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] (P : Profunctor.{max u w, v_1, v_2, u, u} C D) {Q R : Profunctor.{max u w, v_2, v_3, u, u} D E} (f : Q ⟶ R) (X : C) (Y : Eᵒᵖ) : ((P.whiskerLeft f).app X).app Y = Limits.chosenCoend.map { app := fun (d : Dᵒᵖ) => { app := fun (d' : D) => TypeCat.ofHom (Prod.map id ⇑(ConcreteCategory.hom ((f.app d').app Y))), naturality := ⋯ }, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Profunctor.whiskerLeft_id {C D E : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] (P : Profunctor.{max u w, v_1, v_2, u, u} C D) (Q : Profunctor.{max u w, v_2, v_3, u, u} D E) : P.whiskerLeft (CategoryStruct.id Q) = CategoryStruct.id (P.comp Q)

@[simp]

theorem CategoryTheory.Profunctor.whiskerLeft_comp {C D E : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] (P : Profunctor.{max u w, v_1, v_2, u, u} C D) {Q R S : Profunctor.{max u w, v_2, v_3, u, u} D E} (f : Q ⟶ R) (g : R ⟶ S) : P.whiskerLeft (CategoryStruct.comp f g) = CategoryStruct.comp (P.whiskerLeft f) (P.whiskerLeft g)

def CategoryTheory.Profunctor.whiskerRight {C D E : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] {P Q : Profunctor.{max u w, v_1, v_2, u, u} C D} (R : Profunctor.{max u w, v_2, v_3, u, u} D E) (f : P ⟶ Q) : P.comp R ⟶ Q.comp R

Right whiskering of a natural transformation of profunctors.

Equations

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

@[simp]

theorem CategoryTheory.Profunctor.whiskerRight_app_app {C D E : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] {P Q : Profunctor.{max u w, v_1, v_2, u, u} C D} (R : Profunctor.{max u w, v_2, v_3, u, u} D E) (f : P ⟶ Q) (X : C) (Y : Eᵒᵖ) : ((whiskerRight R f).app X).app Y = Limits.chosenCoend.map { app := fun (d : Dᵒᵖ) => { app := fun (d' : D) => TypeCat.ofHom (Prod.map (⇑(ConcreteCategory.hom ((f.app X).app d))) id), naturality := ⋯ }, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Profunctor.id_whiskerRight {C D E : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] {P : Profunctor.{max u w, v_1, v_2, u, u} C D} (R : Profunctor.{max u w, v_2, v_3, u, u} D E) : whiskerRight R (CategoryStruct.id P) = CategoryStruct.id (P.comp R)

@[simp]

theorem CategoryTheory.Profunctor.comp_whiskerRight {C D E : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] {P Q R : Profunctor.{max u w, v_1, v_2, u, u} C D} (f : P ⟶ Q) (g : Q ⟶ R) (S : Profunctor.{max u w, v_2, v_3, u, u} D E) : whiskerRight S (CategoryStruct.comp f g) = CategoryStruct.comp (whiskerRight S f) (whiskerRight S g)

@[simp]

theorem CategoryTheory.Profunctor.whisker_exchange {C D E : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] {P Q : Profunctor.{max u w, v_1, v_2, u, u} C D} {R S : Profunctor.{max u w, v_2, v_3, u, u} D E} (f : P ⟶ Q) (g : R ⟶ S) : CategoryStruct.comp (P.whiskerLeft g) (whiskerRight S f) = CategoryStruct.comp (whiskerRight R f) (Q.whiskerLeft g)

@[simp]

theorem CategoryTheory.Profunctor.whisker_exchange_assoc {C D E : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] {P Q : Profunctor.{max u w, v_1, v_2, u, u} C D} {R S : Profunctor.{max u w, v_2, v_3, u, u} D E} (f : P ⟶ Q) (g : R ⟶ S) {Z : Profunctor.{max u w, v_1, v_3, u, u} C E} (h : Q.comp S ⟶ Z) : CategoryStruct.comp (P.whiskerLeft g) (CategoryStruct.comp (whiskerRight S f) h) = CategoryStruct.comp (whiskerRight R f) (CategoryStruct.comp (Q.whiskerLeft g) h)

def CategoryTheory.Profunctor.leftUnitor {C : Type u} [Category.{u, u} C] {D : Type u} [Category.{v_1, u} D] (P : Profunctor.{u, u, v_1, u, u} C D) : Profunctor.id.comp P ≅ P

The left unitor isomorphism Profunctor.id.comp P ≅ P for composition of profunctors.

Equations

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

@[simp]

theorem CategoryTheory.Profunctor.leftUnitor_inv_app_app {C : Type u} [Category.{u, u} C] {D : Type u} [Category.{v_1, u} D] (P : Profunctor.{u, u, v_1, u, u} C D) (X : C) (X✝ : Dᵒᵖ) : (P.leftUnitor.inv.app X).app X✝ = TypeCat.ofHom fun (x : (P.obj X).obj X✝) => Quot.mk (Limits.Types.coendRel (Profunctor.id.compDiagram P X (Opposite.unop X✝))) ⟨X, (CategoryStruct.id X, x)⟩

@[simp]

theorem CategoryTheory.Profunctor.leftUnitor_hom_app_app_mk {C : Type u} [Category.{u, u} C] {D : Type u} [Category.{v_1, u} D] (P : Profunctor.{u, u, v_1, u, u} C D) (X : C) (Y : Dᵒᵖ) (d : C) (f : d ⟶ X) (x : (P.obj d).obj Y) : (ConcreteCategory.hom ((P.leftUnitor.hom.app X).app Y)) (Quot.mk (Limits.Types.coendRel (Profunctor.id.compDiagram P X (Opposite.unop Y))) ⟨d, (f, x)⟩) = (ConcreteCategory.hom ((P.map f).app Y)) x

@[simp]

theorem CategoryTheory.Profunctor.id_whiskerLeft {C : Type u} [Category.{u, u} C] {D : Type u} [Category.{v_1, u} D] {P Q : Profunctor.{u, u, v_1, u, u} C D} (f : P ⟶ Q) : Profunctor.id.whiskerLeft f = CategoryStruct.comp P.leftUnitor.hom (CategoryStruct.comp f Q.leftUnitor.inv)

def CategoryTheory.Profunctor.rightUnitor {C : Type u} [Category.{v_1, u} C] {D : Type u} [Category.{u, u} D] (P : Profunctor.{u, v_1, u, u, u} C D) : P.comp Profunctor.id ≅ P

The right unitor isomorphism P.comp Profunctor.id ≅ P for composition of profunctors.

Equations

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

@[simp]

theorem CategoryTheory.Profunctor.rightUnitor_inv_app_app {C : Type u} [Category.{v_1, u} C] {D : Type u} [Category.{u, u} D] (P : Profunctor.{u, v_1, u, u, u} C D) (X : C) (X✝ : Dᵒᵖ) : (P.rightUnitor.inv.app X).app X✝ = TypeCat.ofHom fun (x : (P.obj X).obj X✝) => Quot.mk (Limits.Types.coendRel (P.compDiagram Profunctor.id X (Opposite.unop X✝))) ⟨Opposite.unop X✝, (x, CategoryStruct.id (Opposite.unop X✝))⟩

@[simp]

theorem CategoryTheory.Profunctor.rightUnitor_hom_app_app_mk {C : Type u} [Category.{v_1, u} C] {D : Type u} [Category.{u, u} D] (P : Profunctor.{u, v_1, u, u, u} C D) (X : C) (Y : Dᵒᵖ) (d : D) (x : (P.obj X).obj (Opposite.op d)) (f : Opposite.unop Y ⟶ d) : (ConcreteCategory.hom ((P.rightUnitor.hom.app X).app Y)) (Quot.mk (Limits.Types.coendRel (P.compDiagram Profunctor.id X (Opposite.unop Y))) ⟨d, (x, f)⟩) = (ConcreteCategory.hom ((P.obj X).map f.op)) x

@[simp]

theorem CategoryTheory.Profunctor.whiskerRight_id {C : Type u} [Category.{v_1, u} C] {D : Type u} [Category.{u, u} D] {P Q : Profunctor.{u, v_1, u, u, u} C D} (f : P ⟶ Q) : whiskerRight Profunctor.id f = CategoryStruct.comp P.rightUnitor.hom (CategoryStruct.comp f Q.rightUnitor.inv)

def CategoryTheory.Profunctor.associatorHomFun {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) (Q : Profunctor.{max w u, v_2, v_3, u, u} D E) (R : Profunctor.{max w u, v_3, v_4, u, u} E F) (X : C) (Y : Fᵒᵖ) (e : E) (r : (R.obj e).obj (Opposite.op (Opposite.unop Y))) : (j : D) × ((P.compDiagram Q X e).obj (Opposite.op j)).obj j → (j : D) × ((P.compDiagram (Q.comp R) X (Opposite.unop Y)).obj (Opposite.op j)).obj j

The map on representatives underlying associatorHom.

Equations

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

theorem CategoryTheory.Profunctor.associatorHomFun_rel {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) (Q : Profunctor.{max w u, v_2, v_3, u, u} D E) (R : Profunctor.{max w u, v_3, v_4, u, u} E F) (X : C) (Y : Fᵒᵖ) (e : E) (r : (R.obj e).obj (Opposite.op (Opposite.unop Y))) ⦃a b : (j : D) × ((P.compDiagram Q X e).obj (Opposite.op j)).obj j⦄ : Limits.Types.coendRel (P.compDiagram Q X e) a b → Limits.Types.coendRel (P.compDiagram (Q.comp R) X (Opposite.unop Y)) (P.associatorHomFun Q R X Y e r a) (P.associatorHomFun Q R X Y e r b)

associatorHomFun respects the coend relation.

def CategoryTheory.Profunctor.associatorHom {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) (Q : Profunctor.{max w u, v_2, v_3, u, u} D E) (R : Profunctor.{max w u, v_3, v_4, u, u} E F) (X : C) (Y : Fᵒᵖ) : (((P.comp Q).comp R).obj X).obj Y ⟶ ((P.comp (Q.comp R)).obj X).obj Y

The forward map of the objectwise associator for composition of profunctors.

Equations

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

def CategoryTheory.Profunctor.associatorInvFun {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) (Q : Profunctor.{max w u, v_2, v_3, u, u} D E) (R : Profunctor.{max w u, v_3, v_4, u, u} E F) (X : C) (Y : Fᵒᵖ) (d : D) (p : (P.obj X).obj (Opposite.op d)) : (j : E) × ((Q.compDiagram R d (Opposite.unop Y)).obj (Opposite.op j)).obj j → (j : E) × (((P.comp Q).compDiagram R X (Opposite.unop Y)).obj (Opposite.op j)).obj j

The map on representatives underlying associatorInv.

Equations

• P.associatorInvFun Q R X Y d p ⟨e, (q, r)⟩ = ⟨e, (Quot.mk (CategoryTheory.Limits.Types.coendRel (P.compDiagram Q X (Opposite.unop (Opposite.op e)))) ⟨d, (p, q)⟩, r)⟩

theorem CategoryTheory.Profunctor.associatorInvFun_rel {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) (Q : Profunctor.{max w u, v_2, v_3, u, u} D E) (R : Profunctor.{max w u, v_3, v_4, u, u} E F) (X : C) (Y : Fᵒᵖ) (d : D) (p : (P.obj X).obj (Opposite.op d)) ⦃a b : (j : E) × ((Q.compDiagram R d (Opposite.unop Y)).obj (Opposite.op j)).obj j⦄ : Limits.Types.coendRel (Q.compDiagram R d (Opposite.unop Y)) a b → Limits.Types.coendRel ((P.comp Q).compDiagram R X (Opposite.unop Y)) (P.associatorInvFun Q R X Y d p a) (P.associatorInvFun Q R X Y d p b)

associatorInvFun respects the coend relation.

def CategoryTheory.Profunctor.associatorInv {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) (Q : Profunctor.{max w u, v_2, v_3, u, u} D E) (R : Profunctor.{max w u, v_3, v_4, u, u} E F) (X : C) (Y : Fᵒᵖ) : ((P.comp (Q.comp R)).obj X).obj Y ⟶ (((P.comp Q).comp R).obj X).obj Y

The inverse map of the objectwise associator for composition of profunctors.

Equations

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

def CategoryTheory.Profunctor.associatorComponents {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) (Q : Profunctor.{max w u, v_2, v_3, u, u} D E) (R : Profunctor.{max w u, v_3, v_4, u, u} E F) (X : C) (Y : Fᵒᵖ) : (((P.comp Q).comp R).obj X).obj Y ≅ ((P.comp (Q.comp R)).obj X).obj Y

The objectwise components of the associator isomorphism (P.comp Q).comp R ≅ P.comp (Q.comp R).

Equations

• P.associatorComponents Q R X Y = { hom := P.associatorHom Q R X Y, inv := P.associatorInv Q R X Y, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def CategoryTheory.Profunctor.associator {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) (Q : Profunctor.{max w u, v_2, v_3, u, u} D E) (R : Profunctor.{max w u, v_3, v_4, u, u} E F) : (P.comp Q).comp R ≅ P.comp (Q.comp R)

The associator isomorphism (P.comp Q).comp R ≅ P.comp (Q.comp R) for composition of profunctors.

Equations

• P.associator Q R = CategoryTheory.NatIso.ofComponents (fun (X : C) => CategoryTheory.NatIso.ofComponents (fun (Y : Fᵒᵖ) => P.associatorComponents Q R X Y) ⋯) ⋯

@[simp]

theorem CategoryTheory.Profunctor.associator_hom_app_app_mk {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) (Q : Profunctor.{max w u, v_2, v_3, u, u} D E) (R : Profunctor.{max w u, v_3, v_4, u, u} E F) (X : C) (Y : Fᵒᵖ) (d : D) (e : E) (p : (P.obj X).obj (Opposite.op d)) (q : (Q.obj d).obj (Opposite.op e)) (r : (R.obj e).obj Y) : (ConcreteCategory.hom (((P.associator Q R).hom.app X).app Y)) (Quot.mk (Limits.Types.coendRel ((P.comp Q).compDiagram R X (Opposite.unop Y))) ⟨e, (Quot.mk (Limits.Types.coendRel (P.compDiagram Q X e)) ⟨d, (p, q)⟩, r)⟩) = Quot.mk (Limits.Types.coendRel (P.compDiagram (Q.comp R) X (Opposite.unop Y))) ⟨d, (p, Quot.mk (Limits.Types.coendRel (Q.compDiagram R d (Opposite.unop Y))) ⟨e, (q, r)⟩)⟩

@[simp]

theorem CategoryTheory.Profunctor.associator_inv_app_app_mk {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) (Q : Profunctor.{max w u, v_2, v_3, u, u} D E) (R : Profunctor.{max w u, v_3, v_4, u, u} E F) (X : C) (Y : Fᵒᵖ) (d : D) (e : E) (p : (P.obj X).obj (Opposite.op d)) (q : (Q.obj d).obj (Opposite.op e)) (r : (R.obj e).obj Y) : (ConcreteCategory.hom (((P.associator Q R).inv.app X).app Y)) (Quot.mk (Limits.Types.coendRel (P.compDiagram (Q.comp R) X (Opposite.unop Y))) ⟨d, (p, Quot.mk (Limits.Types.coendRel (Q.compDiagram R d (Opposite.unop Y))) ⟨e, (q, r)⟩)⟩) = Quot.mk (Limits.Types.coendRel ((P.comp Q).compDiagram R X (Opposite.unop Y))) ⟨e, (Quot.mk (Limits.Types.coendRel (P.compDiagram Q X e)) ⟨d, (p, q)⟩, r)⟩

@[simp]

theorem CategoryTheory.Profunctor.comp_whiskerLeft {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) (Q : Profunctor.{max w u, v_2, v_3, u, u} D E) (R : Profunctor.{max w u, v_3, v_4, u, u} E F) {S : Profunctor.{max u w, v_3, v_4, u, u} E F} (f : R ⟶ S) : (P.comp Q).whiskerLeft f = CategoryStruct.comp (P.associator Q R).hom (CategoryStruct.comp (P.whiskerLeft (Q.whiskerLeft f)) (P.associator Q S).inv)

@[simp]

theorem CategoryTheory.Profunctor.whiskerRight_comp {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] {P : Profunctor.{max w u, v_1, v_2, u, u} C D} {Q : Profunctor.{max u w, v_1, v_2, u, u} C D} (f : P ⟶ Q) (R : Profunctor.{max u w, v_2, v_3, u, u} D E) (S : Profunctor.{max u w, v_3, v_4, u, u} E F) : whiskerRight (R.comp S) f = CategoryStruct.comp (P.associator R S).inv (CategoryStruct.comp (whiskerRight S (whiskerRight R f)) (Q.associator R S).hom)

@[simp]

theorem CategoryTheory.Profunctor.whisker_assoc {C D E F : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] (P : Profunctor.{max w u, v_1, v_2, u, u} C D) {Q : Profunctor.{max w u, v_2, v_3, u, u} D E} {R : Profunctor.{max u w, v_2, v_3, u, u} D E} (f : Q ⟶ R) (S : Profunctor.{max u w, v_3, v_4, u, u} E F) : whiskerRight S (P.whiskerLeft f) = CategoryStruct.comp (P.associator Q S).hom (CategoryStruct.comp (P.whiskerLeft (whiskerRight S f)) (P.associator R S).inv)