# Disjoint union of categories #

We define the category structure on a sigma-type (disjoint union) of categories.

inductive CategoryTheory.Sigma.SigmaHom {I : Type w₁} {C : IType u₁} [(i : I) → ] :
(i : I) × C i(i : I) × C iType (max w₁ v₁ u₁)

The type of morphisms of a disjoint union of categories: for X : C i and Y : C j, a morphism (i, X) ⟶ (j, Y) if i = j is just a morphism X ⟶ Y, and if i ≠ j there are no such morphisms.

Instances For
def CategoryTheory.Sigma.SigmaHom.id {I : Type w₁} {C : IType u₁} [(i : I) → ] (X : (i : I) × C i) :

The identity morphism on an object.

Equations
• = match x with | fst, snd =>
Instances For
instance CategoryTheory.Sigma.SigmaHom.instInhabited {I : Type w₁} {C : IType u₁} [(i : I) → ] (X : (i : I) × C i) :
Equations
• = { default := }
def CategoryTheory.Sigma.SigmaHom.comp {I : Type w₁} {C : IType u₁} [(i : I) → ] {X : (i : I) × C i} {Y : (i : I) × C i} {Z : (i : I) × C i} :

Composition of sigma homomorphisms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Sigma.SigmaHom.instCategoryStructSigma {I : Type w₁} {C : IType u₁} [(i : I) → ] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CategoryTheory.Sigma.SigmaHom.comp_def {I : Type w₁} {C : IType u₁} [(i : I) → ] (i : I) (X : C i) (Y : C i) (Z : C i) (f : X Y) (g : Y Z) :
theorem CategoryTheory.Sigma.SigmaHom.assoc {I : Type w₁} {C : IType u₁} [(i : I) → ] {X : (i : I) × C i} {Y : (i : I) × C i} {Z : (i : I) × C i} {W : (i : I) × C i} (f : X Y) (g : Y Z) (h : Z W) :
theorem CategoryTheory.Sigma.SigmaHom.id_comp {I : Type w₁} {C : IType u₁} [(i : I) → ] {X : (i : I) × C i} {Y : (i : I) × C i} (f : X Y) :
theorem CategoryTheory.Sigma.SigmaHom.comp_id {I : Type w₁} {C : IType u₁} [(i : I) → ] {X : (i : I) × C i} {Y : (i : I) × C i} (f : X Y) :
instance CategoryTheory.Sigma.sigma {I : Type w₁} {C : IType u₁} [(i : I) → ] :
Equations
• CategoryTheory.Sigma.sigma =
@[simp]
theorem CategoryTheory.Sigma.incl_map {I : Type w₁} {C : IType u₁} [(i : I) → ] (i : I) :
∀ {X Y : C i} (a : X Y),
def CategoryTheory.Sigma.incl {I : Type w₁} {C : IType u₁} [(i : I) → ] (i : I) :
CategoryTheory.Functor (C i) ((i : I) × C i)

The inclusion functor into the disjoint union of categories.

Equations
• = { obj := fun (X : C i) => i, X, map := fun {X Y : C i} => CategoryTheory.Sigma.SigmaHom.mk, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Sigma.incl_obj {I : Type w₁} {C : IType u₁} [(i : I) → ] {i : I} (X : C i) :
.obj X = i, X
instance CategoryTheory.Sigma.instFullSigmaIncl {I : Type w₁} {C : IType u₁} [(i : I) → ] (i : I) :
.Full
Equations
• =
instance CategoryTheory.Sigma.instFaithfulSigmaIncl {I : Type w₁} {C : IType u₁} [(i : I) → ] (i : I) :
.Faithful
Equations
• =
def CategoryTheory.Sigma.natTrans {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] {F : CategoryTheory.Functor ((i : I) × C i) D} {G : CategoryTheory.Functor ((i : I) × C i) D} (h : (i : I) → .comp F .comp G) :
F G

To build a natural transformation over the sigma category, it suffices to specify it restricted to each subcategory.

Equations
• = { app := fun (x : (i : I) × C i) => match x with | j, X => (h j).app X, naturality := }
Instances For
@[simp]
theorem CategoryTheory.Sigma.natTrans_app {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] {F : CategoryTheory.Functor ((i : I) × C i) D} {G : CategoryTheory.Functor ((i : I) × C i) D} (h : (i : I) → .comp F .comp G) (i : I) (X : C i) :
.app i, X = (h i).app X
def CategoryTheory.Sigma.descMap {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] (F : (i : I) → CategoryTheory.Functor (C i) D) (X : (i : I) × C i) (Y : (i : I) × C i) :
(X Y)((F X.fst).obj X.snd (F Y.fst).obj Y.snd)

(Implementation). An auxiliary definition to build the functor desc.

Equations
Instances For
@[simp]
theorem CategoryTheory.Sigma.desc_obj {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] (F : (i : I) → CategoryTheory.Functor (C i) D) (X : (i : I) × C i) :
.obj X = (F X.fst).obj X.snd
def CategoryTheory.Sigma.desc {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] (F : (i : I) → CategoryTheory.Functor (C i) D) :
CategoryTheory.Functor ((i : I) × C i) D

Given a collection of functors F i : C i ⥤ D, we can produce a functor (Σ i, C i) ⥤ D.

The produced functor desc F satisfies: incl i ⋙ desc F ≅ F i, i.e. restricted to just the subcategory C i, desc F agrees with F i, and it is unique (up to natural isomorphism) with this property.

This witnesses that the sigma-type is the coproduct in Cat.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Sigma.desc_map_mk {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] (F : (i : I) → CategoryTheory.Functor (C i) D) {i : I} (X : C i) (Y : C i) (f : X Y) :
= (F i).map f
def CategoryTheory.Sigma.inclDesc {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] (F : (i : I) → CategoryTheory.Functor (C i) D) (i : I) :
.comp F i

This shows that when desc F is restricted to just the subcategory C i, desc F agrees with F i.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Sigma.inclDesc_hom_app {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] (F : (i : I) → CategoryTheory.Functor (C i) D) (i : I) (X : C i) :
.hom.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
@[simp]
theorem CategoryTheory.Sigma.inclDesc_inv_app {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] (F : (i : I) → CategoryTheory.Functor (C i) D) (i : I) (X : C i) :
.inv.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
def CategoryTheory.Sigma.descUniq {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] (F : (i : I) → CategoryTheory.Functor (C i) D) (q : CategoryTheory.Functor ((i : I) × C i) D) (h : (i : I) → .comp q F i) :

If q when restricted to each subcategory C i agrees with F i, then q is isomorphic to desc F.

Equations
Instances For
@[simp]
theorem CategoryTheory.Sigma.descUniq_hom_app {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] (F : (i : I) → CategoryTheory.Functor (C i) D) (q : CategoryTheory.Functor ((i : I) × C i) D) (h : (i : I) → .comp q F i) (i : I) (X : C i) :
().hom.app i, X = (h i).hom.app X
@[simp]
theorem CategoryTheory.Sigma.descUniq_inv_app {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] (F : (i : I) → CategoryTheory.Functor (C i) D) (q : CategoryTheory.Functor ((i : I) × C i) D) (h : (i : I) → .comp q F i) (i : I) (X : C i) :
().inv.app i, X = (h i).inv.app X
@[simp]
theorem CategoryTheory.Sigma.natIso_inv {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] {q₁ : CategoryTheory.Functor ((i : I) × C i) D} {q₂ : CategoryTheory.Functor ((i : I) × C i) D} (h : (i : I) → .comp q₁ .comp q₂) :
.inv = CategoryTheory.Sigma.natTrans fun (i : I) => (h i).inv
@[simp]
theorem CategoryTheory.Sigma.natIso_hom {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] {q₁ : CategoryTheory.Functor ((i : I) × C i) D} {q₂ : CategoryTheory.Functor ((i : I) × C i) D} (h : (i : I) → .comp q₁ .comp q₂) :
.hom = CategoryTheory.Sigma.natTrans fun (i : I) => (h i).hom
def CategoryTheory.Sigma.natIso {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : Type u₂} [] {q₁ : CategoryTheory.Functor ((i : I) × C i) D} {q₂ : CategoryTheory.Functor ((i : I) × C i) D} (h : (i : I) → .comp q₁ .comp q₂) :
q₁ q₂

If q₁ and q₂ when restricted to each subcategory C i agree, then q₁ and q₂ are isomorphic.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Sigma.map {I : Type w₁} (C : IType u₁) [(i : I) → ] {J : Type w₂} (g : JI) :
CategoryTheory.Functor ((j : J) × C (g j)) ((i : I) × C i)

A function J → I induces a functor Σ j, C (g j) ⥤ Σ i, C i.

Equations
Instances For
@[simp]
theorem CategoryTheory.Sigma.map_obj {I : Type w₁} (C : IType u₁) [(i : I) → ] {J : Type w₂} (g : JI) (j : J) (X : C (g j)) :
().obj j, X = g j, X
@[simp]
theorem CategoryTheory.Sigma.map_map {I : Type w₁} (C : IType u₁) [(i : I) → ] {J : Type w₂} (g : JI) {j : J} {X : C (g j)} {Y : C (g j)} (f : X Y) :
@[simp]
theorem CategoryTheory.Sigma.inclCompMap_inv_app {I : Type w₁} (C : IType u₁) [(i : I) → ] {J : Type w₂} (g : JI) (j : J) (X : C (g j)) :
().inv.app X = CategoryTheory.CategoryStruct.id g j, X
@[simp]
theorem CategoryTheory.Sigma.inclCompMap_hom_app {I : Type w₁} (C : IType u₁) [(i : I) → ] {J : Type w₂} (g : JI) (j : J) (X : C (g j)) :
().hom.app X = CategoryTheory.CategoryStruct.id g j, X
def CategoryTheory.Sigma.inclCompMap {I : Type w₁} (C : IType u₁) [(i : I) → ] {J : Type w₂} (g : JI) (j : J) :
.comp ()

The functor Sigma.map C g restricted to the subcategory C j acts as the inclusion of g j.

Equations
Instances For
@[simp]
theorem CategoryTheory.Sigma.mapId_hom_app (I : Type w₁) (C : IType u₁) [(i : I) → ] :
∀ (x : (i : I) × (fun (i : I) => (fun (i : I) => C (id i)) i) i), .hom.app x = CategoryTheory.CategoryStruct.id x.fst, x.snd
@[simp]
theorem CategoryTheory.Sigma.mapId_inv_app (I : Type w₁) (C : IType u₁) [(i : I) → ] :
∀ (x : (i : I) × (fun (i : I) => (fun (i : I) => C (id i)) i) i), .inv.app x = CategoryTheory.CategoryStruct.id x.fst, x.snd
def CategoryTheory.Sigma.mapId (I : Type w₁) (C : IType u₁) [(i : I) → ] :
CategoryTheory.Functor.id ((i : I) × C i)

The functor Sigma.map applied to the identity function is just the identity functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Sigma.mapComp_inv_app {I : Type w₁} (C : IType u₁) [(i : I) → ] {J : Type w₂} {K : Type w₃} (f : KJ) (g : JI) (X : (i : K) × (fun (i : K) => C (g (f i))) i) :
().inv.app X = CategoryTheory.CategoryStruct.id g (f X.fst), X.snd
@[simp]
theorem CategoryTheory.Sigma.mapComp_hom_app {I : Type w₁} (C : IType u₁) [(i : I) → ] {J : Type w₂} {K : Type w₃} (f : KJ) (g : JI) (X : (i : K) × (fun (i : K) => C (g (f i))) i) :
().hom.app X = CategoryTheory.CategoryStruct.id g (f X.fst), X.snd
def CategoryTheory.Sigma.mapComp {I : Type w₁} (C : IType u₁) [(i : I) → ] {J : Type w₂} {K : Type w₃} (f : KJ) (g : JI) :
(CategoryTheory.Sigma.map (fun (x : J) => C (g x)) f).comp () CategoryTheory.Sigma.map C (g f)

The functor Sigma.map applied to a composition is a composition of functors.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Sigma.Functor.sigma {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : IType u₁} [(i : I) → ] (F : (i : I) → CategoryTheory.Functor (C i) (D i)) :
CategoryTheory.Functor ((i : I) × C i) ((i : I) × D i)

Assemble an I-indexed family of functors into a functor between the sigma types.

Equations
Instances For
def CategoryTheory.Sigma.natTrans.sigma {I : Type w₁} {C : IType u₁} [(i : I) → ] {D : IType u₁} [(i : I) → ] {F : (i : I) → CategoryTheory.Functor (C i) (D i)} {G : (i : I) → CategoryTheory.Functor (C i) (D i)} (α : (i : I) → F i G i) :

Assemble an I-indexed family of natural transformations into a single natural transformation.

Equations
Instances For