# mathlibdocumentation

category_theory.sigma.basic

# Disjoint union of categories #

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

inductive category_theory.sigma.sigma_hom {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] :
(Σ (i : I), C i)(Σ (i : I), C i)Type (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 category_theory.sigma.sigma_hom
def category_theory.sigma.sigma_hom.id {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] (X : Σ (i : I), C i) :

The identity morphism on an object.

Equations
@[protected, instance]
def category_theory.sigma.sigma_hom.inhabited {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] (X : Σ (i : I), C i) :
Equations
def category_theory.sigma.sigma_hom.comp {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {X Y Z : Σ (i : I), C i} :

Composition of sigma homomorphisms.

Equations
@[protected, instance]
def category_theory.sigma.sigma_hom.sigma.category_theory.category_struct {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] :
Equations
@[simp]
theorem category_theory.sigma.sigma_hom.comp_def {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] (i : I) (X Y Z : C i) (f : X Y) (g : Y Z) :
theorem category_theory.sigma.sigma_hom.assoc {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] (X Y Z W : Σ (i : I), C i) (f : X Y) (g : Y Z) (h : Z W) :
(f g) h = f g h
theorem category_theory.sigma.sigma_hom.id_comp {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] (X Y : Σ (i : I), C i) (f : X Y) :
𝟙 X f = f
theorem category_theory.sigma.sigma_hom.comp_id {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] (X Y : Σ (i : I), C i) (f : X Y) :
f 𝟙 Y = f
@[protected, instance]
def category_theory.sigma.sigma {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] :
category_theory.category (Σ (i : I), C i)
Equations
def category_theory.sigma.incl {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] (i : I) :
C i Σ (i : I), C i

The inclusion functor into the disjoint union of categories.

Equations
Instances for category_theory.sigma.incl
@[simp]
theorem category_theory.sigma.incl_map {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] (i : I) (X Y : C i) (ᾰ : X Y) :
@[simp]
theorem category_theory.sigma.incl_obj {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {i : I} (X : C i) :
= i, X⟩
@[protected, instance]
def category_theory.sigma.incl.category_theory.full {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] (i : I) :
Equations
• = {preimage := λ (X Y : C i) (_x : , category_theory.sigma.incl.category_theory.full._match_1 i X Y _x, witness' := _}
• category_theory.sigma.incl.category_theory.full._match_1 i X Y = f
@[protected, instance]
def category_theory.sigma.incl.category_theory.faithful {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] (i : I) :
def category_theory.sigma.nat_trans {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} {F G : (Σ (i : I), C i) D} (h : Π (i : I), ) :
F G

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

Equations
• = {app := λ (_x : Σ (i : I), C i), category_theory.sigma.nat_trans._match_1 h _x, naturality' := _}
• category_theory.sigma.nat_trans._match_1 h j, X⟩ = (h j).app X
@[simp]
theorem category_theory.sigma.nat_trans_app {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} {F G : (Σ (i : I), C i) D} (h : Π (i : I), ) (i : I) (X : C i) :
i, X⟩ = (h i).app X
def category_theory.sigma.desc_map {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} (F : Π (i : I), C i D) (X 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
@[simp]
theorem category_theory.sigma.desc_obj {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} (F : Π (i : I), C i D) (X : Σ (i : I), C i) :
= (F X.fst).obj X.snd
def category_theory.sigma.desc {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} (F : Π (i : I), C i D) :
(Σ (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
@[simp]
theorem category_theory.sigma.desc_map_mk {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} (F : Π (i : I), C i D) {i : I} (X Y : C i) (f : X Y) :
= (F i).map f
def category_theory.sigma.incl_desc {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} (F : Π (i : I), C i D) (i : I) :

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

Equations
@[simp]
theorem category_theory.sigma.incl_desc_hom_app {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} (F : Π (i : I), C i D) (i : I) (X : C i) :
= 𝟙 ((F i).obj X)
@[simp]
theorem category_theory.sigma.incl_desc_inv_app {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} (F : Π (i : I), C i D) (i : I) (X : C i) :
= 𝟙 ((F i).obj X)
def category_theory.sigma.desc_uniq {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} (F : Π (i : I), C i D) (q : (Σ (i : I), C i) D) (h : Π (i : I), F i) :

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

Equations
@[simp]
theorem category_theory.sigma.desc_uniq_hom_app {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} (F : Π (i : I), C i D) (q : (Σ (i : I), C i) D) (h : Π (i : I), F i) (i : I) (X : C i) :
.hom.app i, X⟩ = (h i).hom.app X
@[simp]
theorem category_theory.sigma.desc_uniq_inv_app {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} (F : Π (i : I), C i D) (q : (Σ (i : I), C i) D) (h : Π (i : I), F i) (i : I) (X : C i) :
.inv.app i, X⟩ = (h i).inv.app X
@[simp]
theorem category_theory.sigma.nat_iso_inv {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} {q₁ q₂ : (Σ (i : I), C i) D} (h : Π (i : I), ) :
def category_theory.sigma.nat_iso {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} {q₁ q₂ : (Σ (i : I), C i) D} (h : Π (i : I), ) :
q₁ q₂

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

Equations
@[simp]
theorem category_theory.sigma.nat_iso_hom {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : Type u₂} {q₁ q₂ : (Σ (i : I), C i) D} (h : Π (i : I), ) :
def category_theory.sigma.map {I : Type w₁} (C : I → Type u₁) [Π (i : I), ] {J : Type w₂} (g : J → I) :
(Σ (j : J), C (g j)) Σ (i : I), C i

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

Equations
@[simp]
theorem category_theory.sigma.map_obj {I : Type w₁} (C : I → Type u₁) [Π (i : I), ] {J : Type w₂} (g : J → I) (j : J) (X : C (g j)) :
.obj j, X⟩ = g j, X⟩
@[simp]
theorem category_theory.sigma.map_map {I : Type w₁} (C : I → Type u₁) [Π (i : I), ] {J : Type w₂} (g : J → I) {j : J} {X Y : C (g j)} (f : X Y) :
@[simp]
theorem category_theory.sigma.incl_comp_map_hom_app {I : Type w₁} (C : I → Type u₁) [Π (i : I), ] {J : Type w₂} (g : J → I) (j : J) (X : C (g j)) :
X = 𝟙 g j, X⟩
def category_theory.sigma.incl_comp_map {I : Type w₁} (C : I → Type u₁) [Π (i : I), ] {J : Type w₂} (g : J → I) (j : J) :

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

Equations
@[simp]
theorem category_theory.sigma.incl_comp_map_inv_app {I : Type w₁} (C : I → Type u₁) [Π (i : I), ] {J : Type w₂} (g : J → I) (j : J) (X : C (g j)) :
X = 𝟙 g j, X⟩
@[simp]
theorem category_theory.sigma.map_id_hom_app (I : Type w₁) (C : I → Type u₁) [Π (i : I), ] (_x : Σ (i : I), (λ (i : I), (λ (i : I), C (id i)) i) i) :
_x = category_theory.sigma.nat_trans._match_1 (λ (i : I), (category_theory.nat_iso.of_components (λ (X : C i), _).hom) _x
def category_theory.sigma.map_id (I : Type w₁) (C : I → Type u₁) [Π (i : I), ] :
𝟭 (Σ (i : I), C i)

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

Equations
@[simp]
theorem category_theory.sigma.map_id_inv_app (I : Type w₁) (C : I → Type u₁) [Π (i : I), ] (_x : Σ (i : I), (λ (i : I), (λ (i : I), C (id i)) i) i) :
_x = category_theory.sigma.nat_trans._match_1 (λ (i : I), (category_theory.nat_iso.of_components (λ (X : C i), _).inv) _x
def category_theory.sigma.map_comp {I : Type w₁} (C : I → Type u₁) [Π (i : I), ] {J : Type w₂} {K : Type w₃} (f : K → J) (g : J → I) :
f (g f)

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

Equations
@[simp]
theorem category_theory.sigma.map_comp_inv_app {I : Type w₁} (C : I → Type u₁) [Π (i : I), ] {J : Type w₂} {K : Type w₃} (f : K → J) (g : J → I) (X : Σ (i : K), (λ (j : K), (C g) (f j)) i) :
.inv.app X = (category_theory.sigma.desc_uniq._match_1 (λ (j : K), category_theory.sigma.incl (g (f j))) (category_theory.sigma.map (C g) f (λ (k : K), X).inv
@[simp]
theorem category_theory.sigma.map_comp_hom_app {I : Type w₁} (C : I → Type u₁) [Π (i : I), ] {J : Type w₂} {K : Type w₃} (f : K → J) (g : J → I) (X : Σ (i : K), (λ (j : K), (C g) (f j)) i) :
.hom.app X = (category_theory.sigma.desc_uniq._match_1 (λ (j : K), category_theory.sigma.incl (g (f j))) (category_theory.sigma.map (C g) f (λ (k : K), X).hom
def category_theory.sigma.functor.sigma {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : I → Type u₁} [Π (i : I), ] (F : Π (i : I), C i D i) :
(Σ (i : I), C i) Σ (i : I), D i

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

Equations
def category_theory.sigma.nat_trans.sigma {I : Type w₁} {C : I → Type u₁} [Π (i : I), ] {D : I → Type u₁} [Π (i : I), ] {F G : Π (i : I), C i D i} (α : Π (i : I), F i G i) :

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

Equations