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 functorC ⥤ C ⊕ Dinr_: the functorD ⥤ C ⊕ Dswap: the functorC ⊕ 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₁)
[category_theory.category C]
(D : Type u₁)
[category_theory.category D] :
category_theory.category (C ⊕ D)
sum C D gives the direct sum of two categories.
Equations
- category_theory.sum C D = {to_category_struct := {to_quiver := {hom := λ (X Y : C ⊕ D), category_theory.sum._match_1 C D X Y}, id := λ (X : C ⊕ D), category_theory.sum._match_2 C D X, comp := λ (X Y Z : C ⊕ D) (f : X ⟶ Y) (g : Y ⟶ Z), category_theory.sum._match_3 C D X Y Z f g}, id_comp' := _, comp_id' := _, assoc' := _}
- category_theory.sum._match_1 C D (sum.inr X) (sum.inr Y) = (X ⟶ Y)
- category_theory.sum._match_1 C D (sum.inr X) (sum.inl Y) = pempty
- category_theory.sum._match_1 C D (sum.inl X) (sum.inr Y) = pempty
- category_theory.sum._match_1 C D (sum.inl X) (sum.inl Y) = (X ⟶ Y)
- category_theory.sum._match_2 C D (sum.inr X) = 𝟙 X
- category_theory.sum._match_2 C D (sum.inl X) = 𝟙 X
- category_theory.sum._match_3 C D (sum.inr X) (sum.inr Y) (sum.inr Z) f g = f ≫ g
- category_theory.sum._match_3 C D (sum.inl X) (sum.inl Y) (sum.inl Z) f g = f ≫ g
@[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) :
@[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) :
@[simp]
theorem
category_theory.sum.inl__obj
(C : Type u₁)
[category_theory.category C]
(D : Type u₁)
[category_theory.category D]
(X : C) :
(category_theory.sum.inl_ C D).obj X = sum.inl X
@[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) :
(category_theory.sum.inl_ C D).map f = f
def
category_theory.sum.inl_
(C : Type u₁)
[category_theory.category C]
(D : Type u₁)
[category_theory.category D] :
inl_ is the functor X ↦ inl X.
@[simp]
theorem
category_theory.sum.inr__obj
(C : Type u₁)
[category_theory.category C]
(D : Type u₁)
[category_theory.category D]
(X : D) :
(category_theory.sum.inr_ C D).obj X = sum.inr X
@[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) :
(category_theory.sum.inr_ C D).map f = f
def
category_theory.sum.inr_
(C : Type u₁)
[category_theory.category C]
(D : Type u₁)
[category_theory.category D] :
inr_ is the functor X ↦ inr X.
def
category_theory.sum.swap
(C : Type u₁)
[category_theory.category C]
(D : Type u₁)
[category_theory.category D] :
The functor exchanging two direct summand categories.
Equations
- category_theory.sum.swap C D = {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) = sum.inl X
- category_theory.sum.swap._match_1 C D (sum.inl X) = sum.inr 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₁)
[category_theory.category C]
(D : Type u₁)
[category_theory.category D]
(X : C) :
(category_theory.sum.swap C D).obj (sum.inl X) = sum.inr X
@[simp]
theorem
category_theory.sum.swap_obj_inr
(C : Type u₁)
[category_theory.category C]
(D : Type u₁)
[category_theory.category D]
(X : D) :
(category_theory.sum.swap C D).obj (sum.inr X) = sum.inl X
@[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} :
(category_theory.sum.swap C D).map f = f
@[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} :
(category_theory.sum.swap C D).map f = f
def
category_theory.sum.swap.equivalence
(C : Type u₁)
[category_theory.category C]
(D : Type u₁)
[category_theory.category D] :
swap gives an equivalence between C ⊕ D and D ⊕ C.
Equations
- category_theory.sum.swap.equivalence C D = category_theory.equivalence.mk (category_theory.sum.swap C D) (category_theory.sum.swap D C) (category_theory.nat_iso.of_components (λ (X : C ⊕ D), category_theory.eq_to_iso _) _) (category_theory.nat_iso.of_components (λ (X : D ⊕ C), category_theory.eq_to_iso _) _)
@[protected, instance]
def
category_theory.sum.swap.is_equivalence
(C : Type u₁)
[category_theory.category C]
(D : Type u₁)
[category_theory.category D] :
def
category_theory.sum.swap.symmetry
(C : Type u₁)
[category_theory.category C]
(D : Type u₁)
[category_theory.category D] :
category_theory.sum.swap C D ⋙ category_theory.sum.swap D C ≅ 𝟭 (C ⊕ D)
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) :
The sum of two functors.
Equations
- F.sum G = {obj := λ (X : A ⊕ C), category_theory.functor.sum._match_1 F G X, map := λ (X Y : A ⊕ C) (f : X ⟶ Y), category_theory.functor.sum._match_2 F G X Y f, map_id' := _, map_comp' := _}
- category_theory.functor.sum._match_1 F G (sum.inr X) = sum.inr (G.obj X)
- category_theory.functor.sum._match_1 F G (sum.inl X) = sum.inl (F.obj X)
- category_theory.functor.sum._match_2 F G (sum.inr X) (sum.inr Y) f = G.map f
- category_theory.functor.sum._match_2 F G (sum.inl X) (sum.inl Y) f = F.map f
@[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) :
@[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) :
@[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') :
@[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') :
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) :
The sum of two natural transformations.
@[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) :
(category_theory.nat_trans.sum α β).app (sum.inl a) = α.app 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) :
(category_theory.nat_trans.sum α β).app (sum.inr c) = β.app c