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

source

instance CategoryTheory.sum (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] :

Category.{v₁, u₁} (C ⊕ D)

sum C D gives the direct sum of two categories.

Equations

CategoryTheory.sum C D = CategoryTheory.Category.mk ⋯ ⋯ ⋯

source

theorem CategoryTheory.hom_inl_inr_false (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] {X : C} {Y : D} (f : Sum.inl X ⟶ Sum.inr Y) :

False

source

theorem CategoryTheory.hom_inr_inl_false (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] {X : C} {Y : D} (f : Sum.inr X ⟶ Sum.inl Y) :

False

source

theorem CategoryTheory.sum_comp_inl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] {P Q R : C} (f : Sum.inl P ⟶ Sum.inl Q) (g : Sum.inl Q ⟶ Sum.inl R) :

CategoryStruct.comp f g = CategoryStruct.comp f g

source

theorem CategoryTheory.sum_comp_inr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] {P Q R : D} (f : Sum.inr P ⟶ Sum.inr Q) (g : Sum.inr Q ⟶ Sum.inr R) :

CategoryStruct.comp f g = CategoryStruct.comp f g

source

def CategoryTheory.Sum.inl_ (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] :

Functor C (C ⊕ D)

inl_ is the functor X ↦ inl X.

Equations

CategoryTheory.Sum.inl_ C D = { obj := fun (X : C) => Sum.inl X, map := fun {x x_1 : C} (f : x ⟶ x_1) => f, map_id := ⋯, map_comp := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Sum.inl__map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] {x✝ x✝¹ : C} (f : x✝ ⟶ x✝¹) :

(inl_ C D).map f = f

source

@[simp]

theorem CategoryTheory.Sum.inl__obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] (X : C) :

(inl_ C D).obj X = Sum.inl X

source

def CategoryTheory.Sum.inr_ (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] :

Functor D (C ⊕ D)

inr_ is the functor X ↦ inr X.

Equations

CategoryTheory.Sum.inr_ C D = { obj := fun (X : D) => Sum.inr X, map := fun {x x_1 : D} (f : x ⟶ x_1) => f, map_id := ⋯, map_comp := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Sum.inr__obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] (X : D) :

(inr_ C D).obj X = Sum.inr X

source

@[simp]

theorem CategoryTheory.Sum.inr__map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] {x✝ x✝¹ : D} (f : x✝ ⟶ x✝¹) :

(inr_ C D).map f = f

source

def CategoryTheory.Sum.swap (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] :

Functor (C ⊕ D) (D ⊕ C)

The functor exchanging two direct summand categories.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Sum.swap_obj_inl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] (X : C) :

(swap C D).obj (Sum.inl X) = Sum.inr X

source

@[simp]

theorem CategoryTheory.Sum.swap_obj_inr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] (X : D) :

(swap C D).obj (Sum.inr X) = Sum.inl X

source

@[simp]

theorem CategoryTheory.Sum.swap_map_inl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] {X Y : C} {f : Sum.inl X ⟶ Sum.inl Y} :

(swap C D).map f = f

source

@[simp]

theorem CategoryTheory.Sum.swap_map_inr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] {X Y : D} {f : Sum.inr X ⟶ Sum.inr Y} :

(swap C D).map f = f

source

def CategoryTheory.Sum.Swap.equivalence (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] :

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

source

@[simp]

theorem CategoryTheory.Sum.Swap.equivalence_functor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] :

(equivalence C D).functor = swap C D

source

@[simp]

theorem CategoryTheory.Sum.Swap.equivalence_inverse (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] :

(equivalence C D).inverse = swap D C

source

instance CategoryTheory.Sum.Swap.isEquivalence (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] :

(swap C D).IsEquivalence

source

def CategoryTheory.Sum.Swap.symmetry (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₁) [Category.{v₁, u₁} D] :

(swap C D).comp (swap D C) ≅ Functor.id (C ⊕ D)

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

Equations

CategoryTheory.Sum.Swap.symmetry C D = (CategoryTheory.Sum.Swap.equivalence C D).unitIso.symm

Instances For

source

def CategoryTheory.Functor.sum {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor A B) (G : Functor C D) :

Functor (A ⊕ C) (B ⊕ D)

The sum of two functors.

Equations

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

Instances For

source

def CategoryTheory.Functor.sum' {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor A C) (G : Functor B C) :

Functor (A ⊕ B) C

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

source

def CategoryTheory.Functor.inlCompSum' {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor A C) (G : Functor B C) :

(Sum.inl_ A B).comp (F.sum' G) ≅ F

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

Equations

F.inlCompSum' G = CategoryTheory.NatIso.ofComponents (fun (x : A) => CategoryTheory.Iso.refl (((CategoryTheory.Sum.inl_ A B).comp (F.sum' G)).obj x)) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Functor.inlCompSum'_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor A C) (G : Functor B C) (X : A) :

(F.inlCompSum' G).inv.app X = CategoryStruct.id ((F.sum' G).obj (Sum.inl X))

source

@[simp]

theorem CategoryTheory.Functor.inlCompSum'_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor A C) (G : Functor B C) (X : A) :

(F.inlCompSum' G).hom.app X = CategoryStruct.id ((F.sum' G).obj (Sum.inl X))

source

def CategoryTheory.Functor.inrCompSum' {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor A C) (G : Functor B C) :

(Sum.inr_ A B).comp (F.sum' G) ≅ G

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

Equations

F.inrCompSum' G = CategoryTheory.NatIso.ofComponents (fun (x : B) => CategoryTheory.Iso.refl (((CategoryTheory.Sum.inr_ A B).comp (F.sum' G)).obj x)) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Functor.inrCompSum'_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor A C) (G : Functor B C) (X : B) :

(F.inrCompSum' G).inv.app X = CategoryStruct.id ((F.sum' G).obj (Sum.inr X))

source

@[simp]

theorem CategoryTheory.Functor.inrCompSum'_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor A C) (G : Functor B C) (X : B) :

(F.inrCompSum' G).hom.app X = CategoryStruct.id ((F.sum' G).obj (Sum.inr X))

source

@[simp]

theorem CategoryTheory.Functor.sum_obj_inl {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor A B) (G : Functor C D) (a : A) :

(F.sum G).obj (Sum.inl a) = Sum.inl (F.obj a)

source

@[simp]

theorem CategoryTheory.Functor.sum_obj_inr {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor A B) (G : Functor C D) (c : C) :

(F.sum G).obj (Sum.inr c) = Sum.inr (G.obj c)

source

@[simp]

theorem CategoryTheory.Functor.sum_map_inl {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor A B) (G : Functor C D) {a a' : A} (f : Sum.inl a ⟶ Sum.inl a') :

(F.sum G).map f = F.map f

source

@[simp]

theorem CategoryTheory.Functor.sum_map_inr {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor A B) (G : Functor C D) {c c' : C} (f : Sum.inr c ⟶ Sum.inr c') :

(F.sum G).map f = G.map f

source

def CategoryTheory.NatTrans.sum {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₁} [Category.{v₁, u₁} D] {F G : Functor A B} {H I : Functor C D} (α : F ⟶ G) (β : H ⟶ I) :

F.sum H ⟶ G.sum I

The sum of two natural transformations.

Equations

CategoryTheory.NatTrans.sum α β = { app := fun (X : A ⊕ C) => match X with | Sum.inl X => α.app X | Sum.inr X => β.app X, naturality := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.NatTrans.sum_app_inl {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₁} [Category.{v₁, u₁} D] {F G : Functor A B} {H I : Functor C D} (α : F ⟶ G) (β : H ⟶ I) (a : A) :

(sum α β).app (Sum.inl a) = α.app a

source

@[simp]

theorem CategoryTheory.NatTrans.sum_app_inr {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₁} [Category.{v₁, u₁} D] {F G : Functor A B} {H I : Functor C D} (α : F ⟶ G) (β : H ⟶ I) (c : C) :

(sum α β).app (Sum.inr c) = β.app c

Documentation

Mathlib.CategoryTheory.Sums.Basic

Binary disjoint unions of categories #