Pseudofunctors to Cat #
In this file, we state naturality properties of mapId' and mapComp'
for pseudofunctors to Cat.
theorem
CategoryTheory.Pseudofunctor.mapId'_hom_naturality
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₀)
(hf : f = CategoryStruct.id b₀)
(a : X ⟶ Y)
:
CategoryStruct.comp ((F.map f).toFunctor.map a) ((F.mapId' f hf).hom.toNatTrans.app Y) = CategoryStruct.comp ((F.mapId' f hf).hom.toNatTrans.app X) a
theorem
CategoryTheory.Pseudofunctor.mapId'_hom_naturality_assoc
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₀)
(hf : f = CategoryStruct.id b₀)
(a : X ⟶ Y)
{Z : ↑(F.obj b₀)}
(h : (CategoryStruct.id (F.obj b₀)).toFunctor.obj Y ⟶ Z)
:
CategoryStruct.comp ((F.map f).toFunctor.map a) (CategoryStruct.comp ((F.mapId' f hf).hom.toNatTrans.app Y) h) = CategoryStruct.comp ((F.mapId' f hf).hom.toNatTrans.app X) (CategoryStruct.comp a h)
theorem
CategoryTheory.Pseudofunctor.mapId'_inv_naturality
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₀)
(hf : f = CategoryStruct.id b₀)
(a : X ⟶ Y)
:
CategoryStruct.comp ((F.mapId' f hf).inv.toNatTrans.app X) ((F.map f).toFunctor.map a) = CategoryStruct.comp a ((F.mapId' f hf).inv.toNatTrans.app Y)
theorem
CategoryTheory.Pseudofunctor.mapId'_inv_naturality_assoc
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₀)
(hf : f = CategoryStruct.id b₀)
(a : X ⟶ Y)
{Z : ↑(F.obj b₀)}
(h : (F.map f).toFunctor.obj Y ⟶ Z)
:
CategoryStruct.comp ((F.mapId' f hf).inv.toNatTrans.app X) (CategoryStruct.comp ((F.map f).toFunctor.map a) h) = CategoryStruct.comp a (CategoryStruct.comp ((F.mapId' f hf).inv.toNatTrans.app Y) h)
theorem
CategoryTheory.Pseudofunctor.mapComp'_hom_naturality
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(fg : b₀ ⟶ b₂)
(hfg : CategoryStruct.comp f g = fg)
(a : X ⟶ Y)
:
CategoryStruct.comp ((F.map fg).toFunctor.map a) ((F.mapComp' f g fg hfg).hom.toNatTrans.app Y) = CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app X)
((F.map g).toFunctor.map ((F.map f).toFunctor.map a))
theorem
CategoryTheory.Pseudofunctor.mapComp'_hom_naturality_assoc
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(fg : b₀ ⟶ b₂)
(hfg : CategoryStruct.comp f g = fg)
(a : X ⟶ Y)
{Z : ↑(F.obj b₂)}
(h : (CategoryStruct.comp (F.map f) (F.map g)).toFunctor.obj Y ⟶ Z)
:
CategoryStruct.comp ((F.map fg).toFunctor.map a)
(CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app Y) h) = CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app X)
(CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a)) h)
@[simp]
theorem
CategoryTheory.Pseudofunctor.mapComp'_inv_naturality
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(fg : b₀ ⟶ b₂)
(hfg : CategoryStruct.comp f g = fg)
(a : X ⟶ Y)
:
CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a))
((F.mapComp' f g fg hfg).inv.toNatTrans.app Y) = CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app X) ((F.map fg).toFunctor.map a)
@[simp]
theorem
CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(fg : b₀ ⟶ b₂)
(hfg : CategoryStruct.comp f g = fg)
(a : X ⟶ Y)
{Z : ↑(F.obj b₂)}
(h : (F.map fg).toFunctor.obj Y ⟶ Z)
:
CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a))
(CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app Y) h) = CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app X)
(CategoryStruct.comp ((F.map fg).toFunctor.map a) h)
theorem
CategoryTheory.Pseudofunctor.mapComp'_naturality_1
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(fg : b₀ ⟶ b₂)
(hfg : CategoryStruct.comp f g = fg)
(a : X ⟶ Y)
:
CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app X)
(CategoryStruct.comp ((F.map fg).toFunctor.map a) ((F.mapComp' f g fg hfg).hom.toNatTrans.app Y)) = (F.map g).toFunctor.map ((F.map f).toFunctor.map a)
theorem
CategoryTheory.Pseudofunctor.mapComp'_naturality_1_assoc
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(fg : b₀ ⟶ b₂)
(hfg : CategoryStruct.comp f g = fg)
(a : X ⟶ Y)
{Z : ↑(F.obj b₂)}
(h : (CategoryStruct.comp (F.map f) (F.map g)).toFunctor.obj Y ⟶ Z)
:
CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app X)
(CategoryStruct.comp ((F.map fg).toFunctor.map a)
(CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app Y) h)) = CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a)) h
theorem
CategoryTheory.Pseudofunctor.mapComp'_naturality_2
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(fg : b₀ ⟶ b₂)
(hfg : CategoryStruct.comp f g = fg)
(a : X ⟶ Y)
:
CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app X)
(CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a))
((F.mapComp' f g fg hfg).inv.toNatTrans.app Y)) = (F.map fg).toFunctor.map a
theorem
CategoryTheory.Pseudofunctor.mapComp'_naturality_2_assoc
{B : Type u}
[Bicategory B]
(F : Pseudofunctor B Cat)
{b₀ b₁ b₂ : B}
{X Y : ↑(F.obj b₀)}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(fg : b₀ ⟶ b₂)
(hfg : CategoryStruct.comp f g = fg)
(a : X ⟶ Y)
{Z : ↑(F.obj b₂)}
(h : (F.map fg).toFunctor.obj Y ⟶ Z)
:
CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app X)
(CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a))
(CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app Y) h)) = CategoryStruct.comp ((F.map fg).toFunctor.map a) h