Documentation

Mathlib.CategoryTheory.Bicategory.Functor.Strict

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).

source
theorem CategoryTheory.Pseudofunctor.mapComp'_comp_id {B : Type u_1} {C : Type u_2} [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
source
theorem CategoryTheory.Pseudofunctor.mapComp'_id_comp {B : Type u_1} {C : Type u_2} [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)
source
theorem CategoryTheory.Pseudofunctor.mapComp'_hom_comp_whiskerLeft_mapComp'_hom {B : Type u_1} {C : Type u_2} [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₁₃ h₁₃).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)
source
theorem CategoryTheory.Pseudofunctor.mapComp'_hom_comp_whiskerLeft_mapComp'_hom_assoc {B : Type u_1} {C : Type u_2} [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₁₃ h₁₃).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))
source
theorem CategoryTheory.Pseudofunctor.mapComp'_inv_comp_mapComp'_hom {B : Type u_1} {C : Type u_2} [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₂₃)))
source
theorem CategoryTheory.Pseudofunctor.mapComp'_inv_comp_mapComp'_hom_assoc {B : Type u_1} {C : Type u_2} [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))
source
theorem CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'_inv {B : Type u_1} {C : Type u_2} [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)
source
theorem CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'_inv_assoc {B : Type u_1} {C : Type u_2} [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))
source
theorem CategoryTheory.Pseudofunctor.mapComp'_hom_comp_mapComp'_hom_whiskerRight {B : Type u_1} {C : Type u_2} [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)
source
theorem CategoryTheory.Pseudofunctor.mapComp'_hom_comp_mapComp'_hom_whiskerRight_assoc {B : Type u_1} {C : Type u_2} [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))
source
theorem CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv {B : Type u_1} {C : Type u_2} [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)
source
theorem CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv_assoc {B : Type u_1} {C : Type u_2} [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))
source
def CategoryTheory.Pseudofunctor.isoMapOfCommSq {B : Type u_1} {C : Type u_2} [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) :
CategoryStruct.comp (F.map t) (F.map r) ≅ CategoryStruct.comp (F.map l) (F.map 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
Instances For
    source
    theorem CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq {B : Type u_1} {C : Type u_2} [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 = φ) :
    F.isoMapOfCommSq sq = (F.mapComp' t r φ ⋯).symm ≪≫ F.mapComp' l b φ ⋯
    source
    theorem CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id {B : Type u_1} {C : Type u_2} [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.

    source
    theorem CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id {B : Type u_1} {C : Type u_2} [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.