Mathlib.CategoryTheory.Bicategory.Strict

Module docstring

{"# Strict bicategories

A bicategory is called Strict if the left unitors, the right unitors, and the associators are isomorphisms given by equalities.

Implementation notes

In the literature of category theory, a strict bicategory (usually called a strict 2-category) is often defined as a bicategory whose left unitors, right unitors, and associators are identities. We cannot use this definition directly here since the types of 2-morphisms depend on 1-morphisms. For this reason, we use eqToIso, which gives isomorphisms from equalities, instead of identities. "}

CategoryTheory.Bicategory.Strict structure

Full source

/-- A bicategory is called `Strict` if the left unitors, the right unitors, and the associators are
isomorphisms given by equalities.
-/
class Bicategory.Strict : Prop where
  /-- Identity morphisms are left identities for composition. -/
  id_comp : ∀ {a b : B} (f : a ⟶ b), 𝟙𝟙 a ≫ f = f := by aesop_cat
  /-- Identity morphisms are right identities for composition. -/
  comp_id : ∀ {a b : B} (f : a ⟶ b), f ≫ 𝟙 b = f := by aesop_cat
  /-- Composition in a bicategory is associative. -/
  assoc : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), (f ≫ g) ≫ h = f ≫ g ≫ h := by
    aesop_cat
  /-- The left unitors are given by equalities -/
  leftUnitor_eqToIso : ∀ {a b : B} (f : a ⟶ b), λ_ f = eqToIso (id_comp f) := by aesop_cat
  /-- The right unitors are given by equalities -/
  rightUnitor_eqToIso : ∀ {a b : B} (f : a ⟶ b), ρ_ f = eqToIso (comp_id f) := by aesop_cat
  /-- The associators are given by equalities -/
  associator_eqToIso :
    ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), α_ f g h = eqToIso (assoc f g h) := by
    aesop_cat

Strict bicategory

Informal description

A bicategory is called *strict* if its left unitors, right unitors, and associators are isomorphisms induced by equalities (via `eqToIso`). This differs from the traditional definition where these are identity morphisms, due to type dependencies in the 2-morphisms.

CategoryTheory.StrictBicategory.category instance

[Bicategory.Strict B] : Category B

Full source

/-- Category structure on a strict bicategory -/
instance (priority := 100) StrictBicategory.category [Bicategory.Strict B] : Category B where
  id_comp := Bicategory.Strict.id_comp
  comp_id := Bicategory.Strict.comp_id
  assoc := Bicategory.Strict.assoc

Category Structure on a Strict Bicategory

Informal description

Every strict bicategory $B$ has an underlying category structure where the objects are those of $B$ and the morphisms are the 1-morphisms of $B$, with composition given by the horizontal composition in $B$.

CategoryTheory.Bicategory.whiskerLeft_eqToHom theorem

{a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g = h) : f ◁ eqToHom η = eqToHom (congr_arg₂ (· ≫ ·) rfl η)

Full source

@[simp]
theorem whiskerLeft_eqToHom {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g = h) :
    f ◁ eqToHom η = eqToHom (congr_arg₂ (· ≫ ·) rfl η) := by
  cases η
  simp only [whiskerLeft_id, eqToHom_refl]

Left Whiskering of Equality Morphism in Bicategory

Informal description

For any objects $a, b, c$ in a bicategory $B$, given a morphism $f : a \to b$ and morphisms $g, h : b \to c$ with an equality $\eta : g = h$, the left whiskering of $f$ with the morphism $\text{eqToHom}(\eta)$ (constructed from $\eta$) is equal to the morphism $\text{eqToHom}(\text{congr\_arg\_2}(\cdot \gg \cdot, \text{rfl}, \eta))$. Here, $\text{congr\_arg\_2}$ constructs an equality of compositions from equalities of morphisms.

CategoryTheory.Bicategory.eqToHom_whiskerRight theorem

{a b c : B} {f g : a ⟶ b} (η : f = g) (h : b ⟶ c) : eqToHom η ▷ h = eqToHom (congr_arg₂ (· ≫ ·) η rfl)

Full source

@[simp]
theorem eqToHom_whiskerRight {a b c : B} {f g : a ⟶ b} (η : f = g) (h : b ⟶ c) :
    eqToHomeqToHom η ▷ h = eqToHom (congr_arg₂ (· ≫ ·) η rfl) := by
  cases η
  simp only [id_whiskerRight, eqToHom_refl]

Right Whiskering of Equality Morphism in Bicategory

Informal description

For any objects $a, b, c$ in a bicategory $B$, given morphisms $f, g : a \to b$ and an equality $\eta : f = g$, and a morphism $h : b \to c$, the right whiskering of the morphism $\text{eqToHom}(\eta)$ with $h$ is equal to the morphism $\text{eqToHom}(\text{congr\_arg\_2}(\cdot \gg \cdot, \eta, \text{rfl}))$. Here, $\text{eqToHom}(\eta)$ is the morphism constructed from the equality $\eta$, and $\text{congr\_arg\_2}$ constructs an equality of compositions from equalities of morphisms.