# Bicategorical composition `⊗≫` (composition up to associators) #

We provide `f ⊗≫ g`, the `bicategoricalComp` operation, which automatically inserts associators and unitors as needed to make the target of `f` match the source of `g`.

source
class CategoryTheory.BicategoricalCoherence {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) :
Type w

A typeclass carrying a choice of bicategorical structural isomorphism between two objects. Used by the `⊗≫` bicategorical composition operator, and the `coherence` tactic.

- iso : f ≅ g

  The chosen structural isomorphism between to 1-morphisms.

Instances

source
def CategoryTheory.Bicategory.«term⊗𝟙» :
Lean.ParserDescr

Notation for identities up to unitors and associators.

Equations

- CategoryTheory.Bicategory.«term⊗𝟙» = Lean.ParserDescr.node `CategoryTheory.Bicategory.«term⊗𝟙» 1024 (Lean.ParserDescr.symbol " ⊗𝟙 ")

Instances For

source
@[reducible, inline]
abbrev CategoryTheory.bicategoricalIso {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
f ≅ g

Construct an isomorphism between two objects in a bicategorical category out of unitors and associators.

Equations

- CategoryTheory.bicategoricalIso f g = CategoryTheory.BicategoricalCoherence.iso

Instances For

source
def CategoryTheory.bicategoricalComp {B : Type u} [Bicategory B] {a b : B} {f g h i : a ⟶ b} [BicategoricalCoherence g h] (η : f ⟶ g) (θ : h ⟶ i) :
f ⟶ i

Compose two morphisms in a bicategorical category, inserting unitors and associators between as necessary.

Equations

- CategoryTheory.bicategoricalComp η θ = CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp CategoryTheory.BicategoricalCoherence.iso.hom θ)

Instances For

source
def CategoryTheory.Bicategory.«term_⊗≫_» :
Lean.TrailingParserDescr

Compose two morphisms in a bicategorical category, inserting unitors and associators between as necessary.

Equations

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

Instances For

source
def CategoryTheory.bicategoricalIsoComp {B : Type u} [Bicategory B] {a b : B} {f g h i : a ⟶ b} [BicategoricalCoherence g h] (η : f ≅ g) (θ : h ≅ i) :
f ≅ i

Compose two isomorphisms in a bicategorical category, inserting unitors and associators between as necessary.

Equations

- CategoryTheory.bicategoricalIsoComp η θ = η ≪≫ CategoryTheory.BicategoricalCoherence.iso ≪≫ θ

Instances For

source
def CategoryTheory.Bicategory.«term_≪⊗≫_» :
Lean.TrailingParserDescr

Compose two isomorphisms in a bicategorical category, inserting unitors and associators between as necessary.

Equations

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

Instances For

source
instance CategoryTheory.BicategoricalCoherence.refl {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) :
BicategoricalCoherence f f
Equations

- CategoryTheory.BicategoricalCoherence.refl f = { iso := CategoryTheory.Iso.refl f }

source
@[simp]
theorem CategoryTheory.BicategoricalCoherence.refl_iso {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) :
iso = Iso.refl f
source
instance CategoryTheory.BicategoricalCoherence.whiskerLeft {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) (g h : b ⟶ c) [BicategoricalCoherence g h] :
BicategoricalCoherence (CategoryStruct.comp f g) (CategoryStruct.comp f h)
Equations

- CategoryTheory.BicategoricalCoherence.whiskerLeft f g h = { iso := CategoryTheory.Bicategory.whiskerLeftIso f CategoryTheory.BicategoricalCoherence.iso }

source
@[simp]
theorem CategoryTheory.BicategoricalCoherence.whiskerLeft_iso {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) (g h : b ⟶ c) [BicategoricalCoherence g h] :
iso = Bicategory.whiskerLeftIso f iso
source
instance CategoryTheory.BicategoricalCoherence.whiskerRight {B : Type u} [Bicategory B] {a b c : B} (f g : a ⟶ b) (h : b ⟶ c) [BicategoricalCoherence f g] :
BicategoricalCoherence (CategoryStruct.comp f h) (CategoryStruct.comp g h)
Equations

- CategoryTheory.BicategoricalCoherence.whiskerRight f g h = { iso := CategoryTheory.Bicategory.whiskerRightIso CategoryTheory.BicategoricalCoherence.iso h }

source
@[simp]
theorem CategoryTheory.BicategoricalCoherence.whiskerRight_iso {B : Type u} [Bicategory B] {a b c : B} (f g : a ⟶ b) (h : b ⟶ c) [BicategoricalCoherence f g] :
iso = Bicategory.whiskerRightIso iso h
source
instance CategoryTheory.BicategoricalCoherence.tensorRight {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [BicategoricalCoherence (CategoryStruct.id b) g] :
BicategoricalCoherence f (CategoryStruct.comp f g)
Equations

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

source
@[simp]
theorem CategoryTheory.BicategoricalCoherence.tensorRight_iso {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [BicategoricalCoherence (CategoryStruct.id b) g] :
iso = (Bicategory.rightUnitor f).symm ≪≫ Bicategory.whiskerLeftIso f iso
source
instance CategoryTheory.BicategoricalCoherence.tensorRight' {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [BicategoricalCoherence g (CategoryStruct.id b)] :
BicategoricalCoherence (CategoryStruct.comp f g) f
Equations

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

source
@[simp]
theorem CategoryTheory.BicategoricalCoherence.tensorRight'_iso {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [BicategoricalCoherence g (CategoryStruct.id b)] :
iso = Bicategory.whiskerLeftIso f iso ≪≫ Bicategory.rightUnitor f
source
instance CategoryTheory.BicategoricalCoherence.left {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
BicategoricalCoherence (CategoryStruct.comp (CategoryStruct.id a) f) g
Equations

- CategoryTheory.BicategoricalCoherence.left f g = { iso := CategoryTheory.Bicategory.leftUnitor f ≪≫ CategoryTheory.BicategoricalCoherence.iso }

source
@[simp]
theorem CategoryTheory.BicategoricalCoherence.left_iso {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
iso = Bicategory.leftUnitor f ≪≫ iso
source
instance CategoryTheory.BicategoricalCoherence.left' {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
BicategoricalCoherence f (CategoryStruct.comp (CategoryStruct.id a) g)
Equations

- CategoryTheory.BicategoricalCoherence.left' f g = { iso := CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.leftUnitor g).symm }

source
@[simp]
theorem CategoryTheory.BicategoricalCoherence.left'_iso {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
iso = iso ≪≫ (Bicategory.leftUnitor g).symm
source
instance CategoryTheory.BicategoricalCoherence.right {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
BicategoricalCoherence (CategoryStruct.comp f (CategoryStruct.id b)) g
Equations

- CategoryTheory.BicategoricalCoherence.right f g = { iso := CategoryTheory.Bicategory.rightUnitor f ≪≫ CategoryTheory.BicategoricalCoherence.iso }

source
@[simp]
theorem CategoryTheory.BicategoricalCoherence.right_iso {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
iso = Bicategory.rightUnitor f ≪≫ iso
source
instance CategoryTheory.BicategoricalCoherence.right' {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
BicategoricalCoherence f (CategoryStruct.comp g (CategoryStruct.id b))
Equations

- CategoryTheory.BicategoricalCoherence.right' f g = { iso := CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.rightUnitor g).symm }

source
@[simp]
theorem CategoryTheory.BicategoricalCoherence.right'_iso {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
iso = iso ≪≫ (Bicategory.rightUnitor g).symm
source
instance CategoryTheory.BicategoricalCoherence.assoc {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [BicategoricalCoherence (CategoryStruct.comp f (CategoryStruct.comp g h)) i] :
BicategoricalCoherence (CategoryStruct.comp (CategoryStruct.comp f g) h) i
Equations

- CategoryTheory.BicategoricalCoherence.assoc f g h i = { iso := CategoryTheory.Bicategory.associator f g h ≪≫ CategoryTheory.BicategoricalCoherence.iso }

source
@[simp]
theorem CategoryTheory.BicategoricalCoherence.assoc_iso {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [BicategoricalCoherence (CategoryStruct.comp f (CategoryStruct.comp g h)) i] :
iso = Bicategory.associator f g h ≪≫ iso
source
instance CategoryTheory.BicategoricalCoherence.assoc' {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [BicategoricalCoherence i (CategoryStruct.comp f (CategoryStruct.comp g h))] :
BicategoricalCoherence i (CategoryStruct.comp (CategoryStruct.comp f g) h)
Equations

- CategoryTheory.BicategoricalCoherence.assoc' f g h i = { iso := CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.associator f g h).symm }

source
@[simp]
theorem CategoryTheory.BicategoricalCoherence.assoc'_iso {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [BicategoricalCoherence i (CategoryStruct.comp f (CategoryStruct.comp g h))] :
iso = iso ≪≫ (Bicategory.associator f g h).symm
source
@[simp]
theorem CategoryTheory.bicategoricalComp_refl {B : Type u} [Bicategory B] {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) :
bicategoricalComp η θ = CategoryStruct.comp η θ