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 provide an induction principle Sum.homInduction to reason and work with morphisms in this category.

The sum of two functors F : A ⥤ C and G : B ⥤ C is a functor A ⊕ B ⥤ C, written F.sum' G. This construction should be preferred when defining functors out of a sum.

We provide natural isomorphisms inlCompSum' : inl_ ⋙ F.sum' G ≅ F and inrCompSum' : inl_ ⋙ F.sum' G ≅ G.

Furthermore, we provide Functor.sumIsoExt, which constructs a natural isomorphism of functors out of a sum out of natural isomorphism with their precomposition with the inclusion. This construction sholud be preferred when trying to construct isomorphisms between functors out of a sum.

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

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

sum C D gives the direct sum of two categories.

Equations

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

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

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

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 Y : C} (f : X ⟶ Y) => { down := f }, map_id := ⋯, map_comp := ⋯ }

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

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 Y : D} (f : X ⟶ Y) => { down := f }, map_id := ⋯, map_comp := ⋯ }

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

def CategoryTheory.Sum.homInduction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : {x y : C ⊕ D} → (x ⟶ y) → Sort u_1} (inl : (x y : C) → (f : x ⟶ y) → P ((inl_ C D).map f)) (inr : (x y : D) → (f : x ⟶ y) → P ((inr_ C D).map f)) {x y : C ⊕ D} (f : x ⟶ y) : P f

An induction principle for morphisms in a sum of category: a morphism is either of the form (inl_ _ _).map _ or of the form (inr_ _ _).map _).

Equations

• CategoryTheory.Sum.homInduction inl inr f_2 = inl x_2 y_2 f_2.down
• CategoryTheory.Sum.homInduction inl inr f_2 = inr x_2 y_2 f_2.down

@[simp]

theorem CategoryTheory.Sum.homInduction_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : {x y : C ⊕ D} → (x ⟶ y) → Sort u_1} (inl : (x y : C) → (f : x ⟶ y) → P ((inl_ C D).map f)) (inr : (x y : D) → (f : x ⟶ y) → P ((inr_ C D).map f)) {x y : C} (f : x ⟶ y) : homInduction inl inr ((inl_ C D).map f) = inl x y f

@[simp]

theorem CategoryTheory.Sum.homInduction_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {P : {x y : C ⊕ D} → (x ⟶ y) → Sort u_1} (inl : (x y : C) → (f : x ⟶ y) → P ((inl_ C D).map f)) (inr : (x y : D) → (f : x ⟶ y) → P ((inr_ C D).map f)) {x y : D} (f : x ⟶ y) : homInduction inl inr ((inr_ C D).map f) = inr x y f

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

The sum of two functors that land in a given category C.

Equations

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

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)) ⋯

@[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))

@[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))

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)) ⋯

@[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))

@[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))

@[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] (F : Functor A C) (G : Functor B C) (a : A) : (F.sum' G).obj (Sum.inl a) = F.obj a

@[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] (F : Functor A C) (G : Functor B C) (b : B) : (F.sum' G).obj (Sum.inr b) = G.obj b

@[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] (F : Functor A C) (G : Functor B C) {a a' : A} (f : a ⟶ a') : (F.sum' G).map ((Sum.inl_ A B).map f) = F.map f

@[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] (F : Functor A C) (G : Functor B C) {b b' : B} (f : b ⟶ b') : (F.sum' G).map ((Sum.inr_ A B).map f) = G.map f

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

• F.sum G = (F.comp (CategoryTheory.Sum.inl_ B D)).sum' (G.comp (CategoryTheory.Sum.inr_ B D))

@[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)

@[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)

@[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 : a ⟶ a') : (F.sum G).map ((Sum.inl_ A C).map f) = (Sum.inl_ B D).map (F.map f)

@[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 : c ⟶ c') : (F.sum G).map ((Sum.inr_ A C).map f) = (Sum.inr_ B D).map (G.map f)

def CategoryTheory.Functor.sumIsoExt {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor (A ⊕ B) C} (e₁ : (Sum.inl_ A B).comp F ≅ (Sum.inl_ A B).comp G) (e₂ : (Sum.inr_ A B).comp F ≅ (Sum.inr_ A B).comp G) : F ≅ G

A functor out of a sum is uniquely characterized by its precompositions with inl_ and inr_.

Equations

• CategoryTheory.Functor.sumIsoExt e₁ e₂ = CategoryTheory.NatIso.ofComponents (fun (x : A ⊕ B) => match x with | Sum.inl x => e₁.app x | Sum.inr x => e₂.app x) ⋯

@[simp]

theorem CategoryTheory.Functor.sumIsoExt_hom_app_inl {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor (A ⊕ B) C} (e₁ : (Sum.inl_ A B).comp F ≅ (Sum.inl_ A B).comp G) (e₂ : (Sum.inr_ A B).comp F ≅ (Sum.inr_ A B).comp G) (a : A) : (sumIsoExt e₁ e₂).hom.app (Sum.inl a) = e₁.hom.app a

@[simp]

theorem CategoryTheory.Functor.sumIsoExt_hom_app_inr {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor (A ⊕ B) C} (e₁ : (Sum.inl_ A B).comp F ≅ (Sum.inl_ A B).comp G) (e₂ : (Sum.inr_ A B).comp F ≅ (Sum.inr_ A B).comp G) (b : B) : (sumIsoExt e₁ e₂).hom.app (Sum.inr b) = e₂.hom.app b

@[simp]

theorem CategoryTheory.Functor.sumIsoExt_inv_app_inl {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor (A ⊕ B) C} (e₁ : (Sum.inl_ A B).comp F ≅ (Sum.inl_ A B).comp G) (e₂ : (Sum.inr_ A B).comp F ≅ (Sum.inr_ A B).comp G) (a : A) : (sumIsoExt e₁ e₂).inv.app (Sum.inl a) = e₁.inv.app a

@[simp]

theorem CategoryTheory.Functor.sumIsoExt_inv_app_inr {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor (A ⊕ B) C} (e₁ : (Sum.inl_ A B).comp F ≅ (Sum.inl_ A B).comp G) (e₂ : (Sum.inr_ A B).comp F ≅ (Sum.inr_ A B).comp G) (b : B) : (sumIsoExt e₁ e₂).inv.app (Sum.inr b) = e₂.inv.app b

def CategoryTheory.Functor.isoSum {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor (A ⊕ B) C) : F ≅ ((Sum.inl_ A B).comp F).sum' ((Sum.inr_ A B).comp F)

Any functor out of a sum is the sum of its precomposition with the inclusions.

Equations

• F.isoSum = CategoryTheory.Functor.sumIsoExt (CategoryTheory.Iso.refl ((CategoryTheory.Sum.inl_ A B).comp F)) (CategoryTheory.Iso.refl ((CategoryTheory.Sum.inr_ A B).comp F))

@[simp]

theorem CategoryTheory.Functor.isoSum_hom_app_inl {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor (A ⊕ B) C) (a : A) : F.isoSum.hom.app (Sum.inl a) = CategoryStruct.id (F.obj (Sum.inl a))

@[simp]

theorem CategoryTheory.Functor.isoSum_hom_app_inr {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor (A ⊕ B) C) (b : B) : F.isoSum.hom.app (Sum.inr b) = CategoryStruct.id (F.obj (Sum.inr b))

@[simp]

theorem CategoryTheory.Functor.isoSum_inv_app_inl {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor (A ⊕ B) C) (a : A) : F.isoSum.inv.app (Sum.inl a) = CategoryStruct.id (F.obj (Sum.inl a))

@[simp]

theorem CategoryTheory.Functor.isoSum_inv_app_inr {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor (A ⊕ B) C) (b : B) : F.isoSum.inv.app (Sum.inr b) = CategoryStruct.id (F.obj (Sum.inr b))

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] {F G : Functor A C} {H I : Functor B C} (α : F ⟶ G) (β : H ⟶ I) : F.sum' H ⟶ G.sum' I

The sum of two natural transformations, where all functors have the same target category.

Equations

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

@[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] {F G : Functor A C} {H I : Functor B C} (α : F ⟶ G) (β : H ⟶ I) (a : A) : (sum' α β).app (Sum.inl a) = α.app a

@[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] {F G : Functor A C} {H I : Functor B C} (α : F ⟶ G) (β : H ⟶ I) (b : B) : (sum' α β).app (Sum.inr b) = β.app b

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

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

@[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) = (Sum.inl_ B D).map (α.app a)

@[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) = (Sum.inr_ B D).map (β.app c)

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

• CategoryTheory.Sum.swap C D = (CategoryTheory.Sum.inr_ D C).sum' (CategoryTheory.Sum.inl_ D C)

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

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

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

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

def CategoryTheory.Sum.swapCompInl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (inl_ C D).comp (swap C D) ≅ inr_ D C

Precomposing swap with the left inclusion gives the right inclusion.

Equations

• CategoryTheory.Sum.swapCompInl C D = ((CategoryTheory.Sum.inr_ D C).inlCompSum' (CategoryTheory.Sum.inl_ D C)).symm

@[simp]

theorem CategoryTheory.Sum.swapCompInl_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C) : (swapCompInl C D).hom.app X = CategoryStruct.id (Sum.inr X)

@[simp]

theorem CategoryTheory.Sum.swapCompInl_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : C) : (swapCompInl C D).inv.app X = CategoryStruct.id (Sum.inr X)

def CategoryTheory.Sum.swapCompInr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (inr_ C D).comp (swap C D) ≅ inl_ D C

Precomposing swap with the right inclusion gives the leftt inclusion.

Equations

• CategoryTheory.Sum.swapCompInr C D = ((CategoryTheory.Sum.inr_ D C).inrCompSum' (CategoryTheory.Sum.inl_ D C)).symm

@[simp]

theorem CategoryTheory.Sum.swapCompInr_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : D) : (swapCompInr C D).hom.app X = CategoryStruct.id (Sum.inl X)

@[simp]

theorem CategoryTheory.Sum.swapCompInr_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (X : D) : (swapCompInr C D).inv.app X = CategoryStruct.id (Sum.inl X)

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.

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

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

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

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