Pseudofunctors from strict bicategory #
This file provides an API for pseudofunctors F from a strict bicategory B. In
particular, this shall apply to pseudofunctors from locally discrete bicategories.
Firstly, we study the compatibilities of the flexible variants mapId' and mapComp'
of mapId and mapComp with respect to the composition with identities and the
associativity.
Secondly, given a commutative square t ≫ r = l ≫ b in B, we construct an
isomorphism F.map t ≫ F.map r ≅ F.map l ≫ F.map b
(see Pseudofunctor.isoMapOfCommSq).
theorem
CategoryTheory.Pseudofunctor.mapComp'_comp_id
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
:
F.mapComp' f (CategoryStruct.id b₁) f ⋯ = (Bicategory.rightUnitor (F.map f)).symm ≪≫ Bicategory.whiskerLeftIso (F.map f) (F.mapId b₁).symm
theorem
CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
:
(F.mapComp' f (CategoryStruct.id b₁) f ⋯).hom = CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).inv (Bicategory.whiskerLeft (F.map f) (F.mapId b₁).inv)
theorem
CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₁)}
(h : (CategoryStruct.comp (F.map f) (F.map (CategoryStruct.id b₁))).obj X ⟶ Z)
:
CategoryStruct.comp ((F.mapComp' f (CategoryStruct.id b₁) f ⋯).hom.app X) h = CategoryStruct.comp ((F.mapId b₁).inv.app ((F.map f).obj X)) h
theorem
CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
{Z : F.obj b₀ ⟶ F.obj b₁}
(h : CategoryStruct.comp (F.map f) (F.map (CategoryStruct.id b₁)) ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f (CategoryStruct.id b₁) f ⋯).hom h = CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).inv
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapId b₁).inv) h)
theorem
CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
:
(F.mapComp' f (CategoryStruct.id b₁) f ⋯).inv = CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapId b₁).hom) (Bicategory.rightUnitor (F.map f)).hom
theorem
CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
{Z : F.obj b₀ ⟶ F.obj b₁}
(h : F.map f ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f (CategoryStruct.id b₁) f ⋯).inv h = CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapId b₁).hom)
(CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).hom h)
theorem
CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₁)}
(h : (F.map f).obj X ⟶ Z)
:
CategoryStruct.comp ((F.mapComp' f (CategoryStruct.id b₁) f ⋯).inv.app X) h = CategoryStruct.comp ((F.mapId b₁).hom.app ((F.map f).obj X)) h
theorem
CategoryTheory.Pseudofunctor.mapComp'_id_comp
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
:
F.mapComp' (CategoryStruct.id b₀) f f ⋯ = (Bicategory.leftUnitor (F.map f)).symm ≪≫ Bicategory.whiskerRightIso (F.mapId b₀).symm (F.map f)
theorem
CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
:
(F.mapComp' (CategoryStruct.id b₀) f f ⋯).hom = CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).inv (Bicategory.whiskerRight (F.mapId b₀).inv (F.map f))
theorem
CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₁)}
(h : (CategoryStruct.comp (F.map (CategoryStruct.id b₀)) (F.map f)).obj X ⟶ Z)
:
CategoryStruct.comp ((F.mapComp' (CategoryStruct.id b₀) f f ⋯).hom.app X) h = CategoryStruct.comp ((F.map f).map ((F.mapId b₀).inv.app X)) h
theorem
CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
{Z : F.obj b₀ ⟶ F.obj b₁}
(h : CategoryStruct.comp (F.map (CategoryStruct.id b₀)) (F.map f) ⟶ Z)
:
CategoryStruct.comp (F.mapComp' (CategoryStruct.id b₀) f f ⋯).hom h = CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).inv
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapId b₀).inv (F.map f)) h)
theorem
CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
:
(F.mapComp' (CategoryStruct.id b₀) f f ⋯).inv = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId b₀).hom (F.map f)) (Bicategory.leftUnitor (F.map f)).hom
theorem
CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₁)}
(h : (F.map f).obj X ⟶ Z)
:
CategoryStruct.comp ((F.mapComp' (CategoryStruct.id b₀) f f ⋯).inv.app X) h = CategoryStruct.comp ((F.map f).map ((F.mapId b₀).hom.app X)) h
theorem
CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ : B}
(f : b₀ ⟶ b₁)
{Z : F.obj b₀ ⟶ F.obj b₁}
(h : F.map f ⟶ Z)
:
CategoryStruct.comp (F.mapComp' (CategoryStruct.id b₀) f f ⋯).inv h = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId b₀).hom (F.map f))
(CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).hom h)
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
:
CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom) = CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
(Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom)
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : CategoryStruct.comp (F.map f₀₁) (CategoryStruct.comp (F.map f₁₂) (F.map f₂₃)) ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom) h) = CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom h))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₃)}
(h : (F.map f₂₃).obj ((F.map f₁₂).obj ((F.map f₀₁).obj X)) ⟶ Z)
:
@[deprecated CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom (since := "2025-10-02")]
theorem
CategoryTheory.Pseudofunctor.mapComp'_hom_comp_whiskerLeft_mapComp'_hom
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
:
CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom) = CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
(Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom)
Alias of CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom.
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
:
CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv (F.mapComp' f₀₂ f₂₃ f ⋯).hom = CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₃)}
(h : (F.map f₂₃).obj ((F.map f₀₂).obj X) ⟶ Z)
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : CategoryStruct.comp (F.map f₀₂) (F.map f₂₃) ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv (CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom h) = CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) h))
@[deprecated CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom (since := "2025-10-02")]
theorem
CategoryTheory.Pseudofunctor.mapComp'_inv_comp_mapComp'_hom
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
:
CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv (F.mapComp' f₀₂ f₂₃ f ⋯).hom = CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)))
Alias of CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom.
theorem
CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
:
CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
(F.mapComp' f₀₁ f₁₃ f hf).inv = CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
(F.mapComp' f₀₂ f₂₃ f ⋯).inv)
theorem
CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₃)}
(h : (F.map f).obj X ⟶ Z)
:
theorem
CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : F.map f ⟶ Z)
:
CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
(CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f hf).inv h) = CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
(CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h))
@[deprecated CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv (since := "2025-10-02")]
theorem
CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'_inv
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
:
CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
(F.mapComp' f₀₁ f₁₃ f hf).inv = CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
(F.mapComp' f₀₂ f₂₃ f ⋯).inv)
Alias of CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv.
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
:
CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
(Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) = CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
(Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv)
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₃)}
(h : (F.map f₂₃).obj ((F.map f₁₂).obj ((F.map f₀₁).obj X)) ⟶ Z)
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : CategoryStruct.comp (CategoryStruct.comp (F.map f₀₁) (F.map f₁₂)) (F.map f₂₃) ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) h) = CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv h))
@[deprecated CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight (since := "2025-10-02")]
theorem
CategoryTheory.Pseudofunctor.mapComp'_hom_comp_mapComp'_hom_whiskerRight
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
:
CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
(Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) = CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
(Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv)
Alias of CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight.
theorem
CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
:
CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
(F.mapComp' f₀₂ f₂₃ f ⋯).inv = CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
(F.mapComp' f₀₁ f₁₃ f ⋯).inv)
theorem
CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : F.map f ⟶ Z)
:
CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
(CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h) = CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
(CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv h))
theorem
CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₃)}
(h : (F.map f).obj X ⟶ Z)
:
@[deprecated CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv (since := "2025-10-02")]
theorem
CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
:
CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
(F.mapComp' f₀₂ f₂₃ f ⋯).inv = CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
(F.mapComp' f₀₁ f₁₃ f ⋯).inv)
Alias of CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv.
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
:
(F.mapComp' f₀₁ f₁₃ f ⋯).inv = CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
(F.mapComp' f₀₂ f₂₃ f ⋯).inv))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : F.map f ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv h = CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
(CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h)))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₃)}
(h : (F.map f).obj X ⟶ Z)
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
:
(F.mapComp' f₀₁ f₁₃ f ⋯).hom = CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
(Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : CategoryStruct.comp (F.map f₀₁) (F.map f₁₃) ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom h = CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) h)))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₃)}
(h : (CategoryStruct.comp (F.map f₀₁) (F.map f₁₃)).obj X ⟶ Z)
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
:
(F.mapComp' f₀₂ f₂₃ f ⋯).hom = CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₃)}
(h : (CategoryStruct.comp (F.map f₀₂) (F.map f₂₃)).obj X ⟶ Z)
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : CategoryStruct.comp (F.map f₀₂) (F.map f₂₃) ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom h = CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) h)))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
:
(F.mapComp' f₀₂ f₂₃ f ⋯).inv = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
(F.mapComp' f₀₁ f₁₃ f ⋯).inv))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₃)}
(h : (F.map f).obj X ⟶ Z)
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : F.map f ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
(CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv h)))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
:
CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv (F.mapComp' f₀₁ f₁₃ f ⋯).hom = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
(Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
(X : ↑(F.obj b₀))
:
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : CategoryStruct.comp (F.map f₀₁) (F.map f₁₃) ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv (CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom h) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) h))
theorem
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc
{B : Type u_1}
[Bicategory B]
[Bicategory.Strict B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
(X : ↑(F.obj b₀))
{Z : ↑(F.obj b₃)}
(h : (F.map f₁₃).obj ((F.map f₀₁).obj X) ⟶ Z)
:
def
CategoryTheory.Pseudofunctor.isoMapOfCommSq
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{X₁ X₂ Y₁ Y₂ : B}
{t : X₁ ⟶ Y₁}
{l : X₁ ⟶ X₂}
{r : Y₁ ⟶ Y₂}
{b : X₂ ⟶ Y₂}
(sq : CommSq t l r b)
:
Given a commutative square CommSq t l r b in a strict bicategory B and
a pseudofunctor from B, this is the natural isomorphism
F.map t ≫ F.map r ≅ F.map l ≫ F.map b.
Equations
- F.isoMapOfCommSq sq = (F.mapComp t r).symm ≪≫ F.mapComp' l b (CategoryTheory.CategoryStruct.comp t r) ⋯
Instances For
theorem
CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{X₁ X₂ Y₁ Y₂ : B}
{t : X₁ ⟶ Y₁}
{l : X₁ ⟶ X₂}
{r : Y₁ ⟶ Y₂}
{b : X₂ ⟶ Y₂}
(sq : CommSq t l r b)
(φ : X₁ ⟶ Y₂)
(hφ : CategoryStruct.comp t r = φ)
:
theorem
CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{X₁ X₂ : B}
(f : X₁ ⟶ X₂)
:
F.isoMapOfCommSq ⋯ = Bicategory.whiskerRightIso (F.mapId X₁) (F.map f) ≪≫ Bicategory.leftUnitor (F.map f) ≪≫ (Bicategory.rightUnitor (F.map f)).symm ≪≫ (Bicategory.whiskerLeftIso (F.map f) (F.mapId X₂)).symm
Equational lemma for Pseudofunctor.isoMapOfCommSq when
both vertical maps of the square are the same and horizontal maps are identities.
theorem
CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : Pseudofunctor B C)
{X₁ X₂ : B}
(f : X₁ ⟶ X₂)
:
F.isoMapOfCommSq ⋯ = Bicategory.whiskerLeftIso (F.map f) (F.mapId X₂) ≪≫ Bicategory.rightUnitor (F.map f) ≪≫ (Bicategory.leftUnitor (F.map f)).symm ≪≫ (Bicategory.whiskerRightIso (F.mapId X₁) (F.map f)).symm
Equational lemma for Pseudofunctor.isoMapOfCommSq when
both horizontal maps of the square are the same and vertical maps are identities.
theorem
CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp'
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : LaxFunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
:
CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) (F.mapComp' f₀₁ f₁₃ f hf) = CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) (F.mapComp' f₀₂ f₂₃ f ⋯))
theorem
CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp'_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : LaxFunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : F.map f ⟶ Z)
:
CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃))
(CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f hf) h) = CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃))
(CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯) h))
theorem
CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp'
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : LaxFunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
:
CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) (F.mapComp' f₀₂ f₂₃ f ⋯) = CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) (F.mapComp' f₀₁ f₁₃ f ⋯))
theorem
CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp'_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : LaxFunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : F.map f ⟶ Z)
:
CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃))
(CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯) h) = CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃))
(CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯) h))
theorem
CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : OplaxFunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
:
CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯) (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) = CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯)
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃))
(Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom)
theorem
CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : OplaxFunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₁ f₁₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : CategoryStruct.comp (F.map f₀₁) (CategoryStruct.comp (F.map f₁₂) (F.map f₂₃)) ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯)
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) h) = CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯)
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃))
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom h))
theorem
CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : OplaxFunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
:
CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯) (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) = CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯)
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃))
(Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv)
theorem
CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight_assoc
{B : Type u₁}
{C : Type u₂}
[Bicategory B]
[Bicategory.Strict B]
[Bicategory C]
(F : OplaxFunctor B C)
{b₀ b₁ b₂ b₃ : B}
(f₀₁ : b₀ ⟶ b₁)
(f₁₂ : b₁ ⟶ b₂)
(f₂₃ : b₂ ⟶ b₃)
(f₀₂ : b₀ ⟶ b₂)
(f₁₃ : b₁ ⟶ b₃)
(f : b₀ ⟶ b₃)
(h₀₂ : CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
(h₁₃ : CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
(hf : CategoryStruct.comp f₀₂ f₂₃ = f)
{Z : F.obj b₀ ⟶ F.obj b₃}
(h : CategoryStruct.comp (CategoryStruct.comp (F.map f₀₁) (F.map f₁₂)) (F.map f₂₃) ⟶ Z)
:
CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯)
(CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) h) = CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯)
(CategoryStruct.comp (Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃))
(CategoryStruct.comp (Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv h))