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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, u_4} D] (F : Functor B C) (G : Functor C D) : mapPair (Functor.id A) (F.comp G) ≅ (mapPair (Functor.id A) F).comp (mapPair (Functor.id A) G)

The structural isomorphism for composition of pseudofunctorRight.

def CategoryTheory.Join.mapCompLeft {A : Type u_1} {B : Type u_2} {C : Type u_3} (D : Type u_4) [Category.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, u_4} D] (F : Functor A B) (G : Functor B C) : mapPair (F.comp G) (Functor.id D) ≅ (mapPair F (Functor.id D)).comp (mapPair G (Functor.id D))

The structural isomorphism for composition of pseudofunctorLeft.

theorem CategoryTheory.Join.mapWhiskerLeft_whiskerLeft (A : Type u_1) {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, u_4} D] (F : Functor B C) {G H : Functor C D} (η : G ⟶ H) : mapWhiskerLeft (Functor.id A) (F.whiskerLeft η) = CategoryStruct.comp (mapCompRight A F G).hom (CategoryStruct.comp ((mapPair (Functor.id A) F).whiskerLeft (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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, 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) (F.whiskerLeft η)) h = CategoryStruct.comp (mapCompRight A F G).hom (CategoryStruct.comp ((mapPair (Functor.id A) F).whiskerLeft (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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, u_4} D] (F : Functor A B) {G H : Functor B C} (η : G ⟶ H) : mapWhiskerRight (F.whiskerLeft η) (Functor.id D) = CategoryStruct.comp (mapCompLeft D F G).hom (CategoryStruct.comp ((mapPair F (Functor.id D)).whiskerLeft (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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, 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 (F.whiskerLeft η) (Functor.id D)) h = CategoryStruct.comp (mapCompLeft D F G).hom (CategoryStruct.comp ((mapPair F (Functor.id D)).whiskerLeft (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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, u_4} D] {F G : Functor B C} (η : F ⟶ G) (H : Functor C D) : mapWhiskerLeft (Functor.id A) (Functor.whiskerRight η H) = CategoryStruct.comp (mapCompRight A F H).hom (CategoryStruct.comp (Functor.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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, 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) (Functor.whiskerRight η H)) h = CategoryStruct.comp (mapCompRight A F H).hom (CategoryStruct.comp (Functor.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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, u_4} D] {F G : Functor A B} (η : F ⟶ G) (H : Functor B C) : mapWhiskerRight (Functor.whiskerRight η H) (Functor.id D) = CategoryStruct.comp (mapCompLeft D F H).hom (CategoryStruct.comp (Functor.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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, 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 (Functor.whiskerRight η H) (Functor.id D)) h = CategoryStruct.comp (mapCompLeft D F H).hom (CategoryStruct.comp (Functor.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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, u_4} D] {E : Type u_5} [Category.{v_5, 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 (Functor.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 ((mapPair (Functor.id A) F).whiskerLeft (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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, u_4} D] {E : Type u_5} [Category.{v_5, 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 (Functor.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 ((mapPair (Functor.id A) F).whiskerLeft (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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, u_3} C] [Category.{v_4, u_4} D] (E : Type u_5) [Category.{v_5, 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 (Functor.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 ((mapPair F (Functor.id E)).whiskerLeft (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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, 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 (Functor.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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, 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 (Functor.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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, 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 ((mapPair (Functor.id A) F).whiskerLeft 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.{v_1, u_1} A] [Category.{v_2, u_2} B] [Category.{v_3, 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 ((mapPair F (Functor.id C)).whiskerLeft mapPairId.hom) (mapPair F (Functor.id C)).rightUnitor.hom)

def CategoryTheory.Join.pseudofunctorRight (C : Type u₁) [Category.{v₁, u₁} C] : Pseudofunctor Cat Cat

The pseudofunctor sending D to C ⋆ D.

@[simp]

theorem CategoryTheory.Join.pseudofunctorRight_mapId_inv_toNatTrans_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Cat) (x : Join C ↑D) : ((pseudofunctorRight C).mapId D).inv.toNatTrans.app x = match x with | left x => CategoryStruct.id (left x) | right x => CategoryStruct.id (right x)

@[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✝) : CategoryStruct.comp a✝ a✝¹ = comp a✝ a✝¹

@[simp]

theorem CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app (C : Type u₁) [Category.{v₁, u₁} C] {a✝ b✝ : Cat} {f✝ g✝ : a✝ ⟶ b✝} (f : f✝ ⟶ g✝) (x : Join C ↑a✝) : ((pseudofunctorRight C).map₂ f).toNatTrans.app x = match x with | left x => CategoryStruct.id (left x) | right x => (inclRight C ↑b✝).map (f.toNatTrans.app x)

@[simp]

theorem CategoryTheory.Join.pseudofunctorRight_mapComp_hom_toNatTrans_app (C : Type u₁) [Category.{v₁, u₁} C] {a✝ b✝ c✝ : Cat} (F : a✝ ⟶ b✝) (G : b✝ ⟶ c✝) (X : Join C ↑a✝) : ((pseudofunctorRight C).mapComp F G).hom.toNatTrans.app X = CategoryStruct.comp (match X with | left x => CategoryStruct.id (left x) | right x => CategoryStruct.id (right (G.toFunctor.obj (F.toFunctor.obj x)))) ((mapPairComp (Functor.id C) F.toFunctor (Functor.id C) G.toFunctor).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) : CategoryStruct.id x✝ = x✝.id

@[simp]

theorem CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Cat} (F : X✝ ⟶ Y✝) (X : Join C ↑X✝) : ((pseudofunctorRight C).map F).toFunctor.obj X = match X with | left x => left x | right x => right (F.toFunctor.obj x)

@[simp]

theorem CategoryTheory.Join.pseudofunctorRight_mapComp_inv_toNatTrans_app (C : Type u₁) [Category.{v₁, u₁} C] {a✝ b✝ c✝ : Cat} (F : a✝ ⟶ b✝) (G : b✝ ⟶ c✝) (X : Join C ↑a✝) : ((pseudofunctorRight C).mapComp F G).inv.toNatTrans.app X = CategoryStruct.comp ((mapPairComp (Functor.id C) F.toFunctor (Functor.id C) G.toFunctor).inv.app X) (match X with | left x => CategoryStruct.id (left x) | right x => CategoryStruct.id (right (G.toFunctor.obj (F.toFunctor.obj x))))

@[simp]

theorem CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α (C : Type u₁) [Category.{v₁, u₁} C] (D : Cat) : ↑((pseudofunctorRight C).obj D) = Join C ↑D

@[simp]

theorem CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Cat} (F : X✝ ⟶ Y✝) {X✝¹ Y✝¹ : Join C ↑X✝} (f : X✝¹ ⟶ Y✝¹) : ((pseudofunctorRight C).map F).toFunctor.map f = homInduction (fun (x x_1 : C) (f : x ⟶ x_1) => (inclLeft C ↑Y✝).map f) (fun (x x_1 : ↑X✝) (g : x ⟶ x_1) => (inclRight C ↑Y✝).map (F.toFunctor.map g)) (fun (c : C) (d : ↑X✝) => edge c (F.toFunctor.obj d)) f

@[simp]

theorem CategoryTheory.Join.pseudofunctorRight_mapId_hom_toNatTrans_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Cat) (x : Join C ↑D) : ((pseudofunctorRight C).mapId D).hom.toNatTrans.app x = match x with | left x => CategoryStruct.id (left x) | right x => CategoryStruct.id (right x)

def CategoryTheory.Join.pseudofunctorLeft (D : Type u₂) [Category.{v₂, u₂} D] : Pseudofunctor Cat Cat

The pseudofunctor sending C to C ⋆ D.

@[simp]

theorem CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app (D : Type u₂) [Category.{v₂, u₂} D] {a✝ b✝ : Cat} {f✝ g✝ : a✝ ⟶ b✝} (x✝ : f✝ ⟶ g✝) (x : Join (↑a✝) D) : ((pseudofunctorLeft D).map₂ x✝).toNatTrans.app x = match x with | left x => (inclLeft (↑b✝) D).map (x✝.toNatTrans.app x) | right x => CategoryStruct.id (right x)

@[simp]

theorem CategoryTheory.Join.pseudofunctorLeft_mapId_inv_toNatTrans_app (D : Type u₂) [Category.{v₂, u₂} D] (D✝ : Cat) (x : Join (↑D✝) D) : ((pseudofunctorLeft D).mapId D✝).inv.toNatTrans.app x = match x with | left x => CategoryStruct.id (left x) | right x => CategoryStruct.id (right x)

@[simp]

theorem CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : Cat} (F : X✝ ⟶ Y✝) {X✝¹ Y✝¹ : Join (↑X✝) D} (f : X✝¹ ⟶ Y✝¹) : ((pseudofunctorLeft D).map F).toFunctor.map f = homInduction (fun (x x_1 : ↑X✝) (f : x ⟶ x_1) => (inclLeft (↑Y✝) D).map (F.toFunctor.map f)) (fun (x x_1 : D) (g : x ⟶ x_1) => (inclRight (↑Y✝) D).map g) (fun (c : ↑X✝) (d : D) => edge (F.toFunctor.obj c) d) f

@[simp]

theorem CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α (D : Type u₂) [Category.{v₂, u₂} D] (C : Cat) : ↑((pseudofunctorLeft D).obj C) = Join (↑C) D

@[simp]

theorem CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app (D : Type u₂) [Category.{v₂, u₂} D] {a✝ b✝ c✝ : Cat} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) (X : Join (↑a✝) D) : ((pseudofunctorLeft D).mapComp x✝ x✝¹).hom.toNatTrans.app X = CategoryStruct.comp (match X with | left x => CategoryStruct.id (left (x✝¹.toFunctor.obj (x✝.toFunctor.obj x))) | right x => CategoryStruct.id (right x)) ((mapPairComp x✝.toFunctor (Functor.id D) x✝¹.toFunctor (Functor.id D)).hom.app X)

@[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✝) : CategoryStruct.comp a✝ a✝¹ = comp a✝ a✝¹

@[simp]

theorem CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app (D : Type u₂) [Category.{v₂, u₂} D] {a✝ b✝ c✝ : Cat} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) (X : Join (↑a✝) D) : ((pseudofunctorLeft D).mapComp x✝ x✝¹).inv.toNatTrans.app X = CategoryStruct.comp ((mapPairComp x✝.toFunctor (Functor.id D) x✝¹.toFunctor (Functor.id D)).inv.app X) (match X with | left x => CategoryStruct.id (left (x✝¹.toFunctor.obj (x✝.toFunctor.obj x))) | right x => CategoryStruct.id (right x))

@[simp]

theorem CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app (D : Type u₂) [Category.{v₂, u₂} D] (D✝ : Cat) (x : Join (↑D✝) D) : ((pseudofunctorLeft D).mapId D✝).hom.toNatTrans.app x = match x with | left x => CategoryStruct.id (left x) | right x => CategoryStruct.id (right x)

@[simp]

theorem CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : Cat} (F : X✝ ⟶ Y✝) (X : Join (↑X✝) D) : ((pseudofunctorLeft D).map F).toFunctor.obj X = match X with | left x => left (F.toFunctor.obj x) | right x => right x

@[simp]

theorem CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id (D : Type u₂) [Category.{v₂, u₂} D] (C : Cat) (x✝ : Join (↑C) D) : CategoryStruct.id x✝ = x✝.id