Documentation

Mathlib.CategoryTheory.Profunctor.Bicategory

The Profunctor Bicategory #

This file defines the bicategory ProfCat whose objects are categories and whose 1-morphisms are profunctors. The 2-morphisms are natural transformations between profunctors.

The bicategory instance is defined on ProfCat.{u, u}, with profunctors valued in Type u. Its operations simplify to the corresponding operations in the Profunctor namespace.

source
structure CategoryTheory.ProfCat :
Type (max (u + 1) (v + 1))

The bicategory of categories where the 1-morphisms are profunctors.

  • of :: (
    • obj : Type u

      The objects of the bicategory are types...

    • str : Category.{v, u} self.obj

      ... bundled with a category instance.

  • )
Instances For
    source
    @[instance_reducible]
    instance CategoryTheory.instCoeSortProfCatType :
    CoeSort ProfCat (Type u)
    Equations
    source
    @[simp]
    theorem CategoryTheory.ProfCat.of_obj (C : Type u) [Category.{v, u} C] :
    { obj := C, str := inst✝ }.obj = C
    source
    @[simp]
    theorem CategoryTheory.ProfCat.coe_of (C : ProfCat) :
    { obj := C.obj, str := C.str } = C
    source
    @[simp]
    theorem CategoryTheory.Profunctor.pentagon {C D E F G : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] [Category.{v_5, u} G] (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) (R : Profunctor.{max u w, v_3, v_4, u, u} E F) (S : Profunctor.{max u w, v_4, v_5, u, u} F G) :
    CategoryStruct.comp (whiskerRight S (P.associator Q R).hom) (CategoryStruct.comp (P.associator (Q.comp R) S).hom (P.whiskerLeft (Q.associator R S).hom)) = CategoryStruct.comp ((P.comp Q).associator R S).hom (P.associator Q (R.comp S)).hom
    source
    @[simp]
    theorem CategoryTheory.Profunctor.pentagon_assoc {C D E F G : Type u} [Category.{v_1, u} C] [Category.{v_2, u} D] [Category.{v_3, u} E] [Category.{v_4, u} F] [Category.{v_5, u} G] (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) (R : Profunctor.{max u w, v_3, v_4, u, u} E F) (S : Profunctor.{max u w, v_4, v_5, u, u} F G) {Z : Profunctor.{max u w, v_1, v_5, u, u} C G} (h : P.comp (Q.comp (R.comp S)) ⟶ Z) :
    CategoryStruct.comp (whiskerRight S (P.associator Q R).hom) (CategoryStruct.comp (P.associator (Q.comp R) S).hom (CategoryStruct.comp (P.whiskerLeft (Q.associator R S).hom) h)) = CategoryStruct.comp ((P.comp Q).associator R S).hom (CategoryStruct.comp (P.associator Q (R.comp S)).hom h)
    source
    @[simp]
    theorem CategoryTheory.Profunctor.triangle {C D E : Type u} [Category.{v_1, u} C] [Category.{u, u} D] [Category.{v_2, u} E] (P : Profunctor.{u, v_1, u, u, u} C D) (Q : Profunctor.{u, u, v_2, u, u} D E) :
    CategoryStruct.comp (P.associator Profunctor.id Q).hom (P.whiskerLeft Q.leftUnitor.hom) = whiskerRight Q P.rightUnitor.hom
    source
    @[simp]
    theorem CategoryTheory.Profunctor.triangle_assoc {C D E : Type u} [Category.{v_1, u} C] [Category.{u, u} D] [Category.{v_2, u} E] (P : Profunctor.{u, v_1, u, u, u} C D) (Q : Profunctor.{u, u, v_2, u, u} D E) {Z : Profunctor.{u, v_1, v_2, u, u} C E} (h : P.comp Q ⟶ Z) :
    CategoryStruct.comp (P.associator Profunctor.id Q).hom (CategoryStruct.comp (P.whiskerLeft Q.leftUnitor.hom) h) = CategoryStruct.comp (whiskerRight Q P.rightUnitor.hom) h
    source
    @[instance_reducible]
    instance CategoryTheory.ProfCat.bicategory :
    Bicategory ProfCat

    The bicategory of categories, profunctors, and natural transformations.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[simp]
    theorem CategoryTheory.ProfCat.bicategory_leftUnitor {a✝ b✝ : ProfCat} (P : Profunctor.{u, u, u, u, u} a✝.obj b✝.obj) :
    Bicategory.leftUnitor P = P.leftUnitor
    source
    @[simp]
    theorem CategoryTheory.ProfCat.bicategory_whiskerRight {a✝ b✝ c✝ : ProfCat} {f✝ g✝ : Profunctor.{u, u, u, u, u} a✝.obj b✝.obj} (f : f✝ ⟶ g✝) (R : Profunctor.{u, u, u, u, u} b✝.obj c✝.obj) :
    Bicategory.whiskerRight f R = Profunctor.whiskerRight R f
    source
    @[simp]
    theorem CategoryTheory.ProfCat.bicategory_rightUnitor {a✝ b✝ : ProfCat} (P : Profunctor.{u, u, u, u, u} a✝.obj b✝.obj) :
    Bicategory.rightUnitor P = P.rightUnitor
    source
    @[simp]
    theorem CategoryTheory.ProfCat.bicategory_comp {X✝ Y✝ Z✝ : ProfCat} (P : Profunctor.{u, u, u, u, u} X✝.obj Y✝.obj) (Q : Profunctor.{u, u, u, u, u} Y✝.obj Z✝.obj) :
    CategoryStruct.comp P Q = P.comp Q
    source
    @[simp]
    theorem CategoryTheory.ProfCat.bicategory_whiskerLeft {x✝ x✝¹ x✝² : ProfCat} (P : Profunctor.{u, u, u, u, u} x✝.obj x✝¹.obj) {x✝³ x✝⁴ : Profunctor.{u, u, u, u, u} x✝¹.obj x✝².obj} (f : x✝³ ⟶ x✝⁴) :
    Bicategory.whiskerLeft P f = P.whiskerLeft f
    source
    @[simp]
    theorem CategoryTheory.ProfCat.bicategory_id (X : ProfCat) :
    CategoryStruct.id X = Profunctor.id
    source
    @[simp]
    theorem CategoryTheory.ProfCat.bicategory_associator {a✝ b✝ c✝ d✝ : ProfCat} (P : Profunctor.{u, u, u, u, u} a✝.obj b✝.obj) (Q : Profunctor.{u, u, u, u, u} b✝.obj c✝.obj) (R : Profunctor.{u, u, u, u, u} c✝.obj d✝.obj) :
    Bicategory.associator P Q R = P.associator Q R
    source
    theorem CategoryTheory.ProfCat.hom_ext {C D : ProfCat} {P Q : C ⟶ D} {η θ : P ⟶ Q} (h : ∀ (X : C.obj) (Y : D.objᵒᵖ) (x : (P.obj X).obj Y), (ConcreteCategory.hom ((η.app X).app Y)) x = (ConcreteCategory.hom ((θ.app X).app Y)) x) :
    η = θ

    Two 2-morphisms in ProfCat are equal if they agree on every element.

    source
    theorem CategoryTheory.ProfCat.hom_ext_iff {C D : ProfCat} {P Q : C ⟶ D} {η θ : P ⟶ Q} :
    η = θ ↔ ∀ (X : C.obj) (Y : D.objᵒᵖ) (x : (P.obj X).obj Y), (ConcreteCategory.hom ((η.app X).app Y)) x = (ConcreteCategory.hom ((θ.app X).app Y)) x