Joins of category

Given categories C, D, this file constructs a category C ⋆ D. Its objects are either objects of C or objects of D, morphisms between objects of C are morphisms in C, morphisms between object of D are morphisms in D, and finally, given c : C and d : D, there is a unique morphism c ⟶ d in C ⋆ D.

Main constructions

• Join.edge c d: the unique map from c to d.
• Join.inclLeft : C ⥤ C ⋆ D, the left inclusion. Its action on morphism is the main entry point to construct maps in C ⋆ D between objects coming from C.
• Join.inclRight : D ⥤ C ⋆ D, the left inclusion. Its action on morphism is the main entry point to construct maps in C ⋆ D between object coming from D.
• Join.mkFunctor, A constructor for functors out of a join of categories.
• Join.mkNatTrans, A constructor for natural transformations between functors out of a join of categories.
• Join.mkNatIso, A constructor for natural isomorphisms between functors out of a join of categories.

References

• Kerodon: section 1.4.3.2

inductive CategoryTheory.Join (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Type (max u₁ u₂)

Elements of Join C D are either elements of C or elements of D.

• left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] : C → Join C D
• right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] : D → Join C D

def CategoryTheory.Join.«term_⋆_» : Lean.TrailingParserDescr

Elements of Join C D are either elements of C or elements of D.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Join.Hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] : Join C D → Join C D → Type (max v₁ v₂)

Morphisms in C ⋆ D are those of C and D, plus an unique morphism (left c ⟶ right d) for every c : C and d : D.

Equations

• (CategoryTheory.Join.left x_2).Hom (CategoryTheory.Join.left y) = ULift.{?u.16, ?u.17} (x_2 ⟶ y)
• (CategoryTheory.Join.right x_2).Hom (CategoryTheory.Join.right y) = ULift.{?u.47, ?u.46} (x_2 ⟶ y)
• (CategoryTheory.Join.left a).Hom (CategoryTheory.Join.right a_1) = PUnit.{max (?u.77 + 1) (?u.76 + 1)}
• (CategoryTheory.Join.right a).Hom (CategoryTheory.Join.left a_1) = PEmpty.{max (?u.103 + 1) (?u.102 + 1)}

def CategoryTheory.Join.id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (X : Join C D) : X.Hom X

Identity morphisms in C ⋆ D are inherited from those in C and D.

Equations

• (CategoryTheory.Join.left x_1).id = { down := CategoryTheory.CategoryStruct.id x_1 }
• (CategoryTheory.Join.right x_1).id = { down := CategoryTheory.CategoryStruct.id x_1 }

def CategoryTheory.Join.comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {x y z : Join C D} : x.Hom y → y.Hom z → x.Hom z

Composition in C ⋆ D is inherited from the compositions in C and D.

Equations

• CategoryTheory.Join.comp f g = { down := CategoryTheory.CategoryStruct.comp f.down g.down }
• CategoryTheory.Join.comp x_5 x_6 = PUnit.unit
• CategoryTheory.Join.comp x_5 x_6 = PUnit.unit
• CategoryTheory.Join.comp f g = { down := CategoryTheory.CategoryStruct.comp f.down g.down }

instance CategoryTheory.Join.instCategory {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] : Category.{max v₁ v₂, max u₂ u₁} (Join C D)

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Join.false_of_right_to_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : D} {Y : C} (f : right X ⟶ left Y) : False

instance CategoryTheory.Join.instUniqueHomLeftRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} {Y : D} : Unique (left X ⟶ right Y)

Equations

• CategoryTheory.Join.instUniqueHomLeftRight = inferInstanceAs (Unique PUnit.{max (?u.43 + 1) (?u.42 + 1)})

def CategoryTheory.Join.edge {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (c : C) (d : D) : left c ⟶ right d

Join.edge c d is the unique morphism from c to d.

Equations

• CategoryTheory.Join.edge c d = default

def CategoryTheory.Join.inclLeft (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor C (Join C D)

The canonical inclusion from C to C ⋆ D. Terms of the form (inclLeft C D).map fshould be treated as primitive when working with joins and one should avoid trying to reduce them. For this reason, there is no inclLeft_map simp lemma.

Equations

• CategoryTheory.Join.inclLeft C D = { obj := CategoryTheory.Join.left, map := fun {X Y : C} => ULift.up, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Join.inclLeft_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (a✝ : C) : (inclLeft C D).obj a✝ = left a✝

def CategoryTheory.Join.inclRight (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor D (Join C D)

The canonical inclusion from D to C ⋆ D. Terms of the form (inclRight C D).map fshould be treated as primitive when working with joins and one should avoid trying to reduce them. For this reason, there is no inclRight_map simp lemma.

Equations

• CategoryTheory.Join.inclRight C D = { obj := CategoryTheory.Join.right, map := fun {X Y : D} => ULift.up, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Join.inclRight_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (a✝ : D) : (inclRight C D).obj a✝ = right a✝

def CategoryTheory.Join.homInduction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : {x y : Join C D} → (x ⟶ y) → Sort u_1} (left : (x y : C) → (f : x ⟶ y) → P ((inclLeft C D).map f)) (right : (x y : D) → (f : x ⟶ y) → P ((inclRight C D).map f)) (edge : (c : C) → (d : D) → P (edge c d)) {x y : Join C D} (f : x ⟶ y) : P f

An induction principle for morphisms in a join of category: a morphism is either of the form (inclLeft _ _).map _, (inclRight _ _).map _, or is edge _ _.

Equations

• CategoryTheory.Join.homInduction left right edge { down := f_2 } = left x_2 y_2 f_2
• CategoryTheory.Join.homInduction left right edge { down := f_2 } = right x_2 y_2 f_2
• CategoryTheory.Join.homInduction left right edge x_3 = edge x_2 y_2

@[simp]

theorem CategoryTheory.Join.homInduction_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : {x y : Join C D} → (x ⟶ y) → Sort u_1} (left : (x y : C) → (f : x ⟶ y) → P ((inclLeft C D).map f)) (right : (x y : D) → (f : x ⟶ y) → P ((inclRight C D).map f)) (edge : (c : C) → (d : D) → P (edge c d)) {x y : C} (f : x ⟶ y) : homInduction left right edge ((inclLeft C D).map f) = left x y f

@[simp]

theorem CategoryTheory.Join.homInduction_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : {x y : Join C D} → (x ⟶ y) → Sort u_1} (left : (x y : C) → (f : x ⟶ y) → P ((inclLeft C D).map f)) (right : (x y : D) → (f : x ⟶ y) → P ((inclRight C D).map f)) (edge : (c : C) → (d : D) → P (edge c d)) {x y : D} (f : x ⟶ y) : homInduction left right edge ((inclRight C D).map f) = right x y f

@[simp]

theorem CategoryTheory.Join.homInduction_edge {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : {x y : Join C D} → (x ⟶ y) → Sort u_1} (left : (x y : C) → (f : x ⟶ y) → P ((inclLeft C D).map f)) (right : (x y : D) → (f : x ⟶ y) → P ((inclRight C D).map f)) (edge : (c : C) → (d : D) → P (edge c d)) {c : C} {d : D} : homInduction left right edge (CategoryTheory.Join.edge c d) = edge c d

def CategoryTheory.Join.inclLeftFullyFaithful (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (inclLeft C D).FullyFaithful

The left inclusion is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Join.inclRightFullyFaithful (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (inclRight C D).FullyFaithful

The right inclusion is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Join.inclLeftFull (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (inclLeft C D).Full

instance CategoryTheory.Join.inclRightFull (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (inclRight C D).Full

instance CategoryTheory.Join.inclLeftFaithFull (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (inclLeft C D).Faithful

instance CategoryTheory.Join.inclRightFaithfull (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (inclRight C D).Faithful

theorem CategoryTheory.Join.id_left {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (c : C) : CategoryStruct.id (left c) = (inclLeft C D).map (CategoryStruct.id c)

A situational lemma to help putting identities in the form (inclLeft _ _).map _ when using homInduction.

theorem CategoryTheory.Join.id_right (C : Type u₁) [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (d : D) : CategoryStruct.id (right d) = (inclRight C D).map (CategoryStruct.id d)

A situational lemma to help putting identities in the form (inclRight _ _).map _ when using homInduction.

def CategoryTheory.Join.edgeTransform (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (Prod.fst C D).comp (inclLeft C D) ⟶ (Prod.snd C D).comp (inclRight C D)

The "canonical" natural transformation from (Prod.fst C D) ⋙ inclLeft C D to (Prod.snd C D) ⋙ inclRight C D. This is bundling together all the edge morphisms into the data of a natural transformation.

Equations

• CategoryTheory.Join.edgeTransform C D = { app := fun (x : C × D) => match x with | (c, d) => CategoryTheory.Join.edge c d, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Join.edgeTransform_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (x✝ : C × D) : (edgeTransform C D).app x✝ = edge x✝.1 x✝.2

def CategoryTheory.Join.mkFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) : Functor (Join C D) E

A pair of functor F : C ⥤ E, G : D ⥤ E as well as a natural transformation α : (Prod.fst C D) ⋙ F ⟶ (Prod.snd C D) ⋙ G. defines a functor out of C ⋆ D. This is the main entry point to define functors out of a join of categories.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mkFunctor_obj_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) (c : C) : (mkFunctor F G α).obj (left c) = F.obj c

@[simp]

theorem CategoryTheory.Join.mkFunctor_obj_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) (d : D) : (mkFunctor F G α).obj (right d) = G.obj d

@[simp]

theorem CategoryTheory.Join.mkFunctor_map_inclLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) {c c' : C} (f : c ⟶ c') : (mkFunctor F G α).map ((inclLeft C D).map f) = F.map f

def CategoryTheory.Join.mkFunctorLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) : (inclLeft C D).comp (mkFunctor F G α) ≅ F

Precomposing mkFunctor F G α with the left inclusion gives back F.

Equations

• CategoryTheory.Join.mkFunctorLeft F G α = CategoryTheory.Iso.refl ((CategoryTheory.Join.inclLeft C D).comp (CategoryTheory.Join.mkFunctor F G α))

@[simp]

theorem CategoryTheory.Join.mkFunctorLeft_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) (X : C) : (mkFunctorLeft F G α).hom.app X = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Join.mkFunctorLeft_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) (X : C) : (mkFunctorLeft F G α).inv.app X = CategoryStruct.id (F.obj X)

def CategoryTheory.Join.mkFunctorRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) : (inclRight C D).comp (mkFunctor F G α) ≅ G

Precomposing mkFunctor F G α with the right inclusion gives back G.

Equations

• CategoryTheory.Join.mkFunctorRight F G α = CategoryTheory.Iso.refl ((CategoryTheory.Join.inclRight C D).comp (CategoryTheory.Join.mkFunctor F G α))

@[simp]

theorem CategoryTheory.Join.mkFunctorRight_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) (X : D) : (mkFunctorRight F G α).hom.app X = CategoryStruct.id (G.obj X)

@[simp]

theorem CategoryTheory.Join.mkFunctorRight_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) (X : D) : (mkFunctorRight F G α).inv.app X = CategoryStruct.id (G.obj X)

@[simp]

theorem CategoryTheory.Join.mkFunctor_map_inclRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) {d d' : D} (f : d ⟶ d') : (mkFunctor F G α).map ((inclRight C D).map f) = G.map f

@[simp]

theorem CategoryTheory.Join.mkFunctor_edgeTransform {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) : whiskerRight (edgeTransform C D) (mkFunctor F G α) = α

Whiskering mkFunctor F G α with the universal transformation gives back α.

@[simp]

theorem CategoryTheory.Join.mkFunctor_map_edge {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) (α : (Prod.fst C D).comp F ⟶ (Prod.snd C D).comp G) (c : C) (d : D) : (mkFunctor F G α).map (edge c d) = α.app (c, d)

def CategoryTheory.Join.mkNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F F' : Functor (Join C D) E} (αₗ : (inclLeft C D).comp F ⟶ (inclLeft C D).comp F') (αᵣ : (inclRight C D).comp F ⟶ (inclRight C D).comp F') (h : CategoryStruct.comp (whiskerRight (edgeTransform C D) F) (whiskerLeft (Prod.snd C D) αᵣ) = CategoryStruct.comp (whiskerLeft (Prod.fst C D) αₗ) (whiskerRight (edgeTransform C D) F') := by aesop_cat) : F ⟶ F'

Construct a natural transformation between functors from a join from the data of natural transformations between each side that are compatible with the action on edge maps.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mkNatTrans_app_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F F' : Functor (Join C D) E} (αₗ : (inclLeft C D).comp F ⟶ (inclLeft C D).comp F') (αᵣ : (inclRight C D).comp F ⟶ (inclRight C D).comp F') (h : CategoryStruct.comp (whiskerRight (edgeTransform C D) F) (whiskerLeft (Prod.snd C D) αᵣ) = CategoryStruct.comp (whiskerLeft (Prod.fst C D) αₗ) (whiskerRight (edgeTransform C D) F') := by aesop_cat) (c : C) : (mkNatTrans αₗ αᵣ h).app (left c) = αₗ.app c

@[simp]

theorem CategoryTheory.Join.mkNatTrans_app_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F F' : Functor (Join C D) E} (αₗ : (inclLeft C D).comp F ⟶ (inclLeft C D).comp F') (αᵣ : (inclRight C D).comp F ⟶ (inclRight C D).comp F') (h : CategoryStruct.comp (whiskerRight (edgeTransform C D) F) (whiskerLeft (Prod.snd C D) αᵣ) = CategoryStruct.comp (whiskerLeft (Prod.fst C D) αₗ) (whiskerRight (edgeTransform C D) F') := by aesop_cat) (d : D) : (mkNatTrans αₗ αᵣ h).app (right d) = αᵣ.app d

@[simp]

theorem CategoryTheory.Join.whiskerLeft_inclLeft_mkNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F F' : Functor (Join C D) E} (αₗ : (inclLeft C D).comp F ⟶ (inclLeft C D).comp F') (αᵣ : (inclRight C D).comp F ⟶ (inclRight C D).comp F') (h : CategoryStruct.comp (whiskerRight (edgeTransform C D) F) (whiskerLeft (Prod.snd C D) αᵣ) = CategoryStruct.comp (whiskerLeft (Prod.fst C D) αₗ) (whiskerRight (edgeTransform C D) F') := by aesop_cat) : whiskerLeft (inclLeft C D) (mkNatTrans αₗ αᵣ h) = αₗ

@[simp]

theorem CategoryTheory.Join.whiskerLeft_inclRight_mkNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F F' : Functor (Join C D) E} (αₗ : (inclLeft C D).comp F ⟶ (inclLeft C D).comp F') (αᵣ : (inclRight C D).comp F ⟶ (inclRight C D).comp F') (h : CategoryStruct.comp (whiskerRight (edgeTransform C D) F) (whiskerLeft (Prod.snd C D) αᵣ) = CategoryStruct.comp (whiskerLeft (Prod.fst C D) αₗ) (whiskerRight (edgeTransform C D) F') := by aesop_cat) : whiskerLeft (inclRight C D) (mkNatTrans αₗ αᵣ h) = αᵣ

theorem CategoryTheory.Join.natTrans_ext {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F F' : Functor (Join C D) E} {α β : F ⟶ F'} (h₁ : whiskerLeft (inclLeft C D) α = whiskerLeft (inclLeft C D) β) (h₂ : whiskerLeft (inclRight C D) α = whiskerLeft (inclRight C D) β) : α = β

Two natural transformations between functors out of a join are equal if they are so after whiskering with the inclusions.

theorem CategoryTheory.Join.eq_mkNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F F' : Functor (Join C D) E} (α : F ⟶ F') : mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) ⋯ = α

theorem CategoryTheory.Join.mkNatTransComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F F' F'' : Functor (Join C D) E} (αₗ : (inclLeft C D).comp F ⟶ (inclLeft C D).comp F') (αᵣ : (inclRight C D).comp F ⟶ (inclRight C D).comp F') (βₗ : (inclLeft C D).comp F' ⟶ (inclLeft C D).comp F'') (βᵣ : (inclRight C D).comp F' ⟶ (inclRight C D).comp F'') (h : CategoryStruct.comp (whiskerRight (edgeTransform C D) F) (whiskerLeft (Prod.snd C D) αᵣ) = CategoryStruct.comp (whiskerLeft (Prod.fst C D) αₗ) (whiskerRight (edgeTransform C D) F') := by aesop_cat) (h' : CategoryStruct.comp (whiskerRight (edgeTransform C D) F') (whiskerLeft (Prod.snd C D) βᵣ) = CategoryStruct.comp (whiskerLeft (Prod.fst C D) βₗ) (whiskerRight (edgeTransform C D) F'') := by aesop_cat) : mkNatTrans (CategoryStruct.comp αₗ βₗ) (CategoryStruct.comp αᵣ βᵣ) ⋯ = CategoryStruct.comp (mkNatTrans αₗ αᵣ h) (mkNatTrans βₗ βᵣ h')

mkNatTrans respects vertical composition.

def CategoryTheory.Join.mkNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor (Join C D) E} (eₗ : (inclLeft C D).comp F ≅ (inclLeft C D).comp G) (eᵣ : (inclRight C D).comp F ≅ (inclRight C D).comp G) (h : CategoryStruct.comp (whiskerRight (edgeTransform C D) F) (isoWhiskerLeft (Prod.snd C D) eᵣ).hom = CategoryStruct.comp (isoWhiskerLeft (Prod.fst C D) eₗ).hom (whiskerRight (edgeTransform C D) G) := by aesop_cat) : F ≅ G

Two functors out of a join of category are naturally isomorphic if their compositions with the inclusions are isomorphic and the whiskering with the canonical transformation is respected through these isomorphisms.

Equations

• CategoryTheory.Join.mkNatIso eₗ eᵣ h = { hom := CategoryTheory.Join.mkNatTrans eₗ.hom eᵣ.hom h, inv := CategoryTheory.Join.mkNatTrans eₗ.inv eᵣ.inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Join.mkNatIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor (Join C D) E} (eₗ : (inclLeft C D).comp F ≅ (inclLeft C D).comp G) (eᵣ : (inclRight C D).comp F ≅ (inclRight C D).comp G) (h : CategoryStruct.comp (whiskerRight (edgeTransform C D) F) (isoWhiskerLeft (Prod.snd C D) eᵣ).hom = CategoryStruct.comp (isoWhiskerLeft (Prod.fst C D) eₗ).hom (whiskerRight (edgeTransform C D) G) := by aesop_cat) : (mkNatIso eₗ eᵣ h).hom = mkNatTrans eₗ.hom eᵣ.hom h

@[simp]

theorem CategoryTheory.Join.mkNatIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor (Join C D) E} (eₗ : (inclLeft C D).comp F ≅ (inclLeft C D).comp G) (eᵣ : (inclRight C D).comp F ≅ (inclRight C D).comp G) (h : CategoryStruct.comp (whiskerRight (edgeTransform C D) F) (isoWhiskerLeft (Prod.snd C D) eᵣ).hom = CategoryStruct.comp (isoWhiskerLeft (Prod.fst C D) eₗ).hom (whiskerRight (edgeTransform C D) G) := by aesop_cat) : (mkNatIso eₗ eᵣ h).inv = mkNatTrans eₗ.inv eᵣ.inv ⋯

def CategoryTheory.Join.mapPair {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ : Functor C E) (Fᵣ : Functor D E') : Functor (Join C D) (Join E E')

A pair of functors ((C ⥤ E), (D ⥤ E')) induces a functor C ⋆ D ⥤ E ⋆ E'.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mapPair_obj_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ : Functor C E) (Fᵣ : Functor D E') (c : C) : (mapPair Fₗ Fᵣ).obj (left c) = left (Fₗ.obj c)

@[simp]

theorem CategoryTheory.Join.mapPair_obj_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ : Functor C E) (Fᵣ : Functor D E') (d : D) : (mapPair Fₗ Fᵣ).obj (right d) = right (Fᵣ.obj d)

@[simp]

theorem CategoryTheory.Join.mapPair_map_inclLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ : Functor C E) (Fᵣ : Functor D E') {c c' : C} (f : c ⟶ c') : (mapPair Fₗ Fᵣ).map ((inclLeft C D).map f) = (inclLeft E E').map (Fₗ.map f)

@[simp]

theorem CategoryTheory.Join.mapPair_map_inclRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ : Functor C E) (Fᵣ : Functor D E') {d d' : D} (f : d ⟶ d') : (mapPair Fₗ Fᵣ).map ((inclRight C D).map f) = (inclRight E E').map (Fᵣ.map f)

def CategoryTheory.Join.mapPairLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ : Functor C E) (Fᵣ : Functor D E') : (inclLeft C D).comp (mapPair Fₗ Fᵣ) ≅ Fₗ.comp (inclLeft E E')

Characterizing mapPair on left morphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mapPairLeft_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ : Functor C E) (Fᵣ : Functor D E') (X : C) : (mapPairLeft Fₗ Fᵣ).hom.app X = CategoryStruct.id (left (Fₗ.obj X))

@[simp]

theorem CategoryTheory.Join.mapPairLeft_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ : Functor C E) (Fᵣ : Functor D E') (X : C) : (mapPairLeft Fₗ Fᵣ).inv.app X = CategoryStruct.id (left (Fₗ.obj X))

def CategoryTheory.Join.mapPairRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ : Functor C E) (Fᵣ : Functor D E') : (inclRight C D).comp (mapPair Fₗ Fᵣ) ≅ Fᵣ.comp (inclRight E E')

Characterizing mapPair on right morphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mapPairRight_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ : Functor C E) (Fᵣ : Functor D E') (X : D) : (mapPairRight Fₗ Fᵣ).inv.app X = CategoryStruct.id (right (Fᵣ.obj X))

@[simp]

theorem CategoryTheory.Join.mapPairRight_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ : Functor C E) (Fᵣ : Functor D E') (X : D) : (mapPairRight Fₗ Fᵣ).hom.app X = CategoryStruct.id (right (Fᵣ.obj X))

def CategoryTheory.Join.isoMkFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor (Join C D) E) : F ≅ mkFunctor ((inclLeft C D).comp F) ((inclRight C D).comp F) (whiskerRight (edgeTransform C D) F)

Any functor out of a join is naturally isomorphic to a functor of the form mkFunctor F G α.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.isoMkFunctor_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor (Join C D) E) (x : Join C D) : (isoMkFunctor F).inv.app x = match x with | left x => CategoryStruct.id (F.obj (left x)) | right x => CategoryStruct.id (F.obj (right x))

@[simp]

theorem CategoryTheory.Join.isoMkFunctor_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor (Join C D) E) (x : Join C D) : (isoMkFunctor F).hom.app x = match x with | left x => CategoryStruct.id (F.obj (left x)) | right x => CategoryStruct.id (F.obj (right x))

def CategoryTheory.Join.mapPairId {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] : mapPair (Functor.id C) (Functor.id D) ≅ Functor.id (Join C D)

mapPair respects identities

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mapPairId_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (x : Join C D) : mapPairId.inv.app x = match x with | left x => CategoryStruct.id (left x) | right x => CategoryStruct.id (right x)

@[simp]

theorem CategoryTheory.Join.mapPairId_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (x : Join C D) : mapPairId.hom.app x = match x with | left x => CategoryStruct.id (left x) | right x => CategoryStruct.id (right x)

def CategoryTheory.Join.mapPairComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {J : Type u₅} [Category.{v₅, u₅} J] {K : Type u₆} [Category.{v₆, u₆} K] (Fₗ : Functor C E) (Fᵣ : Functor D E') (Gₗ : Functor E J) (Gᵣ : Functor E' K) : mapPair (Fₗ.comp Gₗ) (Fᵣ.comp Gᵣ) ≅ (mapPair Fₗ Fᵣ).comp (mapPair Gₗ Gᵣ)

mapPair respects composition

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mapPairComp_hom_app_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {J : Type u₅} [Category.{v₅, u₅} J] {K : Type u₆} [Category.{v₆, u₆} K] (Fₗ : Functor C E) (Fᵣ : Functor D E') (Gₗ : Functor E J) (Gᵣ : Functor E' K) (c : C) : (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (left c) = CategoryStruct.id (left (Gₗ.obj (Fₗ.obj c)))

@[simp]

theorem CategoryTheory.Join.mapPairComp_hom_app_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {J : Type u₅} [Category.{v₅, u₅} J] {K : Type u₆} [Category.{v₆, u₆} K] (Fₗ : Functor C E) (Fᵣ : Functor D E') (Gₗ : Functor E J) (Gᵣ : Functor E' K) (d : D) : (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (right d) = CategoryStruct.id (right (Gᵣ.obj (Fᵣ.obj d)))

@[simp]

theorem CategoryTheory.Join.mapPairComp_inv_app_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {J : Type u₅} [Category.{v₅, u₅} J] {K : Type u₆} [Category.{v₆, u₆} K] (Fₗ : Functor C E) (Fᵣ : Functor D E') (Gₗ : Functor E J) (Gᵣ : Functor E' K) (c : C) : (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (left c) = CategoryStruct.id (left (Gₗ.obj (Fₗ.obj c)))

@[simp]

theorem CategoryTheory.Join.mapPairComp_inv_app_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {J : Type u₅} [Category.{v₅, u₅} J] {K : Type u₆} [Category.{v₆, u₆} K] (Fₗ : Functor C E) (Fᵣ : Functor D E') (Gₗ : Functor E J) (Gᵣ : Functor E' K) (d : D) : (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (right d) = CategoryStruct.id (right (Gᵣ.obj (Fᵣ.obj d)))

def CategoryTheory.Join.mapWhiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {Fₗ Gₗ : Functor C E} (α : Fₗ ⟶ Gₗ) (H : Functor D E') : mapPair Fₗ H ⟶ mapPair Gₗ H

A natural transformation Fₗ ⟶ Gₗ induces a natural transformation mapPair Fₗ H ⟶ mapPair Gₗ H for every H : D ⥤ E'.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mapWhiskerRight_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {Fₗ Gₗ : Functor C E} (α : Fₗ ⟶ Gₗ) (H : Functor D E') (x : Join C D) : (mapWhiskerRight α H).app x = match x with | left x => (inclLeft E E').map (α.app x) | right x => CategoryStruct.id (right (H.obj x))

@[simp]

theorem CategoryTheory.Join.mapWhiskerRight_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {Fₗ Gₗ Hₗ : Functor C E} (α : Fₗ ⟶ Gₗ) (β : Gₗ ⟶ Hₗ) (H : Functor D E') : mapWhiskerRight (CategoryStruct.comp α β) H = CategoryStruct.comp (mapWhiskerRight α H) (mapWhiskerRight β H)

def CategoryTheory.Join.mapWhiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (H : Functor C E) {Fᵣ Gᵣ : Functor D E'} (α : Fᵣ ⟶ Gᵣ) : mapPair H Fᵣ ⟶ mapPair H Gᵣ

A natural transformation Fᵣ ⟶ Gᵣ induces a natural transformation mapPair H Fᵣ ⟶ mapPair H Gᵣ for every H : C ⥤ E.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mapWhiskerLeft_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (H : Functor C E) {Fᵣ Gᵣ : Functor D E'} (α : Fᵣ ⟶ Gᵣ) (x : Join C D) : (mapWhiskerLeft H α).app x = match x with | left x => CategoryStruct.id (left (H.obj x)) | right x => (inclRight E E').map (α.app x)

@[simp]

theorem CategoryTheory.Join.mapWhiskerLeft_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {Fᵣ Gᵣ Hᵣ : Functor D E'} (H : Functor C E) (α : Fᵣ ⟶ Gᵣ) (β : Gᵣ ⟶ Hᵣ) : mapWhiskerLeft H (CategoryStruct.comp α β) = CategoryStruct.comp (mapWhiskerLeft H α) (mapWhiskerLeft H β)

theorem CategoryTheory.Join.mapWhisker_exchange {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (Fₗ Gₗ : Functor C E) (Fᵣ Gᵣ : Functor D E') (αₗ : Fₗ ⟶ Gₗ) (αᵣ : Fᵣ ⟶ Gᵣ) : CategoryStruct.comp (mapWhiskerLeft Fₗ αᵣ) (mapWhiskerRight αₗ Gᵣ) = CategoryStruct.comp (mapWhiskerRight αₗ Fᵣ) (mapWhiskerLeft Gₗ αᵣ)

One can exchange mapWhiskerLeft and mapWhiskerRight.

def CategoryTheory.Join.mapIsoWhiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (H : Functor C E) {Fᵣ Gᵣ : Functor D E'} (α : Fᵣ ≅ Gᵣ) : mapPair H Fᵣ ≅ mapPair H Gᵣ

A natural isomorphism Fᵣ ≅ Gᵣ induces a natural isomorphism mapPair H Fᵣ ≅ mapPair H Gᵣ for every H : C ⥤ E.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mapIsoWhiskerLeft_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (H : Functor C E) {Fᵣ Gᵣ : Functor D E'} (α : Fᵣ ≅ Gᵣ) (x : Join C D) : (mapIsoWhiskerLeft H α).hom.app x = match x with | left x => CategoryStruct.id (left (H.obj x)) | right x => (inclRight E E').map (α.hom.app x)

@[simp]

theorem CategoryTheory.Join.mapIsoWhiskerLeft_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (H : Functor C E) {Fᵣ Gᵣ : Functor D E'} (α : Fᵣ ≅ Gᵣ) (x : Join C D) : (mapIsoWhiskerLeft H α).inv.app x = match x with | left x => CategoryStruct.id (left (H.obj x)) | right x => (inclRight E E').map (α.inv.app x)

def CategoryTheory.Join.mapIsoWhiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {Fₗ Gₗ : Functor C E} (α : Fₗ ≅ Gₗ) (H : Functor D E') : mapPair Fₗ H ≅ mapPair Gₗ H

A natural isomorphism Fᵣ ≅ Gᵣ induces a natural isomorphism mapPair Fₗ H ≅ mapPair Gₗ H for every H : C ⥤ E.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mapIsoWhiskerRight_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {Fₗ Gₗ : Functor C E} (α : Fₗ ≅ Gₗ) (H : Functor D E') (x : Join C D) : (mapIsoWhiskerRight α H).inv.app x = match x with | left x => (inclLeft E E').map (α.inv.app x) | right x => CategoryStruct.id (right (H.obj x))

@[simp]

theorem CategoryTheory.Join.mapIsoWhiskerRight_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {Fₗ Gₗ : Functor C E} (α : Fₗ ≅ Gₗ) (H : Functor D E') (x : Join C D) : (mapIsoWhiskerRight α H).hom.app x = match x with | left x => (inclLeft E E').map (α.hom.app x) | right x => CategoryStruct.id (right (H.obj x))

theorem CategoryTheory.Join.mapIsoWhiskerRight_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {Fₗ Gₗ : Functor C E} (α : Fₗ ≅ Gₗ) (H : Functor D E') : (mapIsoWhiskerRight α H).hom = mapWhiskerRight α.hom H

theorem CategoryTheory.Join.mapIsoWhiskerRight_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {Fₗ Gₗ : Functor C E} (α : Fₗ ≅ Gₗ) (H : Functor D E') : (mapIsoWhiskerRight α H).inv = mapWhiskerRight α.inv H

theorem CategoryTheory.Join.mapIsoWhiskerLeft_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (H : Functor C E) {Fᵣ Gᵣ : Functor D E'} (α : Fᵣ ≅ Gᵣ) : (mapIsoWhiskerLeft H α).hom = mapWhiskerLeft H α.hom

theorem CategoryTheory.Join.mapIsoWhiskerLeft_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (H : Functor C E) {Fᵣ Gᵣ : Functor D E'} (α : Fᵣ ≅ Gᵣ) : (mapIsoWhiskerLeft H α).inv = mapWhiskerLeft H α.inv

def CategoryTheory.Join.mapPairEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] {D' : Type u₄} [Category.{v₄, u₄} D'] (e : C ≌ C') (e' : D ≌ D') : Join C D ≌ Join C' D'

Equivalent categories have equivalent joins.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Join.mapPairEquiv_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] {D' : Type u₄} [Category.{v₄, u₄} D'] (e : C ≌ C') (e' : D ≌ D') : (mapPairEquiv e e').inverse = mapPair e.inverse e'.inverse

@[simp]

theorem CategoryTheory.Join.mapPairEquiv_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] {D' : Type u₄} [Category.{v₄, u₄} D'] (e : C ≌ C') (e' : D ≌ D') : (mapPairEquiv e e').functor = mapPair e.functor e'.functor

@[simp]

theorem CategoryTheory.Join.mapPairEquiv_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] {D' : Type u₄} [Category.{v₄, u₄} D'] (e : C ≌ C') (e' : D ≌ D') : (mapPairEquiv e e').counitIso = (mapPairComp e.inverse e'.inverse e.functor e'.functor).symm ≪≫ mapIsoWhiskerRight e.counitIso (e'.inverse.comp e'.functor) ≪≫ mapIsoWhiskerLeft (Functor.id C') e'.counitIso ≪≫ mapPairId

@[simp]

theorem CategoryTheory.Join.mapPairEquiv_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] {D' : Type u₄} [Category.{v₄, u₄} D'] (e : C ≌ C') (e' : D ≌ D') : (mapPairEquiv e e').unitIso = mapPairId.symm ≪≫ mapIsoWhiskerRight e.unitIso (Functor.id D) ≪≫ mapIsoWhiskerLeft (e.functor.comp e.inverse) e'.unitIso ≪≫ mapPairComp e.functor e'.functor e.inverse e'.inverse

instance CategoryTheory.Join.isEquivalenceMapPair {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] {D' : Type u₄} [Category.{v₄, u₄} D'] {F : Functor C C'} {F' : Functor D D'} [F.IsEquivalence] [F'.IsEquivalence] : (mapPair F F').IsEquivalence