Pseudofunctoriality of categorical joins #
In this file, we promote the join construction to two pseudofunctors
Join.pseudofunctorLeft
and Join.pseudoFunctorRight
, expressing its pseudofunctoriality in
each variable.
def
CategoryTheory.Join.mapCompRight
(A : Type u_1)
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[Category.{u_5, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
[Category.{u_8, u_4} D]
(F : Functor B C)
(G : Functor C D)
:
The structural isomorphism for composition of pseudoFunctorRight
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Join.mapCompLeft
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
(D : Type u_4)
[Category.{u_5, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
[Category.{u_8, u_4} D]
(F : Functor A B)
(G : Functor B C)
:
The structural isomorphism for composition of pseudoFunctorLeft
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Join.mapWhiskerLeft_whiskerLeft
(A : Type u_1)
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[Category.{u_8, u_1} A]
[Category.{u_5, u_2} B]
[Category.{u_6, u_3} C]
[Category.{u_7, u_4} D]
(F : Functor B C)
{G H : Functor C D}
(η : G ⟶ H)
:
mapWhiskerLeft (Functor.id A) (whiskerLeft F η) = CategoryStruct.comp (mapCompRight A F G).hom
(CategoryStruct.comp (whiskerLeft (mapPair (Functor.id A) F) (mapWhiskerLeft (Functor.id A) η))
(mapCompRight A F H).inv)
theorem
CategoryTheory.Join.mapWhiskerLeft_whiskerLeft_assoc
(A : Type u_1)
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[Category.{u_8, u_1} A]
[Category.{u_5, u_2} B]
[Category.{u_6, u_3} C]
[Category.{u_7, u_4} D]
(F : Functor B C)
{G H : Functor C D}
(η : G ⟶ H)
{Z : Functor (Join A B) (Join A D)}
(h : mapPair (Functor.id A) (F.comp H) ⟶ Z)
:
CategoryStruct.comp (mapWhiskerLeft (Functor.id A) (whiskerLeft F η)) h = CategoryStruct.comp (mapCompRight A F G).hom
(CategoryStruct.comp (whiskerLeft (mapPair (Functor.id A) F) (mapWhiskerLeft (Functor.id A) η))
(CategoryStruct.comp (mapCompRight A F H).inv h))
theorem
CategoryTheory.Join.mapWhiskerRight_whiskerLeft
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
(D : Type u_4)
[Category.{u_5, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
[Category.{u_8, u_4} D]
(F : Functor A B)
{G H : Functor B C}
(η : G ⟶ H)
:
mapWhiskerRight (whiskerLeft F η) (Functor.id D) = CategoryStruct.comp (mapCompLeft D F G).hom
(CategoryStruct.comp (whiskerLeft (mapPair F (Functor.id D)) (mapWhiskerRight η (Functor.id D)))
(mapCompLeft D F H).inv)
theorem
CategoryTheory.Join.mapWhiskerRight_whiskerLeft_assoc
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
(D : Type u_4)
[Category.{u_5, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
[Category.{u_8, u_4} D]
(F : Functor A B)
{G H : Functor B C}
(η : G ⟶ H)
{Z : Functor (Join A D) (Join C D)}
(h : mapPair (F.comp H) (Functor.id D) ⟶ Z)
:
CategoryStruct.comp (mapWhiskerRight (whiskerLeft F η) (Functor.id D)) h = CategoryStruct.comp (mapCompLeft D F G).hom
(CategoryStruct.comp (whiskerLeft (mapPair F (Functor.id D)) (mapWhiskerRight η (Functor.id D)))
(CategoryStruct.comp (mapCompLeft D F H).inv h))
theorem
CategoryTheory.Join.mapWhiskerLeft_whiskerRight
(A : Type u_1)
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[Category.{u_8, u_1} A]
[Category.{u_5, u_2} B]
[Category.{u_6, u_3} C]
[Category.{u_7, u_4} D]
{F G : Functor B C}
(η : F ⟶ G)
(H : Functor C D)
:
mapWhiskerLeft (Functor.id A) (whiskerRight η H) = CategoryStruct.comp (mapCompRight A F H).hom
(CategoryStruct.comp (whiskerRight (mapWhiskerLeft (Functor.id A) η) (mapPair (Functor.id A) H))
(mapCompRight A G H).inv)
theorem
CategoryTheory.Join.mapWhiskerLeft_whiskerRight_assoc
(A : Type u_1)
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[Category.{u_8, u_1} A]
[Category.{u_5, u_2} B]
[Category.{u_6, u_3} C]
[Category.{u_7, u_4} D]
{F G : Functor B C}
(η : F ⟶ G)
(H : Functor C D)
{Z : Functor (Join A B) (Join A D)}
(h : mapPair (Functor.id A) (G.comp H) ⟶ Z)
:
CategoryStruct.comp (mapWhiskerLeft (Functor.id A) (whiskerRight η H)) h = CategoryStruct.comp (mapCompRight A F H).hom
(CategoryStruct.comp (whiskerRight (mapWhiskerLeft (Functor.id A) η) (mapPair (Functor.id A) H))
(CategoryStruct.comp (mapCompRight A G H).inv h))
theorem
CategoryTheory.Join.mapWhiskerRight_whiskerRight
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
(D : Type u_4)
[Category.{u_5, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
[Category.{u_8, u_4} D]
{F G : Functor A B}
(η : F ⟶ G)
(H : Functor B C)
:
mapWhiskerRight (whiskerRight η H) (Functor.id D) = CategoryStruct.comp (mapCompLeft D F H).hom
(CategoryStruct.comp (whiskerRight (mapWhiskerRight η (Functor.id D)) (mapPair H (Functor.id D)))
(mapCompLeft D G H).inv)
theorem
CategoryTheory.Join.mapWhiskerRight_whiskerRight_assoc
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
(D : Type u_4)
[Category.{u_5, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
[Category.{u_8, u_4} D]
{F G : Functor A B}
(η : F ⟶ G)
(H : Functor B C)
{Z : Functor (Join A D) (Join C D)}
(h : mapPair (G.comp H) (Functor.id D) ⟶ Z)
:
CategoryStruct.comp (mapWhiskerRight (whiskerRight η H) (Functor.id D)) h = CategoryStruct.comp (mapCompLeft D F H).hom
(CategoryStruct.comp (whiskerRight (mapWhiskerRight η (Functor.id D)) (mapPair H (Functor.id D)))
(CategoryStruct.comp (mapCompLeft D G H).inv h))
theorem
CategoryTheory.Join.mapWhiskerLeft_associator_hom
(A : Type u_1)
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[Category.{u_10, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
[Category.{u_8, u_4} D]
{E : Type u_5}
[Category.{u_9, u_5} E]
(F : Functor B C)
(G : Functor C D)
(H : Functor D E)
:
mapWhiskerLeft (Functor.id A) (F.associator G H).hom = CategoryStruct.comp (mapCompRight A (F.comp G) H).hom
(CategoryStruct.comp (whiskerRight (mapCompRight A F G).hom (mapPair (Functor.id A) H))
(CategoryStruct.comp
((mapPair (Functor.id A) F).associator (mapPair (Functor.id A) G) (mapPair (Functor.id A) H)).hom
(CategoryStruct.comp (whiskerLeft (mapPair (Functor.id A) F) (mapCompRight A G H).inv)
(mapCompRight A F (G.comp H)).inv)))
theorem
CategoryTheory.Join.mapWhiskerLeft_associator_hom_assoc
(A : Type u_1)
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[Category.{u_10, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
[Category.{u_8, u_4} D]
{E : Type u_5}
[Category.{u_9, u_5} E]
(F : Functor B C)
(G : Functor C D)
(H : Functor D E)
{Z : Functor (Join A B) (Join A E)}
(h : mapPair (Functor.id A) (F.comp (G.comp H)) ⟶ Z)
:
CategoryStruct.comp (mapWhiskerLeft (Functor.id A) (F.associator G H).hom) h = CategoryStruct.comp (mapCompRight A (F.comp G) H).hom
(CategoryStruct.comp (whiskerRight (mapCompRight A F G).hom (mapPair (Functor.id A) H))
(CategoryStruct.comp
((mapPair (Functor.id A) F).associator (mapPair (Functor.id A) G) (mapPair (Functor.id A) H)).hom
(CategoryStruct.comp (whiskerLeft (mapPair (Functor.id A) F) (mapCompRight A G H).inv)
(CategoryStruct.comp (mapCompRight A F (G.comp H)).inv h))))
theorem
CategoryTheory.Join.mapWhiskerRight_associator_hom
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[Category.{u_6, u_1} A]
[Category.{u_7, u_2} B]
[Category.{u_8, u_3} C]
[Category.{u_9, u_4} D]
(E : Type u_5)
[Category.{u_10, u_5} E]
(F : Functor A B)
(G : Functor B C)
(H : Functor C D)
:
mapWhiskerRight (F.associator G H).hom (Functor.id E) = CategoryStruct.comp (mapCompLeft E (F.comp G) H).hom
(CategoryStruct.comp (whiskerRight (mapCompLeft E F G).hom (mapPair H (Functor.id E)))
(CategoryStruct.comp
((mapPair F (Functor.id E)).associator (mapPair G (Functor.id E)) (mapPair H (Functor.id E))).hom
(CategoryStruct.comp (whiskerLeft (mapPair F (Functor.id E)) (mapCompLeft E G H).inv)
(mapCompLeft E F (G.comp H)).inv)))
theorem
CategoryTheory.Join.mapWhiskerLeft_leftUnitor_hom
(A : Type u_1)
{B : Type u_2}
{C : Type u_3}
[Category.{u_8, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
(F : Functor B C)
:
mapWhiskerLeft (Functor.id A) F.leftUnitor.hom = CategoryStruct.comp (mapCompRight A (Functor.id B) F).hom
(CategoryStruct.comp (whiskerRight mapPairId.hom (mapPair (Functor.id A) F))
(mapPair (Functor.id A) F).leftUnitor.hom)
theorem
CategoryTheory.Join.mapWhiskerRight_leftUnitor_hom
{A : Type u_1}
{B : Type u_2}
(C : Type u_3)
[Category.{u_6, u_1} A]
[Category.{u_7, u_2} B]
[Category.{u_8, u_3} C]
(F : Functor A B)
:
mapWhiskerRight F.leftUnitor.hom (Functor.id C) = CategoryStruct.comp (mapCompLeft C (Functor.id A) F).hom
(CategoryStruct.comp (whiskerRight mapPairId.hom (mapPair F (Functor.id C)))
(mapPair F (Functor.id C)).leftUnitor.hom)
theorem
CategoryTheory.Join.mapWhiskerLeft_rightUnitor_hom
(A : Type u_1)
{B : Type u_2}
{C : Type u_3}
[Category.{u_8, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
(F : Functor B C)
:
mapWhiskerLeft (Functor.id A) F.rightUnitor.hom = CategoryStruct.comp (mapCompRight A F (Functor.id C)).hom
(CategoryStruct.comp (whiskerLeft (mapPair (Functor.id A) F) mapPairId.hom)
(mapPair (Functor.id A) F).rightUnitor.hom)
theorem
CategoryTheory.Join.mapWhiskerRight_rightUnitor_hom
{A : Type u_1}
{B : Type u_2}
(C : Type u_3)
[Category.{u_6, u_1} A]
[Category.{u_7, u_2} B]
[Category.{u_8, u_3} C]
(F : Functor A B)
:
mapWhiskerRight F.rightUnitor.hom (Functor.id C) = CategoryStruct.comp (mapCompLeft C F (Functor.id B)).hom
(CategoryStruct.comp (whiskerLeft (mapPair F (Functor.id C)) mapPairId.hom)
(mapPair F (Functor.id C)).rightUnitor.hom)
The pseudofunctor sending D
to C ⋆ D
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Join.pseudofunctorRight_mapId_hom_app
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Cat)
(x : Join C ↑D)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Cat)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_obj
(C : Type u₁)
[Category.{v₁, u₁} C]
{X✝ Y✝ : Cat}
(F : X✝ ⟶ Y✝)
(X : Join C ↑X✝)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorRight_mapComp_inv_app
(C : Type u₁)
[Category.{v₁, u₁} C]
{a✝ b✝ c✝ : Cat}
(F : Functor ↑a✝ ↑b✝)
(G : Functor ↑b✝ ↑c✝)
(X : Join C ↑a✝)
:
((pseudofunctorRight C).mapComp F G).inv.app X = comp ((mapPairComp (Functor.id C) F (Functor.id C) G).inv.app X)
(match X with
| left x => (left x).id
| right x => (right (G.obj (F.obj x))).id)
@[simp]
theorem
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_map
(C : Type u₁)
[Category.{v₁, u₁} C]
{X✝ Y✝ : Cat}
(F : X✝ ⟶ Y✝)
{X✝¹ Y✝¹ : Join C ↑X✝}
(f : X✝¹ ⟶ Y✝¹)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Cat)
{X✝ Y✝ Z✝ : Join C ↑D}
(a✝ : X✝.Hom Y✝)
(a✝¹ : Y✝.Hom Z✝)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorRight_mapId_inv_app
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Cat)
(x : Join C ↑D)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorRight_mapComp_hom_app
(C : Type u₁)
[Category.{v₁, u₁} C]
{a✝ b✝ c✝ : Cat}
(F : Functor ↑a✝ ↑b✝)
(G : Functor ↑b✝ ↑c✝)
(X : Join C ↑a✝)
:
((pseudofunctorRight C).mapComp F G).hom.app X = comp
(match X with
| left x => (left x).id
| right x => (right (G.obj (F.obj x))).id)
((mapPairComp (Functor.id C) F (Functor.id C) G).hom.app X)
@[simp]
theorem
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Cat)
(x✝ : Join C ↑D)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_app
(C : Type u₁)
[Category.{v₁, u₁} C]
{a✝ b✝ : Cat}
{f✝ g✝ : a✝ ⟶ b✝}
(α : f✝ ⟶ g✝)
(x : Join C ↑a✝)
:
The pseudofunctor sending C
to C ⋆ D
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id
(D : Type u₂)
[Category.{v₂, u₂} D]
(C : Cat)
(x✝ : Join (↑C) D)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_map
(D : Type u₂)
[Category.{v₂, u₂} D]
{X✝ Y✝ : Cat}
(F : X✝ ⟶ Y✝)
{X✝¹ Y✝¹ : Join (↑X✝) D}
(f : X✝¹ ⟶ Y✝¹)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorLeft_mapId_hom_app
(D : Type u₂)
[Category.{v₂, u₂} D]
(D✝ : Cat)
(x : Join (↑D✝) D)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp
(D : Type u₂)
[Category.{v₂, u₂} D]
(C : Cat)
{X✝ Y✝ Z✝ : Join (↑C) D}
(a✝ : X✝.Hom Y✝)
(a✝¹ : Y✝.Hom Z✝)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_obj
(D : Type u₂)
[Category.{v₂, u₂} D]
{X✝ Y✝ : Cat}
(F : X✝ ⟶ Y✝)
(X : Join (↑X✝) D)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_app
(D : Type u₂)
[Category.{v₂, u₂} D]
{a✝ b✝ c✝ : Cat}
(F : Functor ↑a✝ ↑b✝)
(G : Functor ↑b✝ ↑c✝)
(X : Join (↑a✝) D)
:
((pseudofunctorLeft D).mapComp F G).inv.app X = comp ((mapPairComp F (Functor.id D) G (Functor.id D)).inv.app X)
(match X with
| left x => (left (G.obj (F.obj x))).id
| right x => (right x).id)
@[simp]
theorem
CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_app
(D : Type u₂)
[Category.{v₂, u₂} D]
{a✝ b✝ c✝ : Cat}
(F : Functor ↑a✝ ↑b✝)
(G : Functor ↑b✝ ↑c✝)
(X : Join (↑a✝) D)
:
((pseudofunctorLeft D).mapComp F G).hom.app X = comp
(match X with
| left x => (left (G.obj (F.obj x))).id
| right x => (right x).id)
((mapPairComp F (Functor.id D) G (Functor.id D)).hom.app X)
@[simp]
theorem
CategoryTheory.Join.pseudofunctorLeft_mapId_inv_app
(D : Type u₂)
[Category.{v₂, u₂} D]
(D✝ : Cat)
(x : Join (↑D✝) D)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_app
(D : Type u₂)
[Category.{v₂, u₂} D]
{a✝ b✝ : Cat}
{f✝ g✝ : a✝ ⟶ b✝}
(x✝ : f✝ ⟶ g✝)
(x : Join (↑a✝) D)
:
@[simp]
theorem
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α
(D : Type u₂)
[Category.{v₂, u₂} D]
(C : Cat)
: