Documentation

Mathlib.CategoryTheory.Bicategory.Basic

Bicategories #

In this file we define typeclass for bicategories.

A bicategory B consists of

We use u, v, and w as the universe variables for objects, 1-morphisms, and 2-morphisms, respectively.

A typeclass for bicategories extends CategoryTheory.CategoryStruct typeclass. This means that we have

For each object a b : B, the collection of 1-morphisms a ⟶ b has a category structure. The 2-morphisms in the bicategory are implemented as the morphisms in this family of categories.

The composition of 1-morphisms is in fact an object part of a functor (a ⟶ b) ⥤ (b ⟶ c) ⥤ (a ⟶ c). The definition of bicategories in this file does not require this functor directly. Instead, it requires the whiskering functions. For a 1-morphism f : a ⟶ b and a 2-morphism η : g ⟶ h between 1-morphisms g h : b ⟶ c, there is a 2-morphism whiskerLeft f η : f ≫ g ⟶ f ≫ h. Similarly, for a 2-morphism η : f ⟶ g between 1-morphisms f g : a ⟶ b and a 1-morphism f : b ⟶ c, there is a 2-morphism whiskerRight η h : f ≫ h ⟶ g ≫ h. These satisfy the exchange law whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ, which is required as an axiom in the definition here.

class CategoryTheory.Bicategory (B : Type u) extends CategoryTheory.CategoryStruct :
Type (max (max u (v + 1)) (w + 1))

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.

Instances
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Simp-normal form for 2-morphisms #

        Rewriting involving associators and unitors could be very complicated. We try to ease this complexity by putting carefully chosen simp lemmas that rewrite any 2-morphisms into simp-normal form defined below. Rewriting into simp-normal form is also useful when applying (forthcoming) coherence tactic.

        The simp-normal form of 2-morphisms is defined to be an expression that has the minimal number of parentheses. More precisely,

        1. it is a composition of 2-morphisms like η₁ ≫ η₂ ≫ η₃ ≫ η₄ ≫ η₅ such that each ηᵢ is either a structural 2-morphisms (2-morphisms made up only of identities, associators, unitors) or non-structural 2-morphisms, and
        2. each non-structural 2-morphism in the composition is of the form f₁ ◁ f₂ ◁ f₃ ◁ η ▷ f₄ ▷ f₅, where each fᵢ is a 1-morphism that is not the identity or a composite and η is a non-structural 2-morphisms that is also not the identity or a composite.

        Note that f₁ ◁ f₂ ◁ f₃ ◁ η ▷ f₄ ▷ f₅ is actually f₁ ◁ (f₂ ◁ (f₃ ◁ ((η ▷ f₄) ▷ f₅))).

        @[simp]
        theorem CategoryTheory.Bicategory.whiskerLeftIso_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a b) {g : b c} {h : b c} (η : g h) :
        @[simp]
        theorem CategoryTheory.Bicategory.whiskerLeftIso_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a b) {g : b c} {h : b c} (η : g h) :

        The left whiskering of a 2-isomorphism is a 2-isomorphism.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.Bicategory.whiskerRightIso_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a b} {g : a b} (η : f g) (h : b c) :
          @[simp]
          theorem CategoryTheory.Bicategory.whiskerRightIso_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a b} {g : a b} (η : f g) (h : b c) :

          The right whiskering of a 2-isomorphism is a 2-isomorphism.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Bicategory.precomp_map {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (c : B) (f : a b) :
            @[simp]
            def CategoryTheory.Bicategory.precomp {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (c : B) (f : a b) :

            Precomposition of a 1-morphism as a functor.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem CategoryTheory.Bicategory.precomposing_map_app {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (c : B) :
              ∀ {X Y : a b} (η : X Y) (x : b c), ((CategoryTheory.Bicategory.precomposing a b c).map η).app x = CategoryTheory.Bicategory.whiskerRight η x

              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).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.Bicategory.postcomp_map {B : Type u} [CategoryTheory.Bicategory B] {b : B} {c : B} (a : B) (f : b c) :
                @[simp]
                def CategoryTheory.Bicategory.postcomp {B : Type u} [CategoryTheory.Bicategory B] {b : B} {c : B} (a : B) (f : b c) :

                Postcomposition of a 1-morphism as a functor.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.Bicategory.postcomposing_map_app {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (c : B) :
                  ∀ {X Y : b c} (η : X Y) (x : a b), ((CategoryTheory.Bicategory.postcomposing a b c).map η).app x = CategoryTheory.Bicategory.whiskerLeft x η

                  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).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Bicategory.associatorNatIsoLeft_inv_app {B : Type u} [CategoryTheory.Bicategory B] {b : B} {c : B} {d : B} (a : B) (g : b c) (h : c d) (X : a b) :
                    @[simp]
                    theorem CategoryTheory.Bicategory.associatorNatIsoLeft_hom_app {B : Type u} [CategoryTheory.Bicategory B] {b : B} {c : B} {d : B} (a : B) (g : b c) (h : c d) (X : a b) :
                    @[simp]
                    @[simp]
                    @[simp]
                    theorem CategoryTheory.Bicategory.associatorNatIsoRight_inv_app {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a b) (g : b c) (d : B) (X : c d) :
                    @[simp]
                    theorem CategoryTheory.Bicategory.associatorNatIsoRight_hom_app {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a b) (g : b c) (d : B) (X : c d) :