mathlib documentation

category_theory.sums.basic

Binary disjoint unions of categories #

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

We define:

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

@[protected, instance]

sum C D gives the direct sum of two categories.

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

inl_ is the functor X ↦ inl X.

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

inr_ is the functor X ↦ inr X.

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

The functor exchanging two direct summand categories.

Equations
Instances for category_theory.sum.swap
@[simp]
@[simp]
@[simp]
theorem category_theory.sum.swap_map_inl (C : Type u₁) [category_theory.category C] (D : Type u₁) [category_theory.category D] {X Y : C} {f : sum.inl X sum.inl Y} :
@[simp]
theorem category_theory.sum.swap_map_inr (C : Type u₁) [category_theory.category C] (D : Type u₁) [category_theory.category D] {X Y : D} {f : sum.inr X sum.inr Y} :

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

Equations
def category_theory.functor.sum {A : Type u₁} [category_theory.category A] {B : Type u₁} [category_theory.category B] {C : Type u₁} [category_theory.category C] {D : Type u₁} [category_theory.category D] (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₁} [category_theory.category A] {B : Type u₁} [category_theory.category B] {C : Type u₁} [category_theory.category C] {D : Type u₁} [category_theory.category D] (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₁} [category_theory.category A] {B : Type u₁} [category_theory.category B] {C : Type u₁} [category_theory.category C] {D : Type u₁} [category_theory.category D] (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₁} [category_theory.category A] {B : Type u₁} [category_theory.category B] {C : Type u₁} [category_theory.category C] {D : Type u₁} [category_theory.category D] (F : A B) (G : C D) {a a' : A} (f : sum.inl a sum.inl a') :
(F.sum G).map f = F.map f
@[simp]
theorem category_theory.functor.sum_map_inr {A : Type u₁} [category_theory.category A] {B : Type u₁} [category_theory.category B] {C : Type u₁} [category_theory.category C] {D : Type u₁} [category_theory.category D] (F : A B) (G : C D) {c c' : C} (f : sum.inr c sum.inr c') :
(F.sum G).map f = G.map f
def category_theory.nat_trans.sum {A : Type u₁} [category_theory.category A] {B : Type u₁} [category_theory.category B] {C : Type u₁} [category_theory.category C] {D : Type u₁} [category_theory.category D] {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
@[simp]
theorem category_theory.nat_trans.sum_app_inl {A : Type u₁} [category_theory.category A] {B : Type u₁} [category_theory.category B] {C : Type u₁} [category_theory.category C] {D : Type u₁} [category_theory.category D] {F G : A B} {H I : C D} (α : F G) (β : H I) (a : A) :
@[simp]
theorem category_theory.nat_trans.sum_app_inr {A : Type u₁} [category_theory.category A] {B : Type u₁} [category_theory.category B] {C : Type u₁} [category_theory.category C] {D : Type u₁} [category_theory.category D] {F G : A B} {H I : C D} (α : F G) (β : H I) (c : C) :