Pseudofunctors

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

• Pseudofunctor.mk : the default constructor, which requires map₂_whiskerLeft and map₂_whiskerRight instead of naturality of mapComp.
• Pseudofunctor.mkOfOplax : construct a pseudofunctor from an oplax functor whose mapId and mapComp are isomorphisms. This constructor uses Iso to describe isomorphisms.
• pseudofunctor.mkOfOplax' : similar to mkOfOplax, but uses IsIso to describe isomorphisms.

The additional constructors are useful when constructing a pseudofunctor where the construction of the oplax functor associated with it is already done. For example, the composition of pseudofunctors can be defined by using the composition of oplax functors as follows:

def comp (F : Pseudofunctor B C) (G : Pseudofunctor C D) : Pseudofunctor B D :=
  mkOfOplax ((F : OplaxFunctor B C).comp G)
  { mapIdIso := fun a ↦ (G.mapFunctor _ _).mapIso (F.mapId a) ≪≫ G.mapId (F.obj a),
    mapCompIso := fun f g ↦
      (G.mapFunctor _ _).mapIso (F.mapComp f g) ≪≫ G.mapComp (F.map f) (F.map g) }

although the composition of pseudofunctors in this file is defined by using the default constructor because obviously wasn't smart enough in mathlib3 and the porter of this file was too lazy to investigate this issue further in mathlib4. Similarly, the composition is also defined by using mkOfOplax' after giving appropriate instances for IsIso. The former constructor mkOfOplax requires isomorphisms as data type Iso, and so it is useful if you don't want to forget the definitions of the inverses. On the other hand, the latter constructor mkOfOplax' is useful if you want to use propositional type class IsIso.

Main definitions

• CategoryTheory.Pseudofunctor B C : a pseudofunctor between bicategories B and C
• CategoryTheory.Pseudofunctor.comp F G : the composition of pseudofunctors

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.

• obj : B → C
• map : {X Y : B} → (X ⟶ Y) → ((↑self.toPrelaxFunctor).obj X ⟶ (↑self.toPrelaxFunctor).obj Y)
• map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → ((↑self.toPrelaxFunctor).map f ⟶ (↑self.toPrelaxFunctor).map g)
• mapId : (a : B) → (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id ((↑self.toPrelaxFunctor).obj a)
• mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).map g)
• map₂_id : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id ((↑self.toPrelaxFunctor).map f)
• map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), self.map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
• map₂_whisker_left : ∀ {a b c : B} (f : a ⟶ b) {g 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.toPrelaxFunctor).map f) (self.map₂ η)) (self.mapComp f h).inv)
• map₂_whisker_right : ∀ {a b c : B} {f 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.toPrelaxFunctor).map h)) (self.mapComp g h).inv)
• map₂_associator : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), self.map₂ (CategoryTheory.Bicategory.associator f g h).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g).hom ((↑self.toPrelaxFunctor).map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).map g) ((↑self.toPrelaxFunctor).map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (self.mapComp g h).inv) (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv)))
• map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a).hom ((↑self.toPrelaxFunctor).map f)) (CategoryTheory.Bicategory.leftUnitor ((↑self.toPrelaxFunctor).map f)).hom)
• map₂_right_unitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (self.mapId b).hom) (CategoryTheory.Bicategory.rightUnitor ((↑self.toPrelaxFunctor).map f)).hom)

@[simp]

theorem CategoryTheory.Pseudofunctor.map₂_id {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} (f : a ⟶ b) : self.map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id ((↑self.toPrelaxFunctor).map f)

@[simp]

theorem CategoryTheory.Pseudofunctor.map₂_comp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) : self.map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (self.map₂ η) (self.map₂ θ)

@[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.toPrelaxFunctor).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.toPrelaxFunctor).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) : self.map₂ (CategoryTheory.Bicategory.associator f g h).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g).hom ((↑self.toPrelaxFunctor).map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).map g) ((↑self.toPrelaxFunctor).map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (self.mapComp g h).inv) (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv)))

@[simp]

theorem CategoryTheory.Pseudofunctor.map₂_left_unitor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} (f : a ⟶ b) : self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a).hom ((↑self.toPrelaxFunctor).map f)) (CategoryTheory.Bicategory.leftUnitor ((↑self.toPrelaxFunctor).map f)).hom)

@[simp]

theorem CategoryTheory.Pseudofunctor.map₂_right_unitor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} (f : a ⟶ b) : self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (self.mapId b).hom) (CategoryTheory.Bicategory.rightUnitor ((↑self.toPrelaxFunctor).map f)).hom)

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.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj c} (h : (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp g h✝) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η h✝)) h = CategoryTheory.CategoryStruct.comp (self.mapComp f h✝).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) ((↑self.toPrelaxFunctor).map h✝)) (CategoryTheory.CategoryStruct.comp (self.mapComp g h✝).inv h))

theorem CategoryTheory.Pseudofunctor.map₂_comp_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h✝) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj b} (h : (↑self.toPrelaxFunctor).map h✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (self.map₂ η) (CategoryTheory.CategoryStruct.comp (self.map₂ θ) h)

theorem CategoryTheory.Pseudofunctor.map₂_left_unitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj b} (h : (↑self.toPrelaxFunctor).map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom) h = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a).hom ((↑self.toPrelaxFunctor).map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor ((↑self.toPrelaxFunctor).map f)).hom h))

theorem CategoryTheory.Pseudofunctor.map₂_right_unitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj b} (h : (↑self.toPrelaxFunctor).map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom) h = CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (self.mapId b).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor ((↑self.toPrelaxFunctor).map f)).hom h))

theorem CategoryTheory.Pseudofunctor.map₂_associator_assoc {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) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj d} (h : (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h✝)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h✝).hom) h = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h✝).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g).hom ((↑self.toPrelaxFunctor).map h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).map g) ((↑self.toPrelaxFunctor).map h✝)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (self.mapComp g h✝).inv) (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h✝)).inv h))))

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.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj c} (h : (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp f h✝) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) h = CategoryTheory.CategoryStruct.comp (self.mapComp f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (self.map₂ η)) (CategoryTheory.CategoryStruct.comp (self.mapComp f h✝).inv h))

instance CategoryTheory.Pseudofunctor.hasCoeToPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] : Coe (CategoryTheory.Pseudofunctor B C) (CategoryTheory.PrelaxFunctor B C)

Equations

• CategoryTheory.Pseudofunctor.hasCoeToPrelaxFunctor = { coe := CategoryTheory.Pseudofunctor.toPrelaxFunctor }

def CategoryTheory.Pseudofunctor.toOplax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) : CategoryTheory.OplaxFunctor B C

The oplax functor associated with a pseudofunctor.

Equations

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

instance CategoryTheory.Pseudofunctor.hasCoeToOplax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] : Coe (CategoryTheory.Pseudofunctor B C) (CategoryTheory.OplaxFunctor B C)

Equations

• CategoryTheory.Pseudofunctor.hasCoeToOplax = { coe := CategoryTheory.Pseudofunctor.toOplax }

@[simp]

theorem CategoryTheory.Pseudofunctor.to_oplax_obj {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) : (↑F.toOplax.toPrelaxFunctor).obj = (↑F.toPrelaxFunctor).obj

@[simp]

theorem CategoryTheory.Pseudofunctor.to_oplax_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.to_oplax_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : F.toOplax.mapComp f g = (F.mapComp f g).hom

@[simp]

theorem CategoryTheory.Pseudofunctor.mapFunctor_obj {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) (b : B) (f : a ⟶ b) : (F.mapFunctor a b).obj f = (↑F.toOplax.toPrelaxFunctor).map f

@[simp]

theorem CategoryTheory.Pseudofunctor.mapFunctor_map {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) (b : B) : ∀ {X Y : a ⟶ b} (η : X ⟶ Y), (F.mapFunctor a b).map η = F.toOplax.map₂ η

def CategoryTheory.Pseudofunctor.mapFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) (b : B) : CategoryTheory.Functor (a ⟶ b) ((↑F.toPrelaxFunctor).obj a ⟶ (↑F.toPrelaxFunctor).obj b)

Function on 1-morphisms as a functor.

Equations

• F.mapFunctor a b = F.toOplax.mapFunctor a b

@[simp]

theorem CategoryTheory.Pseudofunctor.map₂Iso_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ≅ g) : (F.map₂Iso η).hom = F.toOplax.map₂ η.hom

@[simp]

theorem CategoryTheory.Pseudofunctor.map₂Iso_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ≅ g) : (F.map₂Iso η).inv = F.toOplax.map₂ η.inv

@[reducible, inline]

abbrev CategoryTheory.Pseudofunctor.map₂Iso {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ≅ g) : (↑F.toPrelaxFunctor).map f ≅ (↑F.toPrelaxFunctor).map g

A pseudofunctor F : B ⥤ C sends 2-isomorphisms η : f ≅ f to 2-isomorphisms F.map f ≅ F.map g

Equations

• F.map₂Iso η = F.toOplax.map₂Iso η

instance CategoryTheory.Pseudofunctor.map₂_isIso {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] : CategoryTheory.IsIso (F.map₂ η)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Pseudofunctor.map₂_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] : F.map₂ (CategoryTheory.inv η) = CategoryTheory.inv (F.map₂ η)

theorem CategoryTheory.Pseudofunctor.map₂_hom_inv_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] {Z : (↑F.toPrelaxFunctor).obj a ⟶ (↑F.toPrelaxFunctor).obj b} (h : (↑F.toPrelaxFunctor).map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map₂ η) (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.inv η)) h) = h

theorem CategoryTheory.Pseudofunctor.map₂_hom_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] : CategoryTheory.CategoryStruct.comp (F.map₂ η) (F.map₂ (CategoryTheory.inv η)) = CategoryTheory.CategoryStruct.id ((↑F.toPrelaxFunctor).map f)

theorem CategoryTheory.Pseudofunctor.map₂_inv_hom_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] {Z : (↑F.toPrelaxFunctor).obj a ⟶ (↑F.toPrelaxFunctor).obj b} (h : (↑F.toPrelaxFunctor).map g ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.inv η)) (CategoryTheory.CategoryStruct.comp (F.map₂ η) h) = h

theorem CategoryTheory.Pseudofunctor.map₂_inv_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] : CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.inv η)) (F.map₂ η) = CategoryTheory.CategoryStruct.id ((↑F.toPrelaxFunctor).map g)

@[simp]

theorem CategoryTheory.Pseudofunctor.id_mapComp (B : Type u₁) [CategoryTheory.Bicategory B] : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.Pseudofunctor.id B).mapComp f g = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.Pseudofunctor.id_mapId (B : Type u₁) [CategoryTheory.Bicategory B] (a : B) : (CategoryTheory.Pseudofunctor.id B).mapId a = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.id a)

@[simp]

theorem CategoryTheory.Pseudofunctor.id_toPrelaxFunctor (B : Type u₁) [CategoryTheory.Bicategory B] : (CategoryTheory.Pseudofunctor.id B).toPrelaxFunctor = CategoryTheory.PrelaxFunctor.id B

def CategoryTheory.Pseudofunctor.id (B : Type u₁) [CategoryTheory.Bicategory B] : CategoryTheory.Pseudofunctor B B

The identity pseudofunctor.

Equations

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

instance CategoryTheory.Pseudofunctor.instInhabited {B : Type u₁} [CategoryTheory.Bicategory B] : Inhabited (CategoryTheory.Pseudofunctor B B)

Equations

• CategoryTheory.Pseudofunctor.instInhabited = { default := CategoryTheory.Pseudofunctor.id B }

def CategoryTheory.Pseudofunctor.comp {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) : CategoryTheory.Pseudofunctor B D

Composition of pseudofunctors.

Equations

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

@[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_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.toPrelaxFunctor).obj a)

@[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.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g)

@[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_toPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (F' : F.PseudoCore) : (CategoryTheory.Pseudofunctor.mkOfOplax F F').toPrelaxFunctor = F.toPrelaxFunctor

@[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

def CategoryTheory.Pseudofunctor.mkOfOplax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (F' : F.PseudoCore) : CategoryTheory.Pseudofunctor B C

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.

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapId {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 = CategoryTheory.asIso (F.mapId a)

@[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

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapComp {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 = CategoryTheory.asIso (F.mapComp f g)

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)] : CategoryTheory.Pseudofunctor B C

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.