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) : 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.{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) : 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.{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) (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.{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) (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.{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 (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.{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 (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.{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) (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.{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) (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.{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 (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.{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 (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.{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 (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.{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 (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.{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 (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.{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 (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.{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 (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.{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 ((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.{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 ((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_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_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_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_mapId_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Cat) (x : Join C ↑D) : ((pseudofunctorRight C).mapId D).hom.app x = match x with | left x => comp (left x).id (comp (left x).id (left x).id) | right x => comp (right x).id (comp (right x).id (right x).id)

@[simp]

theorem CategoryTheory.Join.pseudofunctorRight_mapId_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Cat) (x : Join C ↑D) : ((pseudofunctorRight C).mapId D).inv.app x = match x with | left x => comp (comp (left x).id (left x).id) (left x).id | right x => comp (comp (right x).id (right x).id) (right 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✝¹) : ((pseudofunctorRight C).map F).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.map g)) (fun (c : C) (d : ↑X✝) => edge c (F.obj d)) f

@[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₂_app (C : Type u₁) [Category.{v₁, u₁} C] {a✝ b✝ : Cat} {f✝ g✝ : a✝ ⟶ b✝} (α : f✝ ⟶ g✝) (x : Join C ↑a✝) : ((pseudofunctorRight C).map₂ α).app x = match x with | left x => comp (left x).id (comp (left x).id (left x).id) | right x => comp (right (f✝.obj x)).id (comp ((inclRight C ↑b✝).map (α.app x)) (right (g✝.obj x)).id)

@[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✝) : ((pseudofunctorRight C).map F).obj X = match X with | left x => left x | right x => right (F.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

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_toPrefunctor_map_obj (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : Cat} (F : X✝ ⟶ Y✝) (X : Join (↑X✝) D) : ((pseudofunctorLeft D).map F).obj X = match X with | left x => left (F.obj x) | right x => right 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_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_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) : ((pseudofunctorLeft D).map₂ x✝).app x = match x with | left x => comp (left (f✝.obj x)).id (comp ((inclLeft (↑b✝) D).map (x✝.app x)) (left (g✝.obj x)).id) | right x => comp (right x).id (comp (right x).id (right x).id)

@[simp]

theorem CategoryTheory.Join.pseudofunctorLeft_mapId_inv_app (D : Type u₂) [Category.{v₂, u₂} D] (D✝ : Cat) (x : Join (↑D✝) D) : ((pseudofunctorLeft D).mapId D✝).inv.app x = match x with | left x => comp (comp (left x).id (left x).id) (left x).id | right x => comp (comp (right x).id (right x).id) (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_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✝¹) : ((pseudofunctorLeft D).map F).map f = homInduction (fun (x x_1 : ↑X✝) (f : x ⟶ x_1) => (inclLeft (↑Y✝) D).map (F.map f)) (fun (x x_1 : D) (g : x ⟶ x_1) => (inclRight (↑Y✝) D).map g) (fun (c : ↑X✝) (d : D) => edge (F.obj c) d) f

@[simp]

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

@[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

@[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