Profunctors

A profunctor from a category C to a category D is a functor from C to a category of presheaves of sets on D. We define this as Profunctor.{w} C D := C ⥤ Dᵒᵖ ⥤ Type w.

This file provides convenient constructors ProfunctorCore and ProfunctorCore.Hom for profunctors and natural transformations between them. We also define the identity profunctor Profunctor.id as the Yoneda bifunctor, the opposite of a profunctor, the ulift of a profunctor, whiskering of a profunctor with functors, and the profunctors in both directions corresponding to a functor C ⥤ D (see Functor.toProfunctor and Functor.toProfunctorFlip).

Future work

• Define composition of profunctors.
• Define the bicategory of categories where the 1-morphisms are profunctors.

structure CategoryTheory.ProfunctorCore (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] : Type (max (max (max (max u₁ u₂) v₁) v₂) (w + 1))

Custom structure to construct profunctors, i.e. bifunctors C ⥤ Dᵒᵖ ⥤ Type w.

• obj : C → D → Type w

  The object part

• map {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y') : self.obj X Y' ⟶ self.obj X' Y

  The morphism part

• map_id (X : C) (Y : D) : self.map (CategoryStruct.id X) (CategoryStruct.id Y) = CategoryStruct.id (self.obj X Y)
• map_comp {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : D} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) : self.map (CategoryStruct.comp f f') (CategoryStruct.comp g g') = CategoryStruct.comp (self.map f g') (self.map f' g)

@[reducible, inline]

abbrev CategoryTheory.Profunctor (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] : Type (max v₁ (max u₂ w) u₁ (max (max (w + 1) u₂) w) v₂)

A profunctor from C to D (Profunctor.{w} C D) is a bifunctor C ⥤ Dᵒᵖ ⥤ Type w.

Equations

• CategoryTheory.Profunctor.{?u.23, ?u.22, ?u.21, ?u.20, ?u.19} C D = CategoryTheory.Functor C (CategoryTheory.Functor Dᵒᵖ (Type ?u.23))

@[reducible, inline]

abbrev CategoryTheory.Functor.profunctor {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C (Functor Dᵒᵖ (Type w))) : Profunctor.{w, v₁, v₂, u₁, u₂} C D

Typecheck a bifunctor C ⥤ Dᵒᵖ ⥤ Type w as a profunctor.

Equations

• F.profunctor = F

structure CategoryTheory.ProfunctorCore.Hom {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P Q : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) : Type (max (max u₁ u₂) w)

Custom structure to construct natural transformations between profunctors, see CategoryTheory.Profunctor.ofHom.

• app (X : C) (Y : D) : P.obj X Y ⟶ Q.obj X Y

  The components of the natural transformation

• naturality ⦃X X' : C⦄ ⦃Y Y' : D⦄ (f : X ⟶ X') (g : Y ⟶ Y') : CategoryStruct.comp (P.map f g) (self.app X' Y) = CategoryStruct.comp (self.app X Y') (Q.map f g)

@[simp]

theorem CategoryTheory.ProfunctorCore.Hom.naturality_assoc {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {P Q : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} (self : P.Hom Q) ⦃X X' : C⦄ ⦃Y Y' : D⦄ (f : X ⟶ X') (g : Y ⟶ Y') {Z : Type w} (h : Q.obj X' Y ⟶ Z) : CategoryStruct.comp (P.map f g) (CategoryStruct.comp (self.app X' Y) h) = CategoryStruct.comp (self.app X Y') (CategoryStruct.comp (Q.map f g) h)

@[simp]

theorem CategoryTheory.ProfunctorCore.map_id_comp {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) (X : C) {Y Y' Y'' : D} (g : Y ⟶ Y') (g' : Y' ⟶ Y'') : P.map (CategoryStruct.id X) (CategoryStruct.comp g g') = CategoryStruct.comp (P.map (CategoryStruct.id X) g') (P.map (CategoryStruct.id X) g)

@[simp]

theorem CategoryTheory.ProfunctorCore.map_comp_id {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X X' X'' : C} (Y : D) (f : X ⟶ X') (f' : X' ⟶ X'') : P.map (CategoryStruct.comp f f') (CategoryStruct.id Y) = CategoryStruct.comp (P.map f (CategoryStruct.id Y)) (P.map f' (CategoryStruct.id Y))

@[simp]

theorem CategoryTheory.ProfunctorCore.map_lid_comp_map_rid {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y') : CategoryStruct.comp (P.map (CategoryStruct.id X) g) (P.map f (CategoryStruct.id Y)) = P.map f g

@[simp]

theorem CategoryTheory.ProfunctorCore.map_lid_comp_map_rid_assoc {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y') {Z : Type w} (h : P.obj X' Y ⟶ Z) : CategoryStruct.comp (P.map (CategoryStruct.id X) g) (CategoryStruct.comp (P.map f (CategoryStruct.id Y)) h) = CategoryStruct.comp (P.map f g) h

@[simp]

theorem CategoryTheory.ProfunctorCore.map_rid_comp_map_lid {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y') : CategoryStruct.comp (P.map f (CategoryStruct.id Y')) (P.map (CategoryStruct.id X') g) = P.map f g

@[simp]

theorem CategoryTheory.ProfunctorCore.map_rid_comp_map_lid_assoc {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y') {Z : Type w} (h : P.obj X' Y ⟶ Z) : CategoryStruct.comp (P.map f (CategoryStruct.id Y')) (CategoryStruct.comp (P.map (CategoryStruct.id X') g) h) = CategoryStruct.comp (P.map f g) h

def CategoryTheory.Profunctor.ofCore {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) : Profunctor.{w, v₁, v₂, u₁, u₂} C D

Construct a profunctor from a ProfunctorCore.

Equations

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

@[simp]

theorem CategoryTheory.Profunctor.ofCore_obj_obj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) (X : C) (Y : Dᵒᵖ) : ((ofCore P).obj X).obj Y = P.obj X (Opposite.unop Y)

@[simp]

theorem CategoryTheory.Profunctor.ofCore_map_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X✝ Y✝ : C} (g : X✝ ⟶ Y✝) (X : Dᵒᵖ) : ((ofCore P).map g).app X = P.map g (CategoryStruct.id (Opposite.unop X))

@[simp]

theorem CategoryTheory.Profunctor.ofCore_obj_map {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) (X : C) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) : ((ofCore P).obj X).map f = P.map (CategoryStruct.id X) f.unop

def CategoryTheory.Profunctor.ofHom {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {P Q : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} (f : P.Hom Q) : ofCore P ⟶ ofCore Q

Construct a natural transformation between profunctors from a ProfunctorCore.Hom.

Equations

• CategoryTheory.Profunctor.ofHom f = { app := fun (X : C) => { app := fun (Y : Dᵒᵖ) => f.app X (Opposite.unop Y), naturality := ⋯ }, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Profunctor.ofHom_app_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {P Q : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} (f : P.Hom Q) (X : C) (Y : Dᵒᵖ) : ((ofHom f).app X).app Y = f.app X (Opposite.unop Y)

def CategoryTheory.Profunctor.id {C : Type u₁} [Category.{v₁, u₁} C] : Profunctor.{v₁, v₁, v₁, u₁, u₁} C C

The identity profunctor from C to C. This is defined as the Yoneda bifunctor.

Equations

• CategoryTheory.Profunctor.id = CategoryTheory.yoneda

@[simp]

theorem CategoryTheory.Profunctor.id_obj_map {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (Profunctor.id.obj X).map f = TypeCat.ofHom fun (g : Opposite.unop X✝ ⟶ X) => CategoryStruct.comp f.unop g

@[simp]

theorem CategoryTheory.Profunctor.id_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (Y : Cᵒᵖ) : (Profunctor.id.obj X).obj Y = (Opposite.unop Y ⟶ X)

@[simp]

theorem CategoryTheory.Profunctor.id_map_app {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (x✝ : Cᵒᵖ) : (Profunctor.id.map f).app x✝ = TypeCat.ofHom fun (g : Opposite.unop x✝ ⟶ X✝) => CategoryStruct.comp g f

def CategoryTheory.Profunctor.op {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) : Profunctor.{w, v₂, v₁, u₂, u₁} Dᵒᵖ Cᵒᵖ

The opposite of a profunctor.

Equations

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

@[simp]

theorem CategoryTheory.Profunctor.op_obj_obj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) (X : Dᵒᵖ) (Y : Cᵒᵖᵒᵖ) : (P.op.obj X).obj Y = (P.obj (Opposite.unop (Opposite.unop Y))).obj X

@[simp]

theorem CategoryTheory.Profunctor.op_map_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) {X✝ Y✝ : Dᵒᵖ} (g : X✝ ⟶ Y✝) (X : Cᵒᵖᵒᵖ) : (P.op.map g).app X = (P.obj (Opposite.unop (Opposite.unop X))).map g

@[simp]

theorem CategoryTheory.Profunctor.op_obj_map {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) (X : Dᵒᵖ) {X✝ Y✝ : Cᵒᵖᵒᵖ} (f : X✝ ⟶ Y✝) : (P.op.obj X).map f = (P.map f.unop.unop).app X

def CategoryTheory.Profunctor.whiskerLeft₂ {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {A : Type u_1} {B : Type u_2} [Category.{v_1, u_1} A] [Category.{v_2, u_2} B] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) (F : Functor A C) (G : Functor B D) : Profunctor.{w, v_1, v_2, u_1, u_2} A B

Whisker a profunctor from C to D with functors into C and D.

Equations

• P.whiskerLeft₂ F G = (((CategoryTheory.Functor.whiskeringLeft₂ (Type ?u.63)).obj F).obj G.op).obj P

@[simp]

theorem CategoryTheory.Profunctor.whiskerLeft₂_map_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {A : Type u_1} {B : Type u_2} [Category.{v_1, u_1} A] [Category.{v_2, u_2} B] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) (F : Functor A C) (G : Functor B D) {X✝ Y✝ : A} (f : X✝ ⟶ Y✝) (X : Bᵒᵖ) : ((P.whiskerLeft₂ F G).map f).app X = (P.map (F.map f)).app (Opposite.op (G.obj (Opposite.unop X)))

@[simp]

theorem CategoryTheory.Profunctor.whiskerLeft₂_obj_obj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {A : Type u_1} {B : Type u_2} [Category.{v_1, u_1} A] [Category.{v_2, u_2} B] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) (F : Functor A C) (G : Functor B D) (X : A) (X✝ : Bᵒᵖ) : ((P.whiskerLeft₂ F G).obj X).obj X✝ = (P.obj (F.obj X)).obj (Opposite.op (G.obj (Opposite.unop X✝)))

@[simp]

theorem CategoryTheory.Profunctor.whiskerLeft₂_obj_map {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {A : Type u_1} {B : Type u_2} [Category.{v_1, u_1} A] [Category.{v_2, u_2} B] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) (F : Functor A C) (G : Functor B D) (X : A) {X✝ Y✝ : Bᵒᵖ} (f : X✝ ⟶ Y✝) : ((P.whiskerLeft₂ F G).obj X).map f = (P.obj (F.obj X)).map (G.map f.unop).op

def CategoryTheory.Profunctor.ulift {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) : Profunctor.{max w' w, v₁, v₂, u₁, u₂} C D

Increase the universe level of a profunctor.

Equations

• CategoryTheory.Profunctor.ulift.{?u.28, ?u.27, ?u.26, ?u.25, ?u.24, ?u.23} P = (CategoryTheory.Functor.postcompose₂.obj CategoryTheory.uliftFunctor.{?u.28, ?u.27}).obj P

@[simp]

theorem CategoryTheory.Profunctor.ulift_map_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (X : Dᵒᵖ) : ((ulift.{w', w, v₁, v₂, u₁, u₂} P).map f).app X = TypeCat.ofHom fun (x : ULift.{w', w} ((P.obj X✝).obj X)) => { down := (ConcreteCategory.hom ((P.map f).app X)) x.down }

@[simp]

theorem CategoryTheory.Profunctor.ulift_obj_map {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) (X : C) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) : ((ulift.{w', w, v₁, v₂, u₁, u₂} P).obj X).map f = TypeCat.ofHom fun (x : ULift.{w', w} ((P.obj X).obj X✝)) => { down := (ConcreteCategory.hom ((P.obj X).map f)) x.down }

@[simp]

theorem CategoryTheory.Profunctor.ulift_obj_obj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) (X : C) (X✝ : Dᵒᵖ) : ((ulift.{w', w, v₁, v₂, u₁, u₂} P).obj X).obj X✝ = ULift.{w', w} ((P.obj X).obj X✝)

@[reducible, inline]

abbrev CategoryTheory.Profunctor.ulift1 {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (P : Profunctor.{w, v₁, v₂, u₁, u₂} C D) : Profunctor.{w + 1, v₁, v₂, u₁, u₂} C D

Increase the universe level of a profunctor by one. This enables dot notation P.ulift1, which is not possible with Profunctor.ulift.

Equations

• P.ulift1 = CategoryTheory.Profunctor.ulift.{?u.27 + 1, ?u.27, ?u.26, ?u.25, ?u.24, ?u.23} P

def CategoryTheory.Functor.toProfunctor {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) : Profunctor.{v₂, v₁, v₂, u₁, u₂} C D

Given a functor from C to D, this is the corresponding profunctor from C to D.

Equations

• F.toProfunctor = CategoryTheory.Profunctor.id.whiskerLeft₂ F (CategoryTheory.Functor.id D)

@[simp]

theorem CategoryTheory.Functor.toProfunctor_obj_map {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (X : C) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) : (F.toProfunctor.obj X).map f = TypeCat.ofHom fun (g : Opposite.unop X✝ ⟶ F.obj X) => CategoryStruct.comp f.unop g

@[simp]

theorem CategoryTheory.Functor.toProfunctor_map_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (X : Dᵒᵖ) : (F.toProfunctor.map f).app X = TypeCat.ofHom fun (g : Opposite.unop X ⟶ F.obj X✝) => CategoryStruct.comp g (F.map f)

@[simp]

theorem CategoryTheory.Functor.toProfunctor_obj_obj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (X : C) (X✝ : Dᵒᵖ) : (F.toProfunctor.obj X).obj X✝ = (Opposite.unop X✝ ⟶ F.obj X)

def CategoryTheory.Functor.toProfunctorRev {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) : Profunctor.{v₂, v₂, v₁, u₂, u₁} D C

Given a functor from C to D, this is the corresponding profunctor from D to C.

Equations

• F.toProfunctorRev = CategoryTheory.Profunctor.id.whiskerLeft₂ (CategoryTheory.Functor.id D) F

@[simp]

theorem CategoryTheory.Functor.toProfunctorRev_obj_map {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (X : D) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (F.toProfunctorRev.obj X).map f = TypeCat.ofHom fun (g : F.obj (Opposite.unop X✝) ⟶ X) => CategoryStruct.comp (F.map f.unop) g

@[simp]

theorem CategoryTheory.Functor.toProfunctorRev_map_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) : (F.toProfunctorRev.map f).app X = TypeCat.ofHom fun (g : F.obj (Opposite.unop X) ⟶ X✝) => CategoryStruct.comp g f

@[simp]

theorem CategoryTheory.Functor.toProfunctorRev_obj_obj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (X : D) (X✝ : Cᵒᵖ) : (F.toProfunctorRev.obj X).obj X✝ = (F.obj (Opposite.unop X✝) ⟶ X)