# mathlib3documentation

category_theory.sums.basic

# Binary disjoint unions of categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 β.

@[protected, instance]
def category_theory.sum (C : Type u₁) (D : Type u₁)  :

sum C D gives the direct sum of two categories.

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

inl_ is the functor X ↦ inl X.

Equations
@[simp]
theorem category_theory.sum.inr__obj (C : Type u₁) (D : Type u₁) (X : D) :
.obj X =
@[simp]
theorem category_theory.sum.inr__map (C : Type u₁) (D : Type u₁) (X Y : D) (f : X Y) :
.map f = f
def category_theory.sum.inr_ (C : Type u₁) (D : Type u₁)  :
D C D

inr_ is the functor X ↦ inr X.

Equations
def category_theory.sum.swap (C : Type u₁) (D : Type u₁)  :
C D D C

The functor exchanging two direct summand categories.

Equations
• = {obj := λ (X : C D), category_theory.sum.swap._match_1 C D X, map := λ (X Y : C D) (f : X Y), category_theory.sum.swap._match_2 C D X Y f, map_id' := _, map_comp' := _}
• category_theory.sum.swap._match_1 C D (sum.inr X) =
• category_theory.sum.swap._match_1 C D (sum.inl X) =
• category_theory.sum.swap._match_2 C D (sum.inr X) (sum.inr Y) f = f
• category_theory.sum.swap._match_2 C D (sum.inl X) (sum.inl Y) f = f
Instances for category_theory.sum.swap
@[simp]
theorem category_theory.sum.swap_obj_inl (C : Type u₁) (D : Type u₁) (X : C) :
.obj (sum.inl X) =
@[simp]
theorem category_theory.sum.swap_obj_inr (C : Type u₁) (D : Type u₁) (X : D) :
.obj (sum.inr X) =
@[simp]
theorem category_theory.sum.swap_map_inl (C : Type u₁) (D : Type u₁) {X Y : C} {f : } :
.map f = f
@[simp]
theorem category_theory.sum.swap_map_inr (C : Type u₁) (D : Type u₁) {X Y : D} {f : } :
.map f = f
def category_theory.sum.swap.equivalence (C : Type u₁) (D : Type u₁)  :
C D D C

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

Equations
@[protected, instance]
Equations
def category_theory.sum.swap.symmetry (C : Type u₁) (D : Type u₁)  :
𝟭 (C D)

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

Equations
def category_theory.functor.sum {A : Type u₁} {B : Type u₁} {C : Type u₁} {D : Type u₁} (F : A B) (G : C D) :
A C B D

The sum of two functors.

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

The sum of two natural transformations.

Equations
• = {app := λ (X : A C), category_theory.nat_trans.sum._match_1 α β X, naturality' := _}
• category_theory.nat_trans.sum._match_1 α β (sum.inr X) = β.app X
• category_theory.nat_trans.sum._match_1 α β (sum.inl X) = α.app X
@[simp]
theorem category_theory.nat_trans.sum_app_inl {A : Type u₁} {B : Type u₁} {C : Type u₁} {D : Type u₁} {F G : A B} {H I : C D} (α : F G) (β : H I) (a : A) :
(sum.inl a) = α.app a
@[simp]
theorem category_theory.nat_trans.sum_app_inr {A : Type u₁} {B : Type u₁} {C : Type u₁} {D : Type u₁} {F G : A B} {H I : C D} (α : F G) (β : H I) (c : C) :
(sum.inr c) = β.app c