Documentation

Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

The bicategory of oplax functors between two bicategories #

Given bicategories B and C, we give a bicategory structure on OplaxFunctor B C whose

source
def CategoryTheory.Oplax.OplaxTrans.whiskerLeft {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) :
CategoryStruct.comp η θ ⟶ CategoryStruct.comp η ι

Left whiskering of an oplax natural transformation and a modification.

Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Oplax.OplaxTrans.whiskerLeft_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) (a : B) :
      (whiskerLeft η Γ).app a = Bicategory.whiskerLeft (η.app a) (Γ.app a)
      source
      def CategoryTheory.Oplax.OplaxTrans.whiskerRight {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) :
      CategoryStruct.comp η ι ⟶ CategoryStruct.comp θ ι

      Right whiskering of an oplax natural transformation and a modification.

      Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Oplax.OplaxTrans.whiskerRight_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B) :
          (whiskerRight Γ ι).app a = Bicategory.whiskerRight (Γ.app a) (ι.app a)
          source
          def CategoryTheory.Oplax.OplaxTrans.associator {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) :
          CategoryStruct.comp (CategoryStruct.comp η θ) ι ≅ CategoryStruct.comp η (CategoryStruct.comp θ ι)

          Associator for the vertical composition of oplax natural transformations.

          Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Oplax.OplaxTrans.associator_hom_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) :
              (associator η θ ι).hom.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
              source
              @[simp]
              theorem CategoryTheory.Oplax.OplaxTrans.associator_inv_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) :
              (associator η θ ι).inv.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
              source
              def CategoryTheory.Oplax.OplaxTrans.leftUnitor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) :
              CategoryStruct.comp (CategoryStruct.id F) η ≅ η

              Left unitor for the vertical composition of oplax natural transformations.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Oplax.OplaxTrans.leftUnitor_inv_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) :
                  (leftUnitor η).inv.app a = (Bicategory.leftUnitor (η.app a)).inv
                  source
                  @[simp]
                  theorem CategoryTheory.Oplax.OplaxTrans.leftUnitor_hom_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) :
                  (leftUnitor η).hom.app a = (Bicategory.leftUnitor (η.app a)).hom
                  source
                  def CategoryTheory.Oplax.OplaxTrans.rightUnitor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) :
                  CategoryStruct.comp η (CategoryStruct.id G) ≅ η

                  Right unitor for the vertical composition of oplax natural transformations.

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Oplax.OplaxTrans.rightUnitor_hom_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) :
                      (rightUnitor η).hom.app a = (Bicategory.rightUnitor (η.app a)).hom
                      source
                      @[simp]
                      theorem CategoryTheory.Oplax.OplaxTrans.rightUnitor_inv_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) :
                      (rightUnitor η).inv.app a = (Bicategory.rightUnitor (η.app a)).inv
                      source
                      def CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] :
                      Bicategory (OplaxFunctor B C)

                      A bicategory structure on the oplax functors between bicategories.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_hom_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :
                          (Bicategory.rightUnitor η).hom.app a = (Bicategory.rightUnitor (η.app a)).hom
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_inv_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (x✝³ : OplaxFunctor B C) (η : x✝ ⟶ x✝¹) (θ : x✝¹ ⟶ x✝²) (ι : x✝² ⟶ x✝³) (a : B) :
                          (Bicategory.associator η θ ι).inv.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_homCategory_id_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (a b : OplaxFunctor B C) (η : a ⟶ b) (a✝ : B) :
                          (CategoryStruct.id η).app a✝ = CategoryStruct.id (η.app a✝)
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_hom_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (x✝³ : OplaxFunctor B C) (η : x✝ ⟶ x✝¹) (θ : x✝¹ ⟶ x✝²) (ι : x✝² ⟶ x✝³) (a : B) :
                          (Bicategory.associator η θ ι).hom.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_id_naturality (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (F : OplaxFunctor B C) {x✝ x✝¹ : B} (f : x✝ ⟶ x✝¹) :
                          (CategoryStruct.id F).naturality f = CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).hom (Bicategory.leftUnitor (F.map f)).inv
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_homCategory_comp_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (a b : OplaxFunctor B C) {X✝ Y✝ Z✝ : a ⟶ b} (Γ : Modification X✝ Y✝) (Δ : Modification Y✝ Z✝) (a✝ : B) :
                          (CategoryStruct.comp Γ Δ).app a✝ = CategoryStruct.comp (Γ.app a✝) (Δ.app a✝)
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_comp_naturality (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {X✝ Y✝ Z✝ : OplaxFunctor B C} (η : OplaxTrans X✝ Y✝) (θ : OplaxTrans Y✝ Z✝) {a b : B} (f : a ⟶ b) :
                          (CategoryStruct.comp η θ).naturality f = CategoryStruct.comp (Bicategory.associator (X✝.map f) (η.app b) (θ.app b)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f) (θ.app b)) (CategoryStruct.comp (Bicategory.associator (η.app a) (Y✝.map f) (θ.app b)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (θ.naturality f)) (Bicategory.associator (η.app a) (θ.app a) (Z✝.map f)).inv)))
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_inv_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :
                          (Bicategory.leftUnitor η).inv.app a = (Bicategory.leftUnitor (η.app a)).inv
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_comp_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {X✝ Y✝ Z✝ : OplaxFunctor B C} (η : OplaxTrans X✝ Y✝) (θ : OplaxTrans Y✝ Z✝) (a : B) :
                          (CategoryStruct.comp η θ).app a = CategoryStruct.comp (η.app a) (θ.app a)
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerLeft_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (x✝³ x✝⁴ : x✝¹ ⟶ x✝²) (Γ : x✝³ ⟶ x✝⁴) (a : B) :
                          (Bicategory.whiskerLeft η Γ).app a = Bicategory.whiskerLeft (η.app a) (Γ.app a)
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_inv_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :
                          (Bicategory.rightUnitor η).inv.app a = (Bicategory.rightUnitor (η.app a)).inv
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerRight_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (x✝³ x✝⁴ : x✝ ⟶ x✝¹) (Γ : x✝³ ⟶ x✝⁴) (η : x✝¹ ⟶ x✝²) (a : B) :
                          (Bicategory.whiskerRight Γ η).app a = Bicategory.whiskerRight (Γ.app a) (η.app a)
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_hom_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :
                          (Bicategory.leftUnitor η).hom.app a = (Bicategory.leftUnitor (η.app a)).hom
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_id_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (F : OplaxFunctor B C) (a : B) :
                          (CategoryStruct.id F).app a = CategoryStruct.id (F.obj a)
                          source
                          @[simp]
                          theorem CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_Hom (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (F G : OplaxFunctor B C) :
                          (F ⟶ G) = OplaxTrans F G