Documentation

Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Pseudofunctors #

A pseudofunctor is an oplax (or lax) functor whose mapId and mapComp are isomorphisms. We provide several constructors for pseudofunctors:

Main definitions #

structure CategoryTheory.Pseudofunctor (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] extends CategoryTheory.PrelaxFunctor :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

A pseudofunctor F between bicategories B and C consists of a function between objects F.obj, a function between 1-morphisms F.map, and a function between 2-morphisms F.map₂.

Unlike functors between categories, F.map do not need to strictly commute with the compositions, and do not need to strictly preserve the identity. Instead, there are specified 2-isomorphisms F.map (𝟙 a) ≅ 𝟙 (F.obj a) and F.map (f ≫ g) ≅ F.map f ≫ F.map g.

F.map₂ strictly commute with compositions and preserve the identity. They also preserve the associator, the left unitor, and the right unitor modulo some adjustments of domains and codomains of 2-morphisms.

Instances For
    @[simp]
    theorem CategoryTheory.Pseudofunctor.map₂_whisker_left {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {c : B} (f : a b) {g : b c} {h : b c} (η : g h) :
    self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) = CategoryTheory.CategoryStruct.comp (self.mapComp f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (self.mapComp f h).inv)
    @[simp]
    theorem CategoryTheory.Pseudofunctor.map₂_whisker_right {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {c : B} {f : a b} {g : a b} (η : f g) (h : b c) :
    self.map₂ (CategoryTheory.Bicategory.whiskerRight η h) = CategoryTheory.CategoryStruct.comp (self.mapComp f h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map h)) (self.mapComp g h).inv)
    @[simp]
    theorem CategoryTheory.Pseudofunctor.map₂_associator {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a b) (g : b c) (h : c d) :
    theorem CategoryTheory.Pseudofunctor.map₂_whisker_right_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {c : B} {f : a b} {g : a b} (η : f g) (h : b c) {Z : self.obj a self.obj c} (h : self.map (CategoryTheory.CategoryStruct.comp g h✝) Z) :
    theorem CategoryTheory.Pseudofunctor.map₂_whisker_left_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {c : B} (f : a b) {g : b c} {h : b c} (η : g h✝) {Z : self.obj a self.obj c} (h : self.map (CategoryTheory.CategoryStruct.comp f h✝) Z) :
    @[simp]
    theorem CategoryTheory.Pseudofunctor.toOplax_mapId {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) :
    F.toOplax.mapId a = (F.mapId a).hom
    @[simp]
    theorem CategoryTheory.Pseudofunctor.toOplax_toPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) :
    F.toOplax.toPrelaxFunctor = F.toPrelaxFunctor
    @[simp]
    theorem CategoryTheory.Pseudofunctor.toOplax_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) :
    ∀ {a b c : B} (f : a b) (g : b c), F.toOplax.mapComp f g = (F.mapComp f g).hom

    The oplax functor associated with a pseudofunctor.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • CategoryTheory.Pseudofunctor.hasCoeToOplax = { coe := CategoryTheory.Pseudofunctor.toOplax }
      @[simp]
      theorem CategoryTheory.Pseudofunctor.toLax_mapId {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) :
      F.toLax.mapId a = (F.mapId a).inv
      @[simp]
      theorem CategoryTheory.Pseudofunctor.toLax_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) :
      ∀ {a b c : B} (f : a b) (g : b c), F.toLax.mapComp f g = (F.mapComp f g).inv
      @[simp]
      theorem CategoryTheory.Pseudofunctor.toLax_toPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) :
      F.toLax.toPrelaxFunctor = F.toPrelaxFunctor

      The Lax functor associated with a pseudofunctor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • CategoryTheory.Pseudofunctor.hasCoeToLax = { coe := CategoryTheory.Pseudofunctor.toLax }

        The identity pseudofunctor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          @[simp]
          theorem CategoryTheory.Pseudofunctor.comp_mapId {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D) (a : B) :
          (F.comp G).mapId a = G.map₂Iso (F.mapId a) ≪≫ G.mapId (F.obj a)
          @[simp]
          theorem CategoryTheory.Pseudofunctor.comp_toPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D) :
          (F.comp G).toPrelaxFunctor = F.comp G.toPrelaxFunctor
          @[simp]
          theorem CategoryTheory.Pseudofunctor.comp_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D) :
          ∀ {a b c : B} (f : a b) (g : b c), (F.comp G).mapComp f g = G.map₂Iso (F.mapComp f g) ≪≫ G.mapComp (F.map f) (F.map g)

          Composition of pseudofunctors.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.Pseudofunctor.mkOfOplax_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (F' : F.PseudoCore) :
            ∀ {a b c : B} (f : a b) (g : b c), (CategoryTheory.Pseudofunctor.mkOfOplax F F').mapComp f g = F'.mapCompIso f g
            @[simp]
            theorem CategoryTheory.Pseudofunctor.mkOfOplax_mapId {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (F' : F.PseudoCore) (a : B) :
            (CategoryTheory.Pseudofunctor.mkOfOplax F F').mapId a = F'.mapIdIso a
            @[simp]

            Construct a pseudofunctor from an oplax functor whose mapId and mapComp are isomorphisms.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapComp_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] :
              ∀ {a b c : B} (f : a b) (g : b c), ((CategoryTheory.Pseudofunctor.mkOfOplax' F).mapComp f g).hom = F.mapComp f g
              @[simp]
              theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapId_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] (a : B) :
              ((CategoryTheory.Pseudofunctor.mkOfOplax' F).mapId a).hom = F.mapId a
              @[simp]
              theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapComp_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] :
              ∀ {a b c : B} (f : a b) (g : b c), ((CategoryTheory.Pseudofunctor.mkOfOplax' F).mapComp f g).inv = CategoryTheory.inv (F.mapComp f g)
              @[simp]
              theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapId_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] (a : B) :
              @[simp]
              theorem CategoryTheory.Pseudofunctor.mkOfOplax'_toPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] :
              (CategoryTheory.Pseudofunctor.mkOfOplax' F).toPrelaxFunctor = F.toPrelaxFunctor
              noncomputable def CategoryTheory.Pseudofunctor.mkOfOplax' {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] :

              Construct a pseudofunctor from an oplax functor whose mapId and mapComp are isomorphisms.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.Pseudofunctor.mkOfLax_toPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) (F' : F.PseudoCore) :
                (CategoryTheory.Pseudofunctor.mkOfLax F F').toPrelaxFunctor = F.toPrelaxFunctor
                @[simp]
                theorem CategoryTheory.Pseudofunctor.mkOfLax_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) (F' : F.PseudoCore) :
                ∀ {a b c : B} (f : a b) (g : b c), (CategoryTheory.Pseudofunctor.mkOfLax F F').mapComp f g = F'.mapCompIso f g
                @[simp]
                theorem CategoryTheory.Pseudofunctor.mkOfLax_mapId {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) (F' : F.PseudoCore) (a : B) :
                (CategoryTheory.Pseudofunctor.mkOfLax F F').mapId a = F'.mapIdIso a

                Construct a pseudofunctor from a lax functor whose mapId and mapComp are isomorphisms.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.Pseudofunctor.mkOfLax'_toPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] :
                  (CategoryTheory.Pseudofunctor.mkOfLax' F).toPrelaxFunctor = F.toPrelaxFunctor
                  @[simp]
                  theorem CategoryTheory.Pseudofunctor.mkOfLax'_mapComp_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] :
                  ∀ {a b c : B} (f : a b) (g : b c), ((CategoryTheory.Pseudofunctor.mkOfLax' F).mapComp f g).inv = F.mapComp f g
                  @[simp]
                  theorem CategoryTheory.Pseudofunctor.mkOfLax'_mapComp_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] :
                  ∀ {a b c : B} (f : a b) (g : b c), ((CategoryTheory.Pseudofunctor.mkOfLax' F).mapComp f g).hom = CategoryTheory.inv (F.mapComp f g)
                  @[simp]
                  theorem CategoryTheory.Pseudofunctor.mkOfLax'_mapId_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] (a : B) :
                  @[simp]
                  theorem CategoryTheory.Pseudofunctor.mkOfLax'_mapId_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] (a : B) :
                  ((CategoryTheory.Pseudofunctor.mkOfLax' F).mapId a).inv = F.mapId a
                  noncomputable def CategoryTheory.Pseudofunctor.mkOfLax' {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a b) (g : b c), CategoryTheory.IsIso (F.mapComp f g)] :

                  Construct a pseudofunctor from a lax functor whose mapId and mapComp are isomorphisms.

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