Mathlib.CategoryTheory.Bicategory.Basic

CategoryTheory.Bicategory structure

(B : Type u) extends CategoryStruct.{v} B

Full source

/-- In a bicategory, we can compose the 1-morphisms `f : a ⟶ b` and `g : b ⟶ c` to obtain
a 1-morphism `f ≫ g : a ⟶ c`. This composition does not need to be strictly associative,
but there is a specified associator, `α_ f g h : (f ≫ g) ≫ h ≅ f ≫ (g ≫ h)`.
There is an identity 1-morphism `𝟙 a : a ⟶ a`, with specified left and right unitor
isomorphisms `λ_ f : 𝟙 a ≫ f ≅ f` and `ρ_ f : f ≫ 𝟙 a ≅ f`.
These associators and unitors satisfy the pentagon and triangle equations.

See https://ncatlab.org/nlab/show/bicategory.
-/
@[nolint checkUnivs]
class Bicategory (B : Type u) extends CategoryStruct.{v} B where
  /-- The category structure on the collection of 1-morphisms -/
  homCategory : ∀ a b : B, Category.{w} (a ⟶ b) := by infer_instance
  /-- Left whiskering for morphisms -/
  whiskerLeft {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) : f ≫ gf ≫ g ⟶ f ≫ h
  /-- Right whiskering for morphisms -/
  whiskerRight {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) : f ≫ hf ≫ h ⟶ g ≫ h
  /-- The associator isomorphism: `(f ≫ g) ≫ h ≅ f ≫ g ≫ h` -/
  associator {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : (f ≫ g) ≫ h(f ≫ g) ≫ h ≅ f ≫ g ≫ h
  /-- The left unitor: `𝟙 a ≫ f ≅ f` -/
  leftUnitor {a b : B} (f : a ⟶ b) : 𝟙𝟙 a ≫ f𝟙 a ≫ f ≅ f
  /-- The right unitor: `f ≫ 𝟙 b ≅ f` -/
  rightUnitor {a b : B} (f : a ⟶ b) : f ≫ 𝟙 bf ≫ 𝟙 b ≅ f
  -- axioms for left whiskering:
  whiskerLeft_id : ∀ {a b c} (f : a ⟶ b) (g : b ⟶ c), whiskerLeft f (𝟙 g) = 𝟙 (f ≫ g) := by
    aesop_cat
  whiskerLeft_comp :
    ∀ {a b c} (f : a ⟶ b) {g h i : b ⟶ c} (η : g ⟶ h) (θ : h ⟶ i),
      whiskerLeft f (η ≫ θ) = whiskerLeft f η ≫ whiskerLeft f θ := by
    aesop_cat
  id_whiskerLeft :
    ∀ {a b} {f g : a ⟶ b} (η : f ⟶ g),
      whiskerLeft (𝟙 a) η = (leftUnitor f).hom ≫ η ≫ (leftUnitor g).inv := by
    aesop_cat
  comp_whiskerLeft :
    ∀ {a b c d} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
      whiskerLeft (f ≫ g) η =
        (associator f g h).hom ≫ whiskerLeft f (whiskerLeft g η) ≫ (associator f g h').inv := by
    aesop_cat
  -- axioms for right whiskering:
  id_whiskerRight : ∀ {a b c} (f : a ⟶ b) (g : b ⟶ c), whiskerRight (𝟙 f) g = 𝟙 (f ≫ g) := by
    aesop_cat
  comp_whiskerRight :
    ∀ {a b c} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c),
      whiskerRight (η ≫ θ) i = whiskerRight η i ≫ whiskerRight θ i := by
    aesop_cat
  whiskerRight_id :
    ∀ {a b} {f g : a ⟶ b} (η : f ⟶ g),
      whiskerRight η (𝟙 b) = (rightUnitor f).hom ≫ η ≫ (rightUnitor g).inv := by
    aesop_cat
  whiskerRight_comp :
    ∀ {a b c d} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
      whiskerRight η (g ≫ h) =
        (associator f g h).inv ≫ whiskerRight (whiskerRight η g) h ≫ (associator f' g h).hom := by
    aesop_cat
  -- associativity of whiskerings:
  whisker_assoc :
    ∀ {a b c d} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
      whiskerRight (whiskerLeft f η) h =
        (associator f g h).hom ≫ whiskerLeft f (whiskerRight η h) ≫ (associator f g' h).inv := by
    aesop_cat
  -- exchange law of left and right whiskerings:
  whisker_exchange :
    ∀ {a b c} {f g : a ⟶ b} {h i : b ⟶ c} (η : f ⟶ g) (θ : h ⟶ i),
      whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ := by
    aesop_cat
  -- pentagon identity:
  pentagon :
    ∀ {a b c d e} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
      whiskerRight (associator f g h).hom i ≫
          (associator f (g ≫ h) i).hom ≫ whiskerLeft f (associator g h i).hom =
        (associator (f ≫ g) h i).hom ≫ (associator f g (h ≫ i)).hom := by
    aesop_cat
  -- triangle identity:
  triangle :
    ∀ {a b c} (f : a ⟶ b) (g : b ⟶ c),
      (associator f (𝟙 b) g).hom ≫ whiskerLeft f (leftUnitor g).hom
      = whiskerRight (rightUnitor f).hom g := by
    aesop_cat

Bicategory

Informal description

A bicategory $\mathcal{B}$ consists of: - Objects $a, b, c, \ldots$ in $\mathcal{B}$, - 1-morphisms $f : a \to b$ between objects, and - 2-morphisms $\eta : f \Rightarrow g$ between parallel 1-morphisms $f, g : a \to b$. The bicategory structure includes: - A composition operation $\circ$ for 1-morphisms (with $f \circ g : a \to c$ for $f : a \to b$ and $g : b \to c$), - An identity 1-morphism $\text{id}_a : a \to a$ for each object $a$, - For each pair of objects $(a, b)$, the 1-morphisms $a \to b$ form a category whose morphisms are the 2-morphisms, - Whiskering operations: for a 1-morphism $f$ and a 2-morphism $\eta$, we have left whiskering $f \triangleleft \eta$ and right whiskering $\eta \triangleright f$, - An associator natural isomorphism $\alpha_{f,g,h} : (f \circ g) \circ h \cong f \circ (g \circ h)$, - Left and right unitor natural isomorphisms $\lambda_f : \text{id}_a \circ f \cong f$ and $\rho_f : f \circ \text{id}_b \cong f$, satisfying the pentagon and triangle coherence conditions.

CategoryTheory.Bicategory.term_◁_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] scoped infixr:81 " ◁ " => Bicategory.whiskerLeft

Left whiskering in a bicategory

Informal description

The notation `◁` represents the left whiskering operation in a bicategory. For a 1-morphism `f : a ⟶ b` and a 2-morphism `η : g ⟶ h` between 1-morphisms `g, h : b ⟶ c`, the left whiskering `f ◁ η` is the 2-morphism `f ≫ g ⟶ f ≫ h`.

CategoryTheory.Bicategory.term_▷_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] scoped infixl:81 " ▷ " => Bicategory.whiskerRight

Right whiskering in bicategories

Informal description

The operator `▷` represents right whiskering in a bicategory. Given a 2-morphism $\eta : f \to g$ between 1-morphisms $f, g : a \to b$ and a 1-morphism $h : b \to c$, the right whiskering $\eta ▷ h$ is a 2-morphism $f ≫ h \to g ≫ h$ between the composed 1-morphisms. This operation satisfies the exchange law with left whiskering.

CategoryTheory.Bicategory.termα_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] scoped notation "α_" => Bicategory.associator

Associator notation in bicategories

Informal description

The notation `α_` is used to represent the associator in a bicategory, which is a natural isomorphism between the two ways of composing three 1-morphisms: `(f ≫ g) ≫ h` and `f ≫ (g ≫ h)`.

CategoryTheory.Bicategory.termλ_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] scoped notation "λ_" => Bicategory.leftUnitor

Left unitor notation in bicategories

Informal description

The notation `λ_` represents the left unitor 2-morphism in a bicategory, which is a natural isomorphism between the composite of the identity 1-morphism and another 1-morphism, and the 1-morphism itself. Specifically, for any 1-morphism `f : a ⟶ b` in a bicategory, `λ_f : 𝟙 a ≫ f ≅ f` is the left unitor isomorphism.

CategoryTheory.Bicategory.termρ_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] scoped notation "ρ_" => Bicategory.rightUnitor

Right unitor notation in bicategories

Informal description

The notation `ρ_` represents the right unitor 2-morphism in a bicategory, which is a natural isomorphism between the composition of a 1-morphism with the identity 1-morphism and the original 1-morphism. Specifically, for any 1-morphism `f : a ⟶ b`, `ρ_f : f ≫ 𝟙 b ≅ f` is the right unitor isomorphism.

CategoryTheory.Bicategory.whiskerLeft_hom_inv theorem

(f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) : f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)

Full source

@[reassoc (attr := simp)]
theorem whiskerLeft_hom_inv (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
    f ◁ η.homf ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g) := by rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]

Left Whiskering of Isomorphism Hom-Inverse Pair Yields Identity

Informal description

For any 1-morphism $f \colon a \to b$ in a bicategory $\mathcal{B}$, and any isomorphism $\eta \colon g \cong h$ between 1-morphisms $g, h \colon b \to c$, the composition of the left whiskering of $f$ with $\eta$'s homomorphism and the left whiskering of $f$ with $\eta$'s inverse is equal to the identity 2-morphism on the composite $f \circ g$. In symbols: $$ f \triangleleft \eta_{\text{hom}} \circ f \triangleleft \eta_{\text{inv}} = \text{id}_{f \circ g} $$

CategoryTheory.Bicategory.hom_inv_whiskerRight theorem

{f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) : η.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h)

Full source

@[reassoc (attr := simp)]
theorem hom_inv_whiskerRight {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
    η.hom ▷ hη.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h) := by rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]

Right whiskering preserves isomorphism composition in bicategories

Informal description

For any isomorphism $\eta \colon f \cong g$ between 1-morphisms $f, g \colon a \to b$ in a bicategory, and for any 1-morphism $h \colon b \to c$, the composition of the right whiskering of $\eta.\text{hom}$ with $h$ followed by the right whiskering of $\eta.\text{inv}$ with $h$ equals the identity 2-morphism on $f \circ h$. In symbols: \[ (\eta.\text{hom} \triangleright h) \circ (\eta.\text{inv} \triangleright h) = \text{id}_{f \circ h} \]

CategoryTheory.Bicategory.whiskerLeft_inv_hom theorem

(f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) : f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)

Full source

@[reassoc (attr := simp)]
theorem whiskerLeft_inv_hom (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
    f ◁ η.invf ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h) := by rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]

Left Whiskering of Isomorphism Inverse and Hom Satisfies Identity

Informal description

In a bicategory $\mathcal{B}$, for any 1-morphism $f : a \to b$ and any isomorphism $\eta : g \cong h$ between 1-morphisms $g, h : b \to c$, the composition of the left whiskering of the inverse of $\eta$ with the left whiskering of $\eta$ itself equals the identity 2-morphism on $f \circ g$. That is, \[ f \triangleleft \eta^{-1} \circ f \triangleleft \eta = \text{id}_{f \circ g}. \]

CategoryTheory.Bicategory.inv_hom_whiskerRight theorem

{f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) : η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h)

Full source

@[reassoc (attr := simp)]
theorem inv_hom_whiskerRight {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
    η.inv ▷ hη.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h) := by rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]

Composition of Whiskered Isomorphism Components Yields Identity

Informal description

For any 1-morphisms $f, g : a \to b$ in a bicategory $\mathcal{B}$, given an isomorphism $\eta : f \cong g$ and any 1-morphism $h : b \to c$, the composition of the right whiskering of the inverse of $\eta$ with $h$ followed by the right whiskering of the forward morphism of $\eta$ with $h$ equals the identity 2-morphism on $g \circ h$. That is, $(\eta^{-1} \triangleright h) \circ (\eta \triangleright h) = \text{id}_{g \circ h}$.

CategoryTheory.Bicategory.whiskerLeftIso definition

(f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) : f ≫ g ≅ f ≫ h

Full source

/-- The left whiskering of a 2-isomorphism is a 2-isomorphism. -/
@[simps]
def whiskerLeftIso (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) : f ≫ gf ≫ g ≅ f ≫ h where
  hom := f ◁ η.hom
  inv := f ◁ η.inv

Left whiskering of a 2-isomorphism

Informal description

Given a bicategory $\mathcal{B}$, for any 1-morphism $f : a \to b$ and any isomorphism $\eta : g \cong h$ between 1-morphisms $g, h : b \to c$, the left whiskering operation constructs an isomorphism $f \circ g \cong f \circ h$ whose forward morphism is $f \triangleleft \eta_\text{hom}$ and whose inverse morphism is $f \triangleleft \eta_\text{inv}$.

CategoryTheory.Bicategory.whiskerLeft_isIso instance

(f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) [IsIso η] : IsIso (f ◁ η)

Full source

instance whiskerLeft_isIso (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) [IsIso η] : IsIso (f ◁ η) :=
  (whiskerLeftIso f (asIso η)).isIso_hom

Left Whiskering Preserves Isomorphisms

Informal description

For any 1-morphism $f \colon a \to b$ in a bicategory $\mathcal{B}$, and any 2-morphism $\eta \colon g \to h$ between 1-morphisms $g, h \colon b \to c$, if $\eta$ is an isomorphism, then the left whiskering $f \triangleleft \eta$ is also an isomorphism.

CategoryTheory.Bicategory.inv_whiskerLeft theorem

(f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) [IsIso η] : inv (f ◁ η) = f ◁ inv η

Full source

@[simp]
theorem inv_whiskerLeft (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) [IsIso η] :
    inv (f ◁ η) = f ◁ inv η := by
  apply IsIso.inv_eq_of_hom_inv_id
  simp only [← whiskerLeft_comp, whiskerLeft_id, IsIso.hom_inv_id]

Inverse of Left Whiskering Equals Left Whiskering of Inverse

Informal description

In a bicategory $\mathcal{B}$, for any 1-morphism $f \colon a \to b$ and any isomorphism $\eta \colon g \to h$ between 1-morphisms $g, h \colon b \to c$, the inverse of the left whiskering $f \triangleleft \eta$ is equal to the left whiskering of $f$ with the inverse of $\eta$, i.e., $$(f \triangleleft \eta)^{-1} = f \triangleleft \eta^{-1}.$$

CategoryTheory.Bicategory.whiskerRightIso definition

{f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) : f ≫ h ≅ g ≫ h

Full source

/-- The right whiskering of a 2-isomorphism is a 2-isomorphism. -/
@[simps!]
def whiskerRightIso {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) : f ≫ hf ≫ h ≅ g ≫ h where
  hom := η.hom ▷ h
  inv := η.inv ▷ h

Right whiskering of a 2-isomorphism with a 1-morphism

Informal description

Given an isomorphism $\eta \colon f \cong g$ between 1-morphisms $f, g \colon a \to b$ in a bicategory $\mathcal{B}$, and a 1-morphism $h \colon b \to c$, the right whiskering of $\eta$ with $h$ yields an isomorphism $\eta \triangleright h \colon f \circ h \cong g \circ h$ between the composite 1-morphisms. Here, $\eta \triangleright h$ is defined by applying the right whiskering operation to both the forward and backward components of $\eta$.

CategoryTheory.Bicategory.whiskerRight_isIso instance

{f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [IsIso η] : IsIso (η ▷ h)

Full source

instance whiskerRight_isIso {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [IsIso η] : IsIso (η ▷ h) :=
  (whiskerRightIso (asIso η) h).isIso_hom

Right Whiskering Preserves Isomorphisms

Informal description

Given a 2-morphism $\eta \colon f \Rightarrow g$ between 1-morphisms $f, g \colon a \to b$ in a bicategory $\mathcal{B}$, if $\eta$ is an isomorphism, then for any 1-morphism $h \colon b \to c$, the right whiskering $\eta \triangleright h \colon f \circ h \Rightarrow g \circ h$ is also an isomorphism.

CategoryTheory.Bicategory.inv_whiskerRight theorem

{f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [IsIso η] : inv (η ▷ h) = inv η ▷ h

Full source

@[simp]
theorem inv_whiskerRight {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [IsIso η] :
    inv (η ▷ h) = invinv η ▷ h := by
  apply IsIso.inv_eq_of_hom_inv_id
  simp only [← comp_whiskerRight, id_whiskerRight, IsIso.hom_inv_id]

Inverse of Right Whiskering Equals Whiskering of Inverse

Informal description

Given a 2-morphism $\eta \colon f \Rightarrow g$ between 1-morphisms $f, g \colon a \to b$ in a bicategory $\mathcal{B}$, if $\eta$ is an isomorphism, then for any 1-morphism $h \colon b \to c$, the inverse of the right whiskering $\eta \triangleright h$ is equal to the right whiskering of the inverse $\eta^{-1} \triangleright h$. That is, $(\eta \triangleright h)^{-1} = \eta^{-1} \triangleright h$.

CategoryTheory.Bicategory.pentagon_inv theorem

 (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
  f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i = (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv

Full source

@[reassoc (attr := simp)]
theorem pentagon_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    f ◁ (α_ g h i).invf ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i =
      (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv :=
  eq_of_inv_eq_inv (by simp)

Inverse Pentagon Identity in Bicategories

Informal description

In a bicategory $\mathcal{B}$, for any 1-morphisms $f \colon a \to b$, $g \colon b \to c$, $h \colon c \to d$, and $i \colon d \to e$, the following equation holds: $$f \triangleleft \alpha_{g,h,i}^{-1} \circ \alpha_{f,g \circ h,i}^{-1} \circ \alpha_{f,g,h}^{-1} \triangleright i = \alpha_{f,g,h \circ i}^{-1} \circ \alpha_{f \circ g,h,i}^{-1},$$ where $\alpha$ denotes the associator isomorphism and $\circ$ denotes vertical composition of 2-morphisms.

CategoryTheory.Bicategory.pentagon_inv_inv_hom_hom_inv theorem

 (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
  (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom = f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv

Full source

@[reassoc (attr := simp)]
theorem pentagon_inv_inv_hom_hom_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom =
    f ◁ (α_ g h i).homf ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv := by
  rw [← cancel_epi (f ◁ (α_ g h i).inv), ← cancel_mono (α_ (f ≫ g) h i).inv]
  simp

Inverse-Hom Pentagon Identity in Bicategories

Informal description

For any 1-morphisms $f \colon a \to b$, $g \colon b \to c$, $h \colon c \to d$, and $i \colon d \to e$ in a bicategory $\mathcal{B}$, the following equation holds: $$(\alpha_{f,g \circ h,i})^{-1} \circ (\alpha_{f,g,h})^{-1} \triangleright i \circ \alpha_{f \circ g,h,i} = f \triangleleft \alpha_{g,h,i} \circ (\alpha_{f,g,h \circ i})^{-1},$$ where $\alpha$ denotes the associator isomorphism and $\circ$ denotes vertical composition of 2-morphisms.

CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_inv theorem

 (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
  (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom = (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv

Full source

@[reassoc (attr := simp)]
theorem pentagon_inv_hom_hom_hom_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom =
      (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv :=
  eq_of_inv_eq_inv (by simp)

Inverse-Hom Pentagon Identity in Bicategories (Inv-Hom-Hom-Hom-Inv Form)

Informal description

For any 1-morphisms $f \colon a \to b$, $g \colon b \to c$, $h \colon c \to d$, and $i \colon d \to e$ in a bicategory $\mathcal{B}$, the following equation holds: $$(\alpha_{f \circ g,h,i})^{-1} \circ \alpha_{f,g,h} \triangleright i \circ \alpha_{f,g \circ h,i} = \alpha_{f,g,h \circ i} \circ f \triangleleft \alpha_{g,h,i}^{-1},$$ where $\alpha$ denotes the associator isomorphism and $\circ$ denotes vertical composition of 2-morphisms.

CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_inv theorem

 (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
  f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv = (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i

Full source

@[reassoc (attr := simp)]
theorem pentagon_hom_inv_inv_inv_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    f ◁ (α_ g h i).homf ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv =
      (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i := by
  simp [← cancel_epi (f ◁ (α_ g h i).inv)]

Pentagon Identity for Associators in Bicategories (Hom-Inv-Inv-Inv-Inv Form)

Informal description

In a bicategory $\mathcal{B}$, for any 1-morphisms $f \colon a \to b$, $g \colon b \to c$, $h \colon c \to d$, and $i \colon d \to e$, the following equation holds: $$f \triangleleft \alpha_{g,h,i} \circ \alpha_{f,g,h \circ i}^{-1} \circ \alpha_{f \circ g,h,i}^{-1} = \alpha_{f,g \circ h,i}^{-1} \circ \alpha_{f,g,h}^{-1} \triangleright i,$$ where $\alpha$ denotes the associator isomorphism, $\circ$ denotes vertical composition of 2-morphisms, and $\triangleleft$, $\triangleright$ denote left and right whiskering respectively.

CategoryTheory.Bicategory.pentagon_hom_hom_inv_hom_hom theorem

 (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
  (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv = (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom

Full source

@[reassoc (attr := simp)]
theorem pentagon_hom_hom_inv_hom_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv =
      (α_ f g h).hom ▷ i(α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom :=
  eq_of_inv_eq_inv (by simp)

Pentagon Identity for Bicategories (Hom-Hom-Inv-Hom-Hom Version)

Informal description

For any 1-morphisms $f \colon a \to b$, $g \colon b \to c$, $h \colon c \to d$, and $i \colon d \to e$ in a bicategory $\mathcal{B}$, the following pentagon identity holds: \[ \alpha_{f \circ g,h,i} \circ \alpha_{f,g,h \circ i} \circ f \triangleleft \alpha_{g,h,i}^{-1} = \alpha_{f,g,h} \triangleright i \circ \alpha_{f,g \circ h,i}, \] where: - $\alpha_{x,y,z}$ denotes the associator isomorphism $(x \circ y) \circ z \cong x \circ (y \circ z)$, - $\circ$ denotes vertical composition of 2-morphisms, - $\triangleright$ denotes right whiskering of a 2-morphism by a 1-morphism, - $\triangleleft$ denotes left whiskering of a 2-morphism by a 1-morphism.

CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_hom theorem

 (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
  (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv = (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i

Full source

@[reassoc (attr := simp)]
theorem pentagon_hom_inv_inv_inv_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv =
    (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i := by
  rw [← cancel_epi (α_ f g (h ≫ i)).inv, ← cancel_mono ((α_ f g h).inv ▷ i)]
  simp

Pentagon Identity for Bicategories (Hom-Inv-Inv-Inv-Hom Version)

Informal description

For any 1-morphisms $f \colon a \to b$, $g \colon b \to c$, $h \colon c \to d$, and $i \colon d \to e$ in a bicategory $\mathcal{B}$, the following pentagon identity holds: \[ \alpha_{f,g,h \circ i} \circ f \triangleleft \alpha_{g,h,i}^{-1} \circ \alpha_{f,g \circ h,i}^{-1} = \alpha_{f \circ g,h,i}^{-1} \circ \alpha_{f,g,h} \triangleright i \] where: - $\alpha_{x,y,z}$ denotes the associator isomorphism $(x \circ y) \circ z \cong x \circ (y \circ z)$, - $\circ$ denotes vertical composition of 2-morphisms, - $\triangleright$ denotes right whiskering of a 2-morphism by a 1-morphism, - $\triangleleft$ denotes left whiskering of a 2-morphism by a 1-morphism.

CategoryTheory.Bicategory.pentagon_hom_hom_inv_inv_hom theorem

 (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
  (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv = (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom

Full source

@[reassoc (attr := simp)]
theorem pentagon_hom_hom_inv_inv_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv =
      (α_ f g h).inv ▷ i(α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom :=
  eq_of_inv_eq_inv (by simp)

Pentagon Identity for Bicategories (Hom-Hom-Inv-Inv-Hom Version)

Informal description

For any 1-morphisms $f \colon a \to b$, $g \colon b \to c$, $h \colon c \to d$, and $i \colon d \to e$ in a bicategory $\mathcal{B}$, the following pentagon identity holds: \[ \alpha_{f,g \circ h,i} \circ f \triangleleft \alpha_{g,h,i} \circ \alpha_{f,g,h \circ i}^{-1} = \alpha_{f,g,h}^{-1} \triangleright i \circ \alpha_{f \circ g,h,i} \] where: - $\alpha_{x,y,z}$ denotes the associator isomorphism $(x \circ y) \circ z \cong x \circ (y \circ z)$, - $\circ$ denotes vertical composition of 2-morphisms, - $\triangleright$ denotes right whiskering of a 2-morphism by a 1-morphism, - $\triangleleft$ denotes left whiskering of a 2-morphism by a 1-morphism.

CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_hom theorem

 (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
  (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom = (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom

Full source

@[reassoc (attr := simp)]
theorem pentagon_inv_hom_hom_hom_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ f g h).inv ▷ i(α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom =
      (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom := by
  simp [← cancel_epi ((α_ f g h).hom ▷ i)]

Pentagon Identity for Bicategories (Inverse-Hom-Hom-Hom-Hom Version)

Informal description

For any 1-morphisms $f \colon a \to b$, $g \colon b \to c$, $h \colon c \to d$, and $i \colon d \to e$ in a bicategory $\mathcal{B}$, the following pentagon identity holds: \[ (\alpha_{f,g,h})^{-1} \triangleright i \circ \alpha_{f \circ g,h,i} \circ \alpha_{f,g,h \circ i} = \alpha_{f,g \circ h,i} \circ f \triangleleft \alpha_{g,h,i} \] where: - $\alpha_{x,y,z}$ denotes the associator isomorphism $(x \circ y) \circ z \cong x \circ (y \circ z)$, - $\circ$ denotes vertical composition of 2-morphisms, - $\triangleright$ denotes right whiskering of a 2-morphism by a 1-morphism, - $\triangleleft$ denotes left whiskering of a 2-morphism by a 1-morphism.

CategoryTheory.Bicategory.pentagon_inv_inv_hom_inv_inv theorem

 (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
  (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i = f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv

Full source

@[reassoc (attr := simp)]
theorem pentagon_inv_inv_hom_inv_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i =
      f ◁ (α_ g h i).invf ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv :=
  eq_of_inv_eq_inv (by simp)

Pentagon Identity for Bicategories (Inverse-Inverse-Hom-Inverse-Inverse Version)

Informal description

For any 1-morphisms $f \colon a \to b$, $g \colon b \to c$, $h \colon c \to d$, and $i \colon d \to e$ in a bicategory $\mathcal{B}$, the following pentagon identity holds: \[ \alpha_{f,g,h \circ i}^{-1} \circ \alpha_{f \circ g,h,i}^{-1} \circ (\alpha_{f,g,h} \triangleright i) = (f \triangleleft \alpha_{g,h,i}^{-1}) \circ \alpha_{f,g \circ h,i}^{-1} \] where: - $\alpha_{x,y,z}$ denotes the associator isomorphism $(x \circ y) \circ z \cong x \circ (y \circ z)$, - $\circ$ denotes vertical composition of 2-morphisms, - $\triangleright$ denotes right whiskering of a 2-morphism by a 1-morphism, - $\triangleleft$ denotes left whiskering of a 2-morphism by a 1-morphism.

CategoryTheory.Bicategory.triangle_assoc_comp_left theorem

(f : a ⟶ b) (g : b ⟶ c) : (α_ f (𝟙 b) g).hom ≫ f ◁ (λ_ g).hom = (ρ_ f).hom ▷ g

Full source

theorem triangle_assoc_comp_left (f : a ⟶ b) (g : b ⟶ c) :
    (α_ f (𝟙 b) g).hom ≫ f ◁ (λ_ g).hom = (ρ_ f).hom ▷ g :=
  triangle f g

Triangle Identity for Bicategories (Left Version)

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory $\mathcal{B}$, the following diagram commutes: \[ \alpha_{f, \text{id}_b, g} \circ (f \triangleleft \lambda_g) = \rho_f \triangleright g \] where: - $\alpha_{f, \text{id}_b, g} \colon (f \circ \text{id}_b) \circ g \cong f \circ (\text{id}_b \circ g)$ is the associator isomorphism, - $\lambda_g \colon \text{id}_b \circ g \cong g$ is the left unitor isomorphism, - $\rho_f \colon f \circ \text{id}_b \cong f$ is the right unitor isomorphism, - $\circ$ denotes horizontal composition of 1-morphisms, - $\triangleleft$ denotes left whiskering of a 2-morphism by a 1-morphism, - $\triangleright$ denotes right whiskering of a 2-morphism by a 1-morphism.

CategoryTheory.Bicategory.triangle_assoc_comp_right theorem

(f : a ⟶ b) (g : b ⟶ c) : (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom

Full source

@[reassoc (attr := simp)]
theorem triangle_assoc_comp_right (f : a ⟶ b) (g : b ⟶ c) :
    (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom := by rw [← triangle, inv_hom_id_assoc]

Triangle Identity for Bicategories (Right Version)

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory, the following equation holds between 2-morphisms: \[ \alpha_{f, \mathrm{id}_b, g}^{-1} \circ (\rho_f \triangleright g) = f \triangleleft \lambda_g \] where: - $\alpha_{f, \mathrm{id}_b, g}$ is the associator isomorphism for the composition $f \circ \mathrm{id}_b \circ g$, - $\rho_f$ is the right unitor isomorphism for $f$, - $\lambda_g$ is the left unitor isomorphism for $g$, - $\circ$ denotes vertical composition of 2-morphisms, and - $\triangleright$ and $\triangleleft$ denote right and left whiskering respectively.

CategoryTheory.Bicategory.triangle_assoc_comp_right_inv theorem

(f : a ⟶ b) (g : b ⟶ c) : (ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv

Full source

@[reassoc (attr := simp)]
theorem triangle_assoc_comp_right_inv (f : a ⟶ b) (g : b ⟶ c) :
    (ρ_ f).inv ▷ g(ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv := by
  simp [← cancel_mono (f ◁ (λ_ g).hom)]

Inverse Triangle Identity for Bicategories (Right Version)

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory $\mathcal{B}$, the following equation holds between 2-morphisms: \[ (\rho_f)^{-1} \triangleright g \circ \alpha_{f, \text{id}_b, g} = f \triangleleft (\lambda_g)^{-1} \] where: - $\rho_f$ is the right unitor isomorphism for $f$, - $\alpha_{f, \text{id}_b, g}$ is the associator isomorphism for the composition $f \circ \text{id}_b \circ g$, - $\lambda_g$ is the left unitor isomorphism for $g$, - $\circ$ denotes vertical composition of 2-morphisms, and - $\triangleright$ and $\triangleleft$ denote right and left whiskering respectively.

CategoryTheory.Bicategory.triangle_assoc_comp_left_inv theorem

(f : a ⟶ b) (g : b ⟶ c) : f ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g

Full source

@[reassoc (attr := simp)]
theorem triangle_assoc_comp_left_inv (f : a ⟶ b) (g : b ⟶ c) :
    f ◁ (λ_ g).invf ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g := by
  simp [← cancel_mono ((ρ_ f).hom ▷ g)]

Inverse Triangle Identity for Bicategories (Left Version)

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory, the following equation holds between 2-morphisms: \[ f \triangleleft \lambda_g^{-1} \circ \alpha_{f, \mathrm{id}_b, g}^{-1} = \rho_f^{-1} \triangleright g \] where: - $\lambda_g$ is the left unitor isomorphism for $g$, - $\alpha_{f, \mathrm{id}_b, g}$ is the associator isomorphism for the composition $f \circ \mathrm{id}_b \circ g$, - $\rho_f$ is the right unitor isomorphism for $f$, - $\circ$ denotes vertical composition of 2-morphisms, and - $\triangleleft$ and $\triangleright$ denote left and right whiskering respectively.

CategoryTheory.Bicategory.associator_naturality_left theorem

 {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) : η ▷ g ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h)

Full source

@[reassoc]
theorem associator_naturality_left {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
    η ▷ gη ▷ g ▷ hη ▷ g ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h) := by simp

Naturality of the associator with respect to left whiskering

Informal description

For any 2-morphism $\eta : f \Rightarrow f'$ between 1-morphisms $f, f' : a \to b$, and any 1-morphisms $g : b \to c$ and $h : c \to d$, the following diagram commutes: \[ (\eta \triangleright g) \triangleright h \circ \alpha_{f',g,h} = \alpha_{f,g,h} \circ \eta \triangleright (g \circ h) \] where $\alpha$ denotes the associator isomorphism and $\triangleright$ denotes right whiskering.

CategoryTheory.Bicategory.associator_inv_naturality_left theorem

 {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) : η ▷ (g ≫ h) ≫ (α_ f' g h).inv = (α_ f g h).inv ≫ η ▷ g ▷ h

Full source

@[reassoc]
theorem associator_inv_naturality_left {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
    η ▷ (g ≫ h)η ▷ (g ≫ h) ≫ (α_ f' g h).inv = (α_ f g h).inv ≫ η ▷ g ▷ h := by simp

Naturality of Inverse Associator with Respect to Left Whiskering

Informal description

For any 2-morphism $\eta : f \Rightarrow f'$ between 1-morphisms $f, f' : a \to b$, and any composable 1-morphisms $g : b \to c$ and $h : c \to d$, the following diagram commutes: \[ \eta \triangleright (g \circ h) \circ \alpha_{f',g,h}^{-1} = \alpha_{f,g,h}^{-1} \circ (\eta \triangleright g) \triangleright h \] where $\alpha_{f,g,h}^{-1} : f \circ (g \circ h) \Rightarrow (f \circ g) \circ h$ is the inverse associator isomorphism.

CategoryTheory.Bicategory.whiskerRight_comp_symm theorem

 {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) : η ▷ g ▷ h = (α_ f g h).hom ≫ η ▷ (g ≫ h) ≫ (α_ f' g h).inv

Full source

@[reassoc]
theorem whiskerRight_comp_symm {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
    η ▷ gη ▷ g ▷ h = (α_ f g h).hom ≫ η ▷ (g ≫ h) ≫ (α_ f' g h).inv := by simp

Symmetrized Right Whiskering via Associators

Informal description

For any 1-morphisms $f, f' \colon a \to b$, any 2-morphism $\eta \colon f \Rightarrow f'$, and any composable 1-morphisms $g \colon b \to c$ and $h \colon c \to d$ in a bicategory, the following equality holds: \[ \eta \triangleright g \triangleright h = \alpha_{f,g,h} \circ (\eta \triangleright (g \circ h)) \circ \alpha_{f',g,h}^{-1}, \] where $\alpha_{f,g,h} \colon (f \circ g) \circ h \cong f \circ (g \circ h)$ is the associator isomorphism, and $\triangleright$ denotes right whiskering.

CategoryTheory.Bicategory.associator_naturality_middle theorem

 (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) : (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ η ▷ h

Full source

@[reassoc]
theorem associator_naturality_middle (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) :
    (f ◁ η) ▷ h(f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ η ▷ h := by simp

Naturality of the associator with respect to middle whiskering

Informal description

For any 1-morphism $f \colon a \to b$, 2-morphism $\eta \colon g \to g'$ between 1-morphisms $g, g' \colon b \to c$, and 1-morphism $h \colon c \to d$ in a bicategory, the following diagram commutes: \[ (f \triangleleft \eta) \triangleright h \circ \alpha_{f,g',h} = \alpha_{f,g,h} \circ f \triangleleft (\eta \triangleright h) \] where $\alpha$ denotes the associator isomorphism.

CategoryTheory.Bicategory.associator_inv_naturality_middle theorem

 (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) : f ◁ η ▷ h ≫ (α_ f g' h).inv = (α_ f g h).inv ≫ (f ◁ η) ▷ h

Full source

@[reassoc]
theorem associator_inv_naturality_middle (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) :
    f ◁ η ▷ hf ◁ η ▷ h ≫ (α_ f g' h).inv = (α_ f g h).inv ≫ (f ◁ η) ▷ h := by simp

Naturality of the Associator Inverse with Middle Whiskering

Informal description

For any 1-morphism $f \colon a \to b$, 2-morphism $\eta \colon g \to g'$ between 1-morphisms $g, g' \colon b \to c$, and 1-morphism $h \colon c \to d$ in a bicategory $\mathcal{B}$, the following diagram commutes: \[ (f \triangleleft \eta) \triangleright h \circ \alpha_{f,g',h}^{-1} = \alpha_{f,g,h}^{-1} \circ (f \triangleleft \eta \triangleright h) \] where $\alpha_{f,g,h} \colon (f \circ g) \circ h \cong f \circ (g \circ h)$ is the associator isomorphism.

CategoryTheory.Bicategory.whisker_assoc_symm theorem

 (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) : f ◁ η ▷ h = (α_ f g h).inv ≫ (f ◁ η) ▷ h ≫ (α_ f g' h).hom

Full source

@[reassoc]
theorem whisker_assoc_symm (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) :
    f ◁ η ▷ h = (α_ f g h).inv ≫ (f ◁ η) ▷ h ≫ (α_ f g' h).hom := by simp

Whiskering-Associator Symmetry Relation in Bicategories

Informal description

For any 1-morphism $f \colon a \to b$, 2-morphism $\eta \colon g \to g'$ between 1-morphisms $g, g' \colon b \to c$, and 1-morphism $h \colon c \to d$ in a bicategory, the following equation holds: \[ f \triangleleft \eta \triangleright h = \alpha_{f,g,h}^{-1} \circ (f \triangleleft \eta) \triangleright h \circ \alpha_{f,g',h} \] where $\alpha$ denotes the associator isomorphism.

CategoryTheory.Bicategory.associator_naturality_right theorem

 (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') : (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ g ◁ η

Full source

@[reassoc]
theorem associator_naturality_right (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
    (f ≫ g) ◁ η(f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ g ◁ η := by simp

Naturality of the Associator with Respect to Right Whiskering

Informal description

For any 1-morphisms $f \colon a \to b$, $g \colon b \to c$, and 2-morphism $\eta \colon h \to h'$ between 1-morphisms $h, h' \colon c \to d$ in a bicategory $\mathcal{B}$, the following diagram commutes: \[ (f \circ g) \triangleleft \eta \circ \alpha_{f,g,h'} = \alpha_{f,g,h} \circ f \triangleleft (g \triangleleft \eta) \] where $\alpha_{f,g,h} \colon (f \circ g) \circ h \cong f \circ (g \circ h)$ is the associator isomorphism.

CategoryTheory.Bicategory.associator_inv_naturality_right theorem

 (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') : f ◁ g ◁ η ≫ (α_ f g h').inv = (α_ f g h).inv ≫ (f ≫ g) ◁ η

Full source

@[reassoc]
theorem associator_inv_naturality_right (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
    f ◁ g ◁ ηf ◁ g ◁ η ≫ (α_ f g h').inv = (α_ f g h).inv ≫ (f ≫ g) ◁ η := by simp

Naturality of the Associator Inverse with Respect to Right Whiskering

Informal description

For any 1-morphisms $f \colon a \to b$, $g \colon b \to c$, and any 2-morphism $\eta \colon h \Rightarrow h'$ between 1-morphisms $h, h' \colon c \to d$ in a bicategory $\mathcal{B}$, the following diagram commutes: \[ f \triangleleft (g \triangleleft \eta) \circ \alpha_{f,g,h'}^{-1} = \alpha_{f,g,h}^{-1} \circ ((f \circ g) \triangleleft \eta) \] where $\alpha_{f,g,h} \colon (f \circ g) \circ h \cong f \circ (g \circ h)$ is the associator isomorphism.

CategoryTheory.Bicategory.comp_whiskerLeft_symm theorem

 (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') : f ◁ g ◁ η = (α_ f g h).inv ≫ (f ≫ g) ◁ η ≫ (α_ f g h').hom

Full source

@[reassoc]
theorem comp_whiskerLeft_symm (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
    f ◁ g ◁ η = (α_ f g h).inv ≫ (f ≫ g) ◁ η ≫ (α_ f g h').hom := by simp

Whiskering-Associator Symmetry in Bicategories

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$, and any 2-morphism $\eta \colon h \to h'$ between 1-morphisms $h, h' \colon c \to d$, the following equation holds in the bicategory: \[ f \triangleleft (g \triangleleft \eta) = \alpha_{f,g,h}^{-1} \circ \big((f \circ g) \triangleleft \eta\big) \circ \alpha_{f,g,h'} \] where: - $\triangleleft$ denotes left whiskering, - $\alpha_{f,g,h}$ is the associator isomorphism $(f \circ g) \circ h \cong f \circ (g \circ h)$, - $\circ$ denotes vertical composition of 2-morphisms.

CategoryTheory.Bicategory.leftUnitor_naturality theorem

{f g : a ⟶ b} (η : f ⟶ g) : 𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η

Full source

@[reassoc]
theorem leftUnitor_naturality {f g : a ⟶ b} (η : f ⟶ g) :
    𝟙𝟙 a ◁ η𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η := by
  simp

Naturality of the Left Unitor in a Bicategory

Informal description

For any 2-morphism $\eta : f \Rightarrow g$ between parallel 1-morphisms $f, g : a \to b$ in a bicategory, the following diagram commutes: \[ (\text{id}_a \triangleleft \eta) \circ \lambda_g = \lambda_f \circ \eta \] where $\lambda_f : \text{id}_a \circ f \cong f$ and $\lambda_g : \text{id}_a \circ g \cong g$ are the left unitor isomorphisms, and $\triangleleft$ denotes left whiskering.

CategoryTheory.Bicategory.leftUnitor_inv_naturality theorem

{f g : a ⟶ b} (η : f ⟶ g) : η ≫ (λ_ g).inv = (λ_ f).inv ≫ 𝟙 a ◁ η

Full source

@[reassoc]
theorem leftUnitor_inv_naturality {f g : a ⟶ b} (η : f ⟶ g) :
    η ≫ (λ_ g).inv = (λ_ f).inv ≫ 𝟙 a ◁ η := by simp

Naturality of Left Unitor Inverse in Bicategories

Informal description

For any 2-morphism $\eta : f \Rightarrow g$ between 1-morphisms $f, g : a \to b$ in a bicategory, the following diagram commutes: \[ \eta \circ \lambda_g^{-1} = \lambda_f^{-1} \circ (\text{id}_a \triangleleft \eta) \] where $\lambda_f$ and $\lambda_g$ are the left unitor isomorphisms for $f$ and $g$ respectively, and $\triangleleft$ denotes left whiskering.

CategoryTheory.Bicategory.id_whiskerLeft_symm theorem

{f g : a ⟶ b} (η : f ⟶ g) : η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom

Full source

theorem id_whiskerLeft_symm {f g : a ⟶ b} (η : f ⟶ g) : η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom := by
  simp

Symmetrized Identity Whiskering via Left Unitors

Informal description

For any 2-morphism $\eta : f \Rightarrow g$ between parallel 1-morphisms $f, g : a \to b$ in a bicategory, the following equality holds: \[ \eta = \lambda_f^{-1} \circ (\text{id}_a \triangleleft \eta) \circ \lambda_g \] where $\lambda_f$ and $\lambda_g$ are the left unitor isomorphisms for $f$ and $g$ respectively, and $\triangleleft$ denotes left whiskering.

CategoryTheory.Bicategory.rightUnitor_naturality theorem

{f g : a ⟶ b} (η : f ⟶ g) : η ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η

Full source

@[reassoc]
theorem rightUnitor_naturality {f g : a ⟶ b} (η : f ⟶ g) :
    η ▷ 𝟙 bη ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η := by simp

Naturality of the Right Unitor in a Bicategory

Informal description

For any two parallel 1-morphisms $f, g : a \to b$ in a bicategory $\mathcal{B}$ and any 2-morphism $\eta : f \Rightarrow g$, the following diagram commutes: \[ (\eta \triangleright \text{id}_b) \circ \rho_g = \rho_f \circ \eta \] where $\rho_f : f \circ \text{id}_b \Rightarrow f$ and $\rho_g : g \circ \text{id}_b \Rightarrow g$ are the right unitor isomorphisms, and $\triangleright$ denotes right whiskering.

CategoryTheory.Bicategory.rightUnitor_inv_naturality theorem

{f g : a ⟶ b} (η : f ⟶ g) : η ≫ (ρ_ g).inv = (ρ_ f).inv ≫ η ▷ 𝟙 b

Full source

@[reassoc]
theorem rightUnitor_inv_naturality {f g : a ⟶ b} (η : f ⟶ g) :
    η ≫ (ρ_ g).inv = (ρ_ f).inv ≫ η ▷ 𝟙 b := by simp

Naturality of the Right Unitor Inverse in a Bicategory

Informal description

For any 2-morphism $\eta \colon f \Rightarrow g$ between parallel 1-morphisms $f, g \colon a \to b$ in a bicategory, the following diagram commutes: \[ \eta \circ \rho_g^{-1} = \rho_f^{-1} \circ (\eta \triangleright \text{id}_b) \] where $\rho_f \colon f \circ \text{id}_b \Rightarrow f$ is the right unitor isomorphism and $\rho_g^{-1}$ denotes its inverse.

CategoryTheory.Bicategory.whiskerRight_id_symm theorem

{f g : a ⟶ b} (η : f ⟶ g) : η = (ρ_ f).inv ≫ η ▷ 𝟙 b ≫ (ρ_ g).hom

Full source

theorem whiskerRight_id_symm {f g : a ⟶ b} (η : f ⟶ g) : η = (ρ_ f).inv ≫ η ▷ 𝟙 b ≫ (ρ_ g).hom := by
  simp

Expression of a 2-morphism via right whiskering and unitors

Informal description

For any 2-morphism $\eta \colon f \Rightarrow g$ between parallel 1-morphisms $f, g \colon a \to b$ in a bicategory, the following equality holds: \[ \eta = \rho_f^{-1} \circ (\eta \triangleright \text{id}_b) \circ \rho_g \] where $\rho_f \colon f \circ \text{id}_b \Rightarrow f$ and $\rho_g \colon g \circ \text{id}_b \Rightarrow g$ are the right unitor isomorphisms, and $\triangleright$ denotes right whiskering.

CategoryTheory.Bicategory.whiskerLeft_iff theorem

{f g : a ⟶ b} (η θ : f ⟶ g) : 𝟙 a ◁ η = 𝟙 a ◁ θ ↔ η = θ

Full source

theorem whiskerLeft_iff {f g : a ⟶ b} (η θ : f ⟶ g) : 𝟙𝟙 a ◁ η𝟙 a ◁ η = 𝟙 a ◁ θ ↔ η = θ := by simp

Equality of 2-Morphisms via Left Whiskering with Identity

Informal description

For any two parallel 2-morphisms $\eta, \theta \colon f \Rightarrow g$ between 1-morphisms $f, g \colon a \to b$ in a bicategory, the left whiskering of $\eta$ and $\theta$ with the identity 1-morphism $\text{id}_a$ are equal if and only if $\eta$ and $\theta$ are equal. That is, \[ \text{id}_a \triangleleft \eta = \text{id}_a \triangleleft \theta \quad \text{if and only if} \quad \eta = \theta. \]

CategoryTheory.Bicategory.whiskerRight_iff theorem

{f g : a ⟶ b} (η θ : f ⟶ g) : η ▷ 𝟙 b = θ ▷ 𝟙 b ↔ η = θ

Full source

theorem whiskerRight_iff {f g : a ⟶ b} (η θ : f ⟶ g) : η ▷ 𝟙 bη ▷ 𝟙 b = θ ▷ 𝟙 b ↔ η = θ := by simp

Right Whiskering with Identity Preserves Equality of 2-Morphisms

Informal description

For any parallel 1-morphisms $f, g : a \to b$ in a bicategory $\mathcal{B}$ and any 2-morphisms $\eta, \theta : f \Rightarrow g$, the equality of right whiskerings $\eta \triangleright \text{id}_b = \theta \triangleright \text{id}_b$ holds if and only if $\eta = \theta$.

CategoryTheory.Bicategory.leftUnitor_whiskerRight theorem

(f : a ⟶ b) (g : b ⟶ c) : (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom

Full source

/-- We state it as a simp lemma, which is regarded as an involved version of
`id_whiskerRight f g : 𝟙 f ▷ g = 𝟙 (f ≫ g)`.
-/
@[reassoc, simp]
theorem leftUnitor_whiskerRight (f : a ⟶ b) (g : b ⟶ c) :
    (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom := by
  rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ←
      cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle, ← associator_naturality_middle, ←
      comp_whiskerRight_assoc, triangle, associator_naturality_left]

Compatibility of Left Unitor with Right Whiskering and Associator

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory, the right whiskering of the left unitor $\lambda_f$ with $g$ is equal to the composition of the associator $\alpha_{\text{id}_a, f, g}$ with the left unitor $\lambda_{f \circ g}$. That is, \[ \lambda_f \triangleright g = \alpha_{\text{id}_a, f, g} \circ \lambda_{f \circ g}. \]

CategoryTheory.Bicategory.leftUnitor_inv_whiskerRight theorem

(f : a ⟶ b) (g : b ⟶ c) : (λ_ f).inv ▷ g = (λ_ (f ≫ g)).inv ≫ (α_ (𝟙 a) f g).inv

Full source

@[reassoc, simp]
theorem leftUnitor_inv_whiskerRight (f : a ⟶ b) (g : b ⟶ c) :
    (λ_ f).inv ▷ g = (λ_ (f ≫ g)).inv ≫ (α_ (𝟙 a) f g).inv :=
  eq_of_inv_eq_inv (by simp)

Inverse Left Unitor and Right Whiskering Relation: $\lambda_f^{-1} \triangleright g = \lambda_{f \circ g}^{-1} \circ \alpha_{\text{id}_a, f, g}^{-1}$

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory, the right whiskering of the inverse left unitor $\lambda_f^{-1}$ with $g$ is equal to the composition of the inverse left unitor $\lambda_{f \circ g}^{-1}$ with the inverse associator $\alpha_{\text{id}_a, f, g}^{-1}$. That is, \[ \lambda_f^{-1} \triangleright g = \lambda_{f \circ g}^{-1} \circ \alpha_{\text{id}_a, f, g}^{-1}. \]

CategoryTheory.Bicategory.whiskerLeft_rightUnitor theorem

(f : a ⟶ b) (g : b ⟶ c) : f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom

Full source

@[reassoc, simp]
theorem whiskerLeft_rightUnitor (f : a ⟶ b) (g : b ⟶ c) :
    f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom := by
  rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ←
      cancel_epi (f ◁ (α_ _ _ _).inv), pentagon_inv_assoc, triangle_assoc_comp_right, ←
      associator_inv_naturality_middle, ← whiskerLeft_comp_assoc, triangle_assoc_comp_right,
      associator_inv_naturality_right]

Left Whiskering of Right Unitor Equals Associator Inverse Composed with Composite Unitor

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory, the left whiskering of the right unitor $\rho_g$ with $f$ is equal to the composition of the inverse associator $\alpha_{f,g,\text{id}_c}^{-1}$ with the right unitor $\rho_{f \circ g}$. That is, \[ f \triangleleft \rho_g = \alpha_{f,g,\text{id}_c}^{-1} \circ \rho_{f \circ g}. \]

CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv theorem

(f : a ⟶ b) (g : b ⟶ c) : f ◁ (ρ_ g).inv = (ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom

Full source

@[reassoc, simp]
theorem whiskerLeft_rightUnitor_inv (f : a ⟶ b) (g : b ⟶ c) :
    f ◁ (ρ_ g).inv = (ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom :=
  eq_of_inv_eq_inv (by simp)

Left Whiskering of Inverse Right Unitor Equals Composite Unitor Inverse Composed with Associator

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory, the left whiskering of the inverse right unitor $\rho_g^{-1}$ with $f$ is equal to the composition of the inverse right unitor $\rho_{f \circ g}^{-1}$ with the associator $\alpha_{f,g,\text{id}_c}$. That is, \[ f \triangleleft \rho_g^{-1} = \rho_{f \circ g}^{-1} \circ \alpha_{f,g,\text{id}_c}. \]

CategoryTheory.Bicategory.leftUnitor_comp theorem

(f : a ⟶ b) (g : b ⟶ c) : (λ_ (f ≫ g)).hom = (α_ (𝟙 a) f g).inv ≫ (λ_ f).hom ▷ g

Full source

@[reassoc]
theorem leftUnitor_comp (f : a ⟶ b) (g : b ⟶ c) :
    (λ_ (f ≫ g)).hom = (α_ (𝟙 a) f g).inv ≫ (λ_ f).hom ▷ g := by simp

Composition of Left Unitor with Associator and Whiskering

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory, the left unitor $\lambda_{f \circ g}$ for the composite morphism $f \circ g$ is equal to the composition of the inverse associator $\alpha^{-1}_{\text{id}_a, f, g}$ with the right whiskering of the left unitor $\lambda_f$ by $g$. That is, \[ \lambda_{f \circ g} = \alpha^{-1}_{\text{id}_a, f, g} \circ (\lambda_f \triangleright g). \]

CategoryTheory.Bicategory.leftUnitor_comp_inv theorem

(f : a ⟶ b) (g : b ⟶ c) : (λ_ (f ≫ g)).inv = (λ_ f).inv ▷ g ≫ (α_ (𝟙 a) f g).hom

Full source

@[reassoc]
theorem leftUnitor_comp_inv (f : a ⟶ b) (g : b ⟶ c) :
    (λ_ (f ≫ g)).inv = (λ_ f).inv ▷ g(λ_ f).inv ▷ g ≫ (α_ (𝟙 a) f g).hom := by simp

Inverse Left Unitor Composition Identity: $\lambda_{f \circ g}^{-1} = (\lambda_f^{-1} \triangleright g) \circ \alpha_{\text{id}_a, f, g}$

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory, the inverse left unitor for the composite morphism $f \circ g$ satisfies: \[ \lambda_{f \circ g}^{-1} = (\lambda_f^{-1} \triangleright g) \circ \alpha_{\text{id}_a, f, g}, \] where $\lambda^{-1}$ denotes the inverse left unitor and $\alpha$ is the associator.

CategoryTheory.Bicategory.rightUnitor_comp theorem

(f : a ⟶ b) (g : b ⟶ c) : (ρ_ (f ≫ g)).hom = (α_ f g (𝟙 c)).hom ≫ f ◁ (ρ_ g).hom

Full source

@[reassoc]
theorem rightUnitor_comp (f : a ⟶ b) (g : b ⟶ c) :
    (ρ_ (f ≫ g)).hom = (α_ f g (𝟙 c)).hom ≫ f ◁ (ρ_ g).hom := by simp

Right Unitor Composition Identity: $\rho_{f \circ g} = \alpha_{f,g,\text{id}_c} \circ (f \triangleleft \rho_g)$

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory, the right unitor $\rho_{f \circ g}$ for the composite morphism $f \circ g$ is equal to the composition of the associator $\alpha_{f,g,\text{id}_c}$ with the left whiskering of the right unitor $\rho_g$ by $f$. That is, \[ \rho_{f \circ g} = \alpha_{f,g,\text{id}_c} \circ (f \triangleleft \rho_g). \]

CategoryTheory.Bicategory.rightUnitor_comp_inv theorem

(f : a ⟶ b) (g : b ⟶ c) : (ρ_ (f ≫ g)).inv = f ◁ (ρ_ g).inv ≫ (α_ f g (𝟙 c)).inv

Full source

@[reassoc]
theorem rightUnitor_comp_inv (f : a ⟶ b) (g : b ⟶ c) :
    (ρ_ (f ≫ g)).inv = f ◁ (ρ_ g).invf ◁ (ρ_ g).inv ≫ (α_ f g (𝟙 c)).inv := by simp

Inverse Right Unitor Composition Identity: $\rho_{f \circ g}^{-1} = (f \triangleleft \rho_g^{-1}) \circ \alpha_{f,g,\text{id}_c}^{-1}$

Informal description

For any 1-morphisms $f \colon a \to b$ and $g \colon b \to c$ in a bicategory, the inverse right unitor $\rho_{f \circ g}^{-1}$ for the composite morphism $f \circ g$ is equal to the composition of the left whiskering $f \triangleleft \rho_g^{-1}$ with the inverse associator $\alpha_{f,g,\text{id}_c}^{-1}$. That is, \[ \rho_{f \circ g}^{-1} = (f \triangleleft \rho_g^{-1}) \circ \alpha_{f,g,\text{id}_c}^{-1}. \]

CategoryTheory.Bicategory.unitors_equal theorem

: (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom

Full source

@[simp]
theorem unitors_equal : (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom := by
  rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ←
      rightUnitor_comp, rightUnitor_naturality]

Equality of Left and Right Unitors for Identity Morphism in a Bicategory

Informal description

For any object $a$ in a bicategory, the left unitor $\lambda_{\text{id}_a}$ and the right unitor $\rho_{\text{id}_a}$ for the identity 1-morphism $\text{id}_a$ are equal. That is, \[ \lambda_{\text{id}_a} = \rho_{\text{id}_a}. \]

CategoryTheory.Bicategory.unitors_inv_equal theorem

: (λ_ (𝟙 a)).inv = (ρ_ (𝟙 a)).inv

Full source

@[simp]
theorem unitors_inv_equal : (λ_ (𝟙 a)).inv = (ρ_ (𝟙 a)).inv := by simp [Iso.inv_eq_inv]

Equality of Inverse Left and Right Unitors for Identity Morphism in a Bicategory

Informal description

For any object $a$ in a bicategory, the inverses of the left unitor $\lambda_{\text{id}_a}$ and the right unitor $\rho_{\text{id}_a}$ for the identity 1-morphism $\text{id}_a$ are equal. That is, \[ \lambda_{\text{id}_a}^{-1} = \rho_{\text{id}_a}^{-1}. \]

CategoryTheory.Bicategory.precomp definition

(c : B) (f : a ⟶ b) : (b ⟶ c) ⥤ (a ⟶ c)

Full source

/-- Precomposition of a 1-morphism as a functor. -/
@[simps]
def precomp (c : B) (f : a ⟶ b) : (b ⟶ c) ⥤ (a ⟶ c) where
  obj := (f ≫ ·)
  map := (f ◁ ·)

Precomposition functor in a bicategory

Informal description

The functor that precomposes a given 1-morphism $f : a \to b$ to any 1-morphism in the category $(b \to c)$, resulting in a 1-morphism in $(a \to c)$. More precisely, for an object $c$ in the bicategory $\mathcal{B}$ and a 1-morphism $f : a \to b$, the functor $\text{precomp}(c, f) : (b \to c) \to (a \to c)$ is defined by: - On objects (1-morphisms $g : b \to c$): $\text{precomp}(c, f)(g) = f \circ g$, - On morphisms (2-morphisms $\eta : g \Rightarrow h$): $\text{precomp}(c, f)(\eta) = f \triangleleft \eta$ (left whiskering of $\eta$ by $f$).

CategoryTheory.Bicategory.precomposing definition

(a b c : B) : (a ⟶ b) ⥤ (b ⟶ c) ⥤ (a ⟶ c)

Full source

/-- Precomposition of a 1-morphism as a functor from the category of 1-morphisms `a ⟶ b` into the
category of functors `(b ⟶ c) ⥤ (a ⟶ c)`. -/
@[simps]
def precomposing (a b c : B) : (a ⟶ b) ⥤ (b ⟶ c) ⥤ (a ⟶ c) where
  obj f := precomp c f
  map η := { app := (η ▷ ·) }

Precomposition functor family in a bicategory

Informal description

For objects $a, b, c$ in a bicategory $\mathcal{B}$, the functor $\text{precomposing}(a, b, c) : (a \to b) \to (b \to c) \to (a \to c)$ is defined by: - On objects (1-morphisms $f : a \to b$): $\text{precomposing}(a, b, c)(f) = \text{precomp}(c, f)$, where $\text{precomp}(c, f)$ is the precomposition functor that maps $g : b \to c$ to $f \circ g$ and $\eta : g \Rightarrow h$ to $f \triangleleft \eta$, - On morphisms (2-morphisms $\eta : f \Rightarrow g$): $\text{precomposing}(a, b, c)(\eta)$ is the natural transformation whose component at $h : b \to c$ is $\eta \triangleright h$ (right whiskering of $\eta$ by $h$).

CategoryTheory.Bicategory.postcomp definition

(a : B) (f : b ⟶ c) : (a ⟶ b) ⥤ (a ⟶ c)

Full source

/-- Postcomposition of a 1-morphism as a functor. -/
@[simps]
def postcomp (a : B) (f : b ⟶ c) : (a ⟶ b) ⥤ (a ⟶ c) where
  obj := (· ≫ f)
  map := (· ▷ f)

Postcomposition functor in a bicategory

Informal description

The functor that postcomposes a given 1-morphism $f : b \to c$ to any 1-morphism in the category $(a \to b)$, resulting in a 1-morphism in $(a \to c)$. More precisely, for an object $a$ in the bicategory $\mathcal{B}$ and a 1-morphism $f : b \to c$, the functor $\text{postcomp}(a, f) : (a \to b) \to (a \to c)$ is defined by: - On objects (1-morphisms $g : a \to b$): $\text{postcomp}(a, f)(g) = g \circ f$, - On morphisms (2-morphisms $\eta : g \Rightarrow h$): $\text{postcomp}(a, f)(\eta) = \eta \triangleright f$ (right whiskering of $\eta$ by $f$).

CategoryTheory.Bicategory.postcomposing definition

(a b c : B) : (b ⟶ c) ⥤ (a ⟶ b) ⥤ (a ⟶ c)

Full source

/-- Postcomposition of a 1-morphism as a functor from the category of 1-morphisms `b ⟶ c` into the
category of functors `(a ⟶ b) ⥤ (a ⟶ c)`. -/
@[simps]
def postcomposing (a b c : B) : (b ⟶ c) ⥤ (a ⟶ b) ⥤ (a ⟶ c) where
  obj f := postcomp a f
  map η := { app := (· ◁ η) }

Postcomposition functor family in a bicategory

Informal description

For objects $a, b, c$ in a bicategory $\mathcal{B}$, the functor $\text{postcomposing}(a, b, c) : (b \to c) \to (a \to b) \to (a \to c)$ is defined by: - On objects (1-morphisms $f : b \to c$): $\text{postcomposing}(a, b, c)(f) = \text{postcomp}(a, f)$, where $\text{postcomp}(a, f)$ is the postcomposition functor that sends $g : a \to b$ to $g \circ f$, - On morphisms (2-morphisms $\eta : f \Rightarrow g$): $\text{postcomposing}(a, b, c)(\eta)$ is the natural transformation whose component at $h : a \to b$ is the left whiskering $h \triangleleft \eta$.

CategoryTheory.Bicategory.associatorNatIsoLeft definition

 (a : B) (g : b ⟶ c) (h : c ⟶ d) :
  (postcomposing a ..).obj g ⋙ (postcomposing ..).obj h ≅ (postcomposing ..).obj (g ≫ h)

Full source

/-- Left component of the associator as a natural isomorphism. -/
@[simps!]
def associatorNatIsoLeft (a : B) (g : b ⟶ c) (h : c ⟶ d) :
    (postcomposing a ..).obj g ⋙ (postcomposing ..).obj h(postcomposing a ..).obj g ⋙ (postcomposing ..).obj h ≅ (postcomposing ..).obj (g ≫ h) :=
  NatIso.ofComponents (α_ · g h)

Left associator natural isomorphism in a bicategory

Informal description

For objects $a, b, c, d$ in a bicategory $\mathcal{B}$ and 1-morphisms $g : b \to c$ and $h : c \to d$, the natural isomorphism $\text{associatorNatIsoLeft}(a, g, h)$ relates the composition of postcomposition functors to the postcomposition functor of composed morphisms. Specifically, it provides an isomorphism between the functors: $$(\text{postcomposing}(a, b, c))(g) \circ (\text{postcomposing}(a, c, d))(h) \cong (\text{postcomposing}(a, b, d))(g \circ h)$$ where $\circ$ denotes functor composition. This isomorphism is built from the associator 2-morphisms $\alpha_{f,g,h}$ for all $f : a \to b$.

CategoryTheory.Bicategory.associatorNatIsoMiddle definition

 (f : a ⟶ b) (h : c ⟶ d) :
  (precomposing ..).obj f ⋙ (postcomposing ..).obj h ≅ (postcomposing ..).obj h ⋙ (precomposing ..).obj f

Full source

/-- Middle component of the associator as a natural isomorphism. -/
@[simps!]
def associatorNatIsoMiddle (f : a ⟶ b) (h : c ⟶ d) :
    (precomposing ..).obj f ⋙ (postcomposing ..).obj h(precomposing ..).obj f ⋙ (postcomposing ..).obj h ≅
      (postcomposing ..).obj h ⋙ (precomposing ..).obj f :=
  NatIso.ofComponents (α_ f · h)

Middle associator natural isomorphism for bicategories

Informal description

For any 1-morphisms $f : a \to b$ and $h : c \to d$ in a bicategory $\mathcal{B}$, there is a natural isomorphism between the functors: $$(\text{precomposing}(b, c, d))(f) \circ (\text{postcomposing}(a, b, c))(h) \cong (\text{postcomposing}(a, b, d))(h) \circ (\text{precomposing}(a, c, d))(f)$$ This isomorphism is the middle component of the associator natural isomorphism, which relates the two different ways of composing whiskering operations involving $f$ and $h$.

CategoryTheory.Bicategory.associatorNatIsoRight definition

 (f : a ⟶ b) (g : b ⟶ c) (d : B) : (precomposing _ _ d).obj (f ≫ g) ≅ (precomposing ..).obj g ⋙ (precomposing ..).obj f

Full source

/-- Right component of the associator as a natural isomorphism. -/
@[simps!]
def associatorNatIsoRight (f : a ⟶ b) (g : b ⟶ c) (d : B) :
    (precomposing _ _ d).obj (f ≫ g) ≅ (precomposing ..).obj g ⋙ (precomposing ..).obj f :=
  NatIso.ofComponents (α_ f g ·)

Right associator natural isomorphism for precomposition functors

Informal description

For 1-morphisms $f : a \to b$ and $g : b \to c$ in a bicategory $\mathcal{B}$, and any object $d$, the right component of the associator is a natural isomorphism between functors: \[ \text{precomposing}(a, c, d)(f \circ g) \cong \text{precomposing}(b, c, d)(g) \circ \text{precomposing}(a, b, d)(f) \] This isomorphism expresses the associativity of composition of 1-morphisms in the bicategory when viewed through the lens of precomposition functors. The components of this natural isomorphism are given by the associator 2-morphisms $\alpha_{f,g,h}$ for each 1-morphism $h : c \to d$.

CategoryTheory.Bicategory.leftUnitorNatIso definition

(a b : B) : (precomposing _ _ b).obj (𝟙 a) ≅ 𝟭 (a ⟶ b)

Full source

/-- Left unitor as a natural isomorphism. -/
@[simps!]
def leftUnitorNatIso (a b : B) : (precomposing _ _ b).obj (𝟙 a) ≅ 𝟭 (a ⟶ b) :=
  NatIso.ofComponents (λ_ ·)

Left unitor natural isomorphism in a bicategory

Informal description

The left unitor natural isomorphism $\lambda$ in a bicategory $\mathcal{B}$ is defined for any objects $a, b$ as an isomorphism between the functor $\text{precomposing}(a, a, b)(\text{id}_a)$ (which precomposes with the identity 1-morphism $\text{id}_a$) and the identity functor $\text{id}_{(a \to b)}$ on the category of 1-morphisms from $a$ to $b$. This natural isomorphism $\lambda$ has components $\lambda_f : \text{id}_a \circ f \cong f$ for each 1-morphism $f : a \to b$, satisfying the naturality condition for all 2-morphisms between parallel 1-morphisms.

CategoryTheory.Bicategory.rightUnitorNatIso definition

(a b : B) : (postcomposing a _ _).obj (𝟙 b) ≅ 𝟭 (a ⟶ b)

Full source

/-- Right unitor as a natural isomorphism. -/
@[simps!]
def rightUnitorNatIso (a b : B) : (postcomposing a _ _).obj (𝟙 b) ≅ 𝟭 (a ⟶ b) :=
  NatIso.ofComponents (ρ_ ·)

Right unitor natural isomorphism in a bicategory

Informal description

For any objects $a$ and $b$ in a bicategory $\mathcal{B}$, the right unitor natural isomorphism $\rho$ is defined as a natural isomorphism between the functor $\text{postcomposing}(a, b, b)(\text{id}_b)$ (which postcomposes with the identity 1-morphism on $b$) and the identity functor $\text{id}_{(a \to b)}$ on the category of 1-morphisms from $a$ to $b$. This natural isomorphism $\rho$ has components $\rho_f : f \circ \text{id}_b \cong f$ for each 1-morphism $f : a \to b$, satisfying the naturality condition with respect to 2-morphisms between parallel 1-morphisms.