Documentation

Mathlib.CategoryTheory.Join.Basic

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 #

References #

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.

Instances For

    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.
    Instances For
      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
      Instances For
        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 yy.Hom zx.Hom z

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

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          def CategoryTheory.Join.edge {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (c : C) (d : D) :

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

          Equations
          Instances For

            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
            Instances For
              @[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✝

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

                  The left inclusion is fully faithful.

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

                    The right inclusion is fully faithful.

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

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

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

                      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
                      Instances For
                        @[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.
                        Instances For
                          @[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
                          Instances For
                            @[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) :
                            @[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) :
                            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
                            Instances For
                              @[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) :
                              @[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) :
                              @[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) :

                              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.
                              Instances For
                                @[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
                                Instances For
                                  @[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
                                  @[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
                                  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.
                                  Instances For
                                    @[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.
                                    Instances For
                                      @[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))
                                      @[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))
                                      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.
                                      Instances For
                                        @[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))
                                        @[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))

                                        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.
                                        Instances For
                                          @[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))
                                          @[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))

                                          mapPair respects identities

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            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.
                                            Instances For
                                              @[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.
                                              Instances For
                                                @[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') :
                                                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.
                                                Instances For
                                                  @[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ᵣ) :
                                                  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ᵣ) :

                                                  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.
                                                  Instances For
                                                    @[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.
                                                    Instances For
                                                      @[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))
                                                      @[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))
                                                      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') :
                                                      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') :
                                                      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ᵣ) :
                                                      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ᵣ) :