# mathlib3documentation

category_theory.bicategory.free

# Free bicategories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the free bicategory over a quiver. In this bicategory, the 1-morphisms are freely generated by the arrows in the quiver, and the 2-morphisms are freely generated by the formal identities, the formal unitors, and the formal associators modulo the relation derived from the axioms of a bicategory.

## Main definitions #

• free_bicategory B: the free bicategory over a quiver B.
• free_bicategory.lift F: the pseudofunctor from free_bicategory B to C associated with a prefunctor F from B to C.

Free bicategory over a quiver. Its objects are the same as those in the underlying quiver.

Equations
Instances for category_theory.free_bicategory
@[protected, instance]
Equations
inductive category_theory.free_bicategory.hom {B : Type u} [quiver B] :
B B Type (max u v)

1-morphisms in the free bicategory.

Instances for category_theory.free_bicategory.hom
@[protected, instance]
Equations
@[nolint]
inductive category_theory.free_bicategory.hom₂ {B : Type u} [quiver B] {a b : B} :
Type (max u v)

Representatives of 2-morphisms in the free bicategory.

Instances for category_theory.free_bicategory.hom₂
• category_theory.free_bicategory.hom₂.has_sizeof_inst
inductive category_theory.free_bicategory.rel {B : Type u} [quiver B] {a b : B} {f g : b} :
• vcomp_right : {B : Type u} [_inst_1 : quiver B] {a b : B} {f g h : (η : (θ₁ θ₂ : , (η.vcomp θ₂)
• vcomp_left : {B : Type u} [_inst_1 : quiver B] {a b : B} {f g h : (η₁ η₂ : (θ : , (η₂.vcomp θ)
• id_comp : {B : Type u} [_inst_1 : quiver B] {a b : B} {f g : (η : ,
• comp_id : {B : Type u} [_inst_1 : quiver B] {a b : B} {f g : (η : ,
• assoc : {B : Type u} [_inst_1 : quiver B] {a b : B} {f g h i : (η : (θ : (ι : , (η.vcomp (θ.vcomp ι))
• whisker_left : {B : Type u} [_inst_1 : quiver B] {a b c : B} (f : (g h : (η η' : ,
• whisker_left_id : {B : Type u} [_inst_1 : quiver B] {a b c : B} (f : (g : ,
• whisker_left_comp : {B : Type u} [_inst_1 : quiver B] {a b c : B} (f : {g h i : (η : (θ : ,
• id_whisker_left : {B : Type u} [_inst_1 : quiver B] {a b : B} {f g : (η : ,
• comp_whisker_left : {B : Type u} [_inst_1 : quiver B] {a b c d : B} (f : (g : {h h' : (η : ,
• whisker_right : {B : Type u} [_inst_1 : quiver B] {a b c : B} (f g : (h : (η η' : ,
• id_whisker_right : {B : Type u} [_inst_1 : quiver B] {a b c : B} (f : (g : ,
• comp_whisker_right : {B : Type u} [_inst_1 : quiver B] {a b c : B} {f g h : (i : (η : (θ : ,
• whisker_right_id :
• whisker_right_comp : {B : Type u} [_inst_1 : quiver B] {a b c d : B} {f f' : (g : (h : (η : ,
• whisker_assoc : {B : Type u} [_inst_1 : quiver B] {a b c d : B} (f : {g g' : (η : (h : ,
• whisker_exchange : {B : Type u} [_inst_1 : quiver B] {a b c : B} {f g : {h i : (η : (θ : ,
• associator_hom_inv : {B : Type u} [_inst_1 : quiver B] {a b c d : B} (f : (g : (h : ,
• associator_inv_hom : {B : Type u} [_inst_1 : quiver B] {a b c d : B} (f : (g : (h : ,
• left_unitor_hom_inv :
• left_unitor_inv_hom : {B : Type u} [_inst_1 : quiver B] {a b : B} (f : ,
• right_unitor_hom_inv :
• right_unitor_inv_hom : {B : Type u} [_inst_1 : quiver B] {a b : B} (f : ,
• pentagon : {B : Type u} [_inst_1 : quiver B] {a b c d e : B} (f : (g : (h : (i : ,
• triangle :

Relations between 2-morphisms in the free bicategory.

@[protected, instance]
Equations
@[protected, instance]

Bicategory structure on the free bicategory.

Equations
@[simp]
theorem category_theory.free_bicategory.mk_vcomp {B : Type u} [quiver B] {a b : category_theory.free_bicategory B} {f g h : a b}  :
(η.vcomp θ) = η θ
@[simp]
theorem category_theory.free_bicategory.mk_whisker_left {B : Type u} [quiver B] {a b c : category_theory.free_bicategory B} (f : a b) {g h : b c}  :
@[simp]
theorem category_theory.free_bicategory.mk_whisker_right {B : Type u} [quiver B] {a b c : category_theory.free_bicategory B} {f g : a b} (h : b c) :
theorem category_theory.free_bicategory.comp_def {B : Type u} [quiver B] {a b c : category_theory.free_bicategory B} (f : a b) (g : b c) :
@[simp]
@[simp]
theorem category_theory.free_bicategory.mk_associator_hom {B : Type u} [quiver B] {a b c d : category_theory.free_bicategory B} (f : a b) (g : b c) (h : c d) :
@[simp]
theorem category_theory.free_bicategory.mk_associator_inv {B : Type u} [quiver B] {a b c d : category_theory.free_bicategory B} (f : a b) (g : b c) (h : c d) :
@[simp]
theorem category_theory.free_bicategory.of_obj {B : Type u} [quiver B] (a : B) :
@[simp]
theorem category_theory.free_bicategory.of_map {B : Type u} [quiver B] (a b : B) (f : a b) :

Canonical prefunctor from B to free_bicategory B.

Equations
@[simp]
def category_theory.free_bicategory.lift_hom {B : Type u₁} [quiver B] {C : Type u₂} (F : B ⥤q C) {a b : B} :
(F.obj a F.obj b)

Auxiliary definition for lift.

Equations
@[simp]
theorem category_theory.free_bicategory.lift_hom_id {B : Type u₁} [quiver B] {C : Type u₂} (F : B ⥤q C)  :
= 𝟙 (F.obj a)
@[simp]
theorem category_theory.free_bicategory.lift_hom_comp {B : Type u₁} [quiver B] {C : Type u₂} (F : B ⥤q C) {a b c : category_theory.free_bicategory B} (f : a b) (g : b c) :
@[simp]
def category_theory.free_bicategory.lift_hom₂ {B : Type u₁} [quiver B] {C : Type u₂} (F : B ⥤q C) {a b : B} {f g : b} :

Auxiliary definition for lift.

Equations
theorem category_theory.free_bicategory.lift_hom₂_congr {B : Type u₁} [quiver B] {C : Type u₂} (F : B ⥤q C) {a b : B} {f g : b} {η θ : g}  :
@[simp]
theorem category_theory.free_bicategory.lift_map {B : Type u₁} [quiver B] {C : Type u₂} (F : B ⥤q C) (a b : category_theory.free_bicategory B)  :
@[simp]
theorem category_theory.free_bicategory.lift_obj {B : Type u₁} [quiver B] {C : Type u₂} (F : B ⥤q C) (ᾰ : B) :
= F.obj
@[simp]
theorem category_theory.free_bicategory.lift_map₂ {B : Type u₁} [quiver B] {C : Type u₂} (F : B ⥤q C) (a b : category_theory.free_bicategory B) (f g : a b) (a_1 : quot (λ (η θ : , ) :
= quot.lift _ a_1
@[simp]
theorem category_theory.free_bicategory.lift_map_comp {B : Type u₁} [quiver B] {C : Type u₂} (F : B ⥤q C) (a b c : category_theory.free_bicategory B) (f : a b) (g : b c) :
def category_theory.free_bicategory.lift {B : Type u₁} [quiver B] {C : Type u₂} (F : B ⥤q C) :

A prefunctor from a quiver B to a bicategory C can be lifted to a pseudofunctor from free_bicategory B to C.

Equations
@[simp]
theorem category_theory.free_bicategory.lift_map_id {B : Type u₁} [quiver B] {C : Type u₂} (F : B ⥤q C)  :