# Binary disjoint unions of categories #

We define the category instance on C ⊕ D when C and D are categories.

We define:

• inl_ : the functor C ⥤ C ⊕ D
• inr_ : the functor D ⥤ C ⊕ D
• swap : the functor C ⊕ D ⥤ D ⊕ C (and the fact this is an equivalence)

We further define sums of functors and natural transformations, written F.sum G and α.sum β.

instance CategoryTheory.sum (C : Type u₁) [] (D : Type u₁) [] :

sum C D gives the direct sum of two categories.

Equations
theorem CategoryTheory.hom_inl_inr_false (C : Type u₁) [] (D : Type u₁) [] {X : C} {Y : D} (f : ) :
theorem CategoryTheory.hom_inr_inl_false (C : Type u₁) [] (D : Type u₁) [] {X : C} {Y : D} (f : ) :
theorem CategoryTheory.sum_comp_inl (C : Type u₁) [] (D : Type u₁) [] {P : C} {Q : C} {R : C} (f : ) (g : ) :
theorem CategoryTheory.sum_comp_inr (C : Type u₁) [] (D : Type u₁) [] {P : D} {Q : D} {R : D} (f : ) (g : ) :
@[simp]
theorem CategoryTheory.Sum.inl__map (C : Type u₁) [] (D : Type u₁) [] {X : C} {Y : C} (f : X Y) :
().map f = f
@[simp]
theorem CategoryTheory.Sum.inl__obj (C : Type u₁) [] (D : Type u₁) [] (X : C) :
().obj X =
def CategoryTheory.Sum.inl_ (C : Type u₁) [] (D : Type u₁) [] :

inl_ is the functor X ↦ inl X.

Equations
• = { obj := fun (X : C) => , map := fun {X Y : C} (f : X Y) => f, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Sum.inr__map (C : Type u₁) [] (D : Type u₁) [] {X : D} {Y : D} (f : X Y) :
().map f = f
@[simp]
theorem CategoryTheory.Sum.inr__obj (C : Type u₁) [] (D : Type u₁) [] (X : D) :
().obj X =
def CategoryTheory.Sum.inr_ (C : Type u₁) [] (D : Type u₁) [] :

inr_ is the functor X ↦ inr X.

Equations
• = { obj := fun (X : D) => , map := fun {X Y : D} (f : X Y) => f, map_id := , map_comp := }
Instances For
def CategoryTheory.Sum.swap (C : Type u₁) [] (D : Type u₁) [] :

The functor exchanging two direct summand categories.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Sum.swap_obj_inl (C : Type u₁) [] (D : Type u₁) [] (X : C) :
().obj () =
@[simp]
theorem CategoryTheory.Sum.swap_obj_inr (C : Type u₁) [] (D : Type u₁) [] (X : D) :
().obj () =
@[simp]
theorem CategoryTheory.Sum.swap_map_inl (C : Type u₁) [] (D : Type u₁) [] {X : C} {Y : C} {f : } :
().map f = f
@[simp]
theorem CategoryTheory.Sum.swap_map_inr (C : Type u₁) [] (D : Type u₁) [] {X : D} {Y : D} {f : } :
().map f = f
def CategoryTheory.Sum.Swap.equivalence (C : Type u₁) [] (D : Type u₁) [] :
C D D C

swap gives an equivalence between C ⊕ D and D ⊕ C.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Sum.Swap.isEquivalence (C : Type u₁) [] (D : Type u₁) [] :
().IsEquivalence
Equations
• =
def CategoryTheory.Sum.Swap.symmetry (C : Type u₁) [] (D : Type u₁) [] :
().comp ()

The double swap on C ⊕ D is naturally isomorphic to the identity functor.

Equations
• = .unitIso.symm
Instances For
def CategoryTheory.Functor.sum {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] {D : Type u₁} [] (F : ) (G : ) :

The sum of two functors.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Functor.sum' {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] (F : ) (G : ) :

Similar to sum, but both functors land in the same category C

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Functor.inlCompSum'_inv_app {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] (F : ) (G : ) (X : A) :
(F.inlCompSum' G).inv.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj ())
@[simp]
theorem CategoryTheory.Functor.inlCompSum'_hom_app {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] (F : ) (G : ) (X : A) :
(F.inlCompSum' G).hom.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj ())
def CategoryTheory.Functor.inlCompSum' {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] (F : ) (G : ) :
().comp (F.sum' G) F

The sum F.sum' G precomposed with the left inclusion functor is isomorphic to F

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.inrCompSum'_hom_app {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] (F : ) (G : ) (X : B) :
(F.inrCompSum' G).hom.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj ())
@[simp]
theorem CategoryTheory.Functor.inrCompSum'_inv_app {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] (F : ) (G : ) (X : B) :
(F.inrCompSum' G).inv.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj ())
def CategoryTheory.Functor.inrCompSum' {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] (F : ) (G : ) :
().comp (F.sum' G) G

The sum F.sum' G precomposed with the right inclusion functor is isomorphic to G

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.sum_obj_inl {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] {D : Type u₁} [] (F : ) (G : ) (a : A) :
(F.sum G).obj () = Sum.inl (F.obj a)
@[simp]
theorem CategoryTheory.Functor.sum_obj_inr {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] {D : Type u₁} [] (F : ) (G : ) (c : C) :
(F.sum G).obj () = Sum.inr (G.obj c)
@[simp]
theorem CategoryTheory.Functor.sum_map_inl {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] {D : Type u₁} [] (F : ) (G : ) {a : A} {a' : A} (f : Sum.inl a') :
(F.sum G).map f = F.map f
@[simp]
theorem CategoryTheory.Functor.sum_map_inr {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] {D : Type u₁} [] (F : ) (G : ) {c : C} {c' : C} (f : Sum.inr c') :
(F.sum G).map f = G.map f
def CategoryTheory.NatTrans.sum {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] {D : Type u₁} [] {F : } {G : } {H : } {I : } (α : F G) (β : H I) :
F.sum H G.sum I

The sum of two natural transformations.

Equations
• = { app := fun (X : A C) => match X with | => α.app X | => β.app X, naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatTrans.sum_app_inl {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] {D : Type u₁} [] {F : } {G : } {H : } {I : } (α : F G) (β : H I) (a : A) :
.app () = α.app a
@[simp]
theorem CategoryTheory.NatTrans.sum_app_inr {A : Type u₁} [] {B : Type u₁} [] {C : Type u₁} [] {D : Type u₁} [] {F : } {G : } {H : } {I : } (α : F G) (β : H I) (c : C) :
.app () = β.app c