Transporting pseudofunctor presentations through equivalences

This file centralizes the Cat-level transport used when an objectwise model of a pseudofunctor is replaced by equivalent categories. It conjugates transition functors and transports their compositors, units, pentagon equation, and two triangle equations. Concrete consumers provide the presentation being transported; the coherence calculus itself belongs to the pseudofunctor root.

def CategoryTheory.Pseudofunctor.equivalenceTransportFunctor {C₀ : Type u_1} {D₀ : Type u_2} {C₁ : Type u_3} {D₁ : Type u_4} [Category.{u_5, u_1} C₀] [Category.{u_6, u_2} D₀] [Category.{u_7, u_3} C₁] [Category.{u_8, u_4} D₁] (E₀ : C₀ ≌ D₀) (E₁ : C₁ ≌ D₁) (F : Functor C₀ C₁) : Functor D₀ D₁

Conjugate a functor by equivalences of its source and target.

Equations

• CategoryTheory.Pseudofunctor.equivalenceTransportFunctor E₀ E₁ F = E₀.inverse.comp (F.comp E₁.functor)

def CategoryTheory.Pseudofunctor.equivalenceTransportCompIso {C₀ : Type u_1} {D₀ : Type u_2} {C₁ : Type u_3} {D₁ : Type u_4} {C₂ : Type u_5} {D₂ : Type u_6} [Category.{u_7, u_1} C₀] [Category.{u_8, u_2} D₀] [Category.{u_9, u_3} C₁] [Category.{u_10, u_4} D₁] [Category.{u_11, u_5} C₂] [Category.{u_12, u_6} D₂] (E₀ : C₀ ≌ D₀) (E₁ : C₁ ≌ D₁) (E₂ : C₂ ≌ D₂) (F : Functor C₀ C₁) (G : Functor C₁ C₂) (H : Functor C₀ C₂) (e : F.comp G ≅ H) : (equivalenceTransportFunctor E₀ E₁ F).comp (equivalenceTransportFunctor E₁ E₂ G) ≅ equivalenceTransportFunctor E₀ E₂ H

A compositor is transported through objectwise equivalences.

Equations

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

def CategoryTheory.Pseudofunctor.equivalenceTransportIdIso {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (E : C ≌ D) (F G : Functor C C) (e₀ : F ≅ G) (e₁ : G ≅ Functor.id C) : equivalenceTransportFunctor E E F ≅ Functor.id D

A two-stage comparison with the identity is transported through an equivalence.

Equations

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

theorem CategoryTheory.Pseudofunctor.equivalenceTransport_associativity {C₀ : Type u_1} {D₀ : Type u_2} {C₁ : Type u_3} {D₁ : Type u_4} {C₂ : Type u_5} {D₂ : Type u_6} {C₃ : Type u_7} {D₃ : Type u_8} [Category.{u_9, u_1} C₀] [Category.{u_10, u_2} D₀] [Category.{u_11, u_3} C₁] [Category.{u_12, u_4} D₁] [Category.{u_13, u_5} C₂] [Category.{u_14, u_6} D₂] [Category.{u_15, u_7} C₃] [Category.{u_16, u_8} D₃] (E₀ : C₀ ≌ D₀) (E₁ : C₁ ≌ D₁) (E₂ : C₂ ≌ D₂) (E₃ : C₃ ≌ D₃) (F₀₁ : Functor C₀ C₁) (F₁₂ : Functor C₁ C₂) (F₂₃ : Functor C₂ C₃) (F₀₂ : Functor C₀ C₂) (F₁₃ : Functor C₁ C₃) (F₀₃ : Functor C₀ C₃) (c₀₁₂ : F₀₁.comp F₁₂ ≅ F₀₂) (c₁₂₃ : F₁₂.comp F₂₃ ≅ F₁₃) (c₀₂₃ : F₀₂.comp F₂₃ ≅ F₀₃) (c₀₁₃ : F₀₁.comp F₁₃ ≅ F₀₃) (hassoc : CategoryStruct.comp c₀₂₃.symm.hom (CategoryStruct.comp (Functor.whiskerRight c₀₁₂.symm.hom F₂₃) (CategoryStruct.comp (F₀₁.associator F₁₂ F₂₃).hom (CategoryStruct.comp (F₀₁.whiskerLeft c₁₂₃.hom) c₀₁₃.hom))) = CategoryStruct.id F₀₃) : CategoryStruct.comp (equivalenceTransportCompIso E₀ E₂ E₃ F₀₂ F₂₃ F₀₃ c₀₂₃).symm.hom (CategoryStruct.comp (Functor.whiskerRight (equivalenceTransportCompIso E₀ E₁ E₂ F₀₁ F₁₂ F₀₂ c₀₁₂).symm.hom (equivalenceTransportFunctor E₂ E₃ F₂₃)) (CategoryStruct.comp ((equivalenceTransportFunctor E₀ E₁ F₀₁).associator (equivalenceTransportFunctor E₁ E₂ F₁₂) (equivalenceTransportFunctor E₂ E₃ F₂₃)).hom (CategoryStruct.comp ((equivalenceTransportFunctor E₀ E₁ F₀₁).whiskerLeft (equivalenceTransportCompIso E₁ E₂ E₃ F₁₂ F₂₃ F₁₃ c₁₂₃).hom) (equivalenceTransportCompIso E₀ E₁ E₃ F₀₁ F₁₃ F₀₃ c₀₁₃).hom))) = CategoryStruct.id (equivalenceTransportFunctor E₀ E₃ F₀₃)

The transported compositors satisfy the pentagon equation whenever the original compositors do.

theorem CategoryTheory.Pseudofunctor.equivalenceTransport_leftUnitality {C₀ : Type u_1} {D₀ : Type u_2} {C₁ : Type u_3} {D₁ : Type u_4} [Category.{u_5, u_1} C₀] [Category.{u_6, u_2} D₀] [Category.{u_7, u_3} C₁] [Category.{u_8, u_4} D₁] (E₀ : C₀ ≌ D₀) (E₁ : C₁ ≌ D₁) (Fid Gid : Functor C₀ C₀) (F : Functor C₀ C₁) (e₀ : Fid ≅ Gid) (e₁ : Gid ≅ Functor.id C₀) (c : Fid.comp F ≅ F) (hleft : CategoryStruct.comp c.symm.hom (CategoryStruct.comp (Functor.whiskerRight (e₀ ≪≫ e₁).hom F) F.leftUnitor.hom) = CategoryStruct.id F) : CategoryStruct.comp (equivalenceTransportCompIso E₀ E₀ E₁ Fid F F c).symm.hom (CategoryStruct.comp (Functor.whiskerRight (equivalenceTransportIdIso E₀ Fid Gid e₀ e₁).hom (equivalenceTransportFunctor E₀ E₁ F)) (equivalenceTransportFunctor E₀ E₁ F).leftUnitor.hom) = CategoryStruct.id (equivalenceTransportFunctor E₀ E₁ F)

The transported unit and compositor satisfy the left triangle equation whenever the original comparisons do.

theorem CategoryTheory.Pseudofunctor.equivalenceTransport_rightUnitality {C₀ : Type u_1} {D₀ : Type u_2} {C₁ : Type u_3} {D₁ : Type u_4} [Category.{u_5, u_1} C₀] [Category.{u_6, u_2} D₀] [Category.{u_7, u_3} C₁] [Category.{u_8, u_4} D₁] (E₀ : C₀ ≌ D₀) (E₁ : C₁ ≌ D₁) (F : Functor C₀ C₁) (Fid Gid : Functor C₁ C₁) (e₀ : Fid ≅ Gid) (e₁ : Gid ≅ Functor.id C₁) (c : F.comp Fid ≅ F) (hright : CategoryStruct.comp c.symm.hom (CategoryStruct.comp (F.whiskerLeft (e₀ ≪≫ e₁).hom) F.rightUnitor.hom) = CategoryStruct.id F) : CategoryStruct.comp (equivalenceTransportCompIso E₀ E₁ E₁ F Fid F c).symm.hom (CategoryStruct.comp ((equivalenceTransportFunctor E₀ E₁ F).whiskerLeft (equivalenceTransportIdIso E₁ Fid Gid e₀ e₁).hom) (equivalenceTransportFunctor E₀ E₁ F).rightUnitor.hom) = CategoryStruct.id (equivalenceTransportFunctor E₀ E₁ F)

The transported unit and compositor satisfy the right triangle equation whenever the original comparisons do.