mathlib3 documentation

category_theory.sigma.basic

Disjoint union of categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

The identity morphism on an object.

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

Composition of sigma homomorphisms.

Equations
source
@[protected, instance]
def category_theory.sigma.sigma_hom.sigma.category_theory.category_struct {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] :
category_theory.category_struct (Σ (i : I), C i)
Equations
source
@[simp]
theorem category_theory.sigma.sigma_hom.comp_def {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] (i : I) (X Y Z : C i) (f : X ⟶ Y) (g : Y ⟶ Z) :
(category_theory.sigma.sigma_hom.mk f).comp (category_theory.sigma.sigma_hom.mk g) = category_theory.sigma.sigma_hom.mk (f ≫ g)
source
theorem category_theory.sigma.sigma_hom.assoc {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] (X Y Z W : Σ (i : I), C i) (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) :
(f ≫ g) ≫ h = f ≫ g ≫ h
source
theorem category_theory.sigma.sigma_hom.id_comp {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] (X Y : Σ (i : I), C i) (f : X ⟶ Y) :
𝟙 X ≫ f = f
source
theorem category_theory.sigma.sigma_hom.comp_id {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] (X Y : Σ (i : I), C i) (f : X ⟶ Y) :
f ≫ 𝟙 Y = f
source
@[protected, instance]
def category_theory.sigma.sigma {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] :
category_theory.category (Σ (i : I), C i)
Equations
source
def category_theory.sigma.incl {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C 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
source
@[simp]
theorem category_theory.sigma.incl_map {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] (i : I) (X Y : C i) (ᾰ : X ⟶ Y) :
(category_theory.sigma.incl i).map ᾰ = category_theory.sigma.sigma_hom.mk ᾰ
source
@[simp]
theorem category_theory.sigma.incl_obj {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {i : I} (X : C i) :
(category_theory.sigma.incl i).obj X = ⟨i, X⟩
source
@[protected, instance]
def category_theory.sigma.incl.category_theory.full {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] (i : I) :
category_theory.full (category_theory.sigma.incl i)
Equations
source
@[protected, instance]
def category_theory.sigma.incl.category_theory.faithful {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] (i : I) :
category_theory.faithful (category_theory.sigma.incl i)
source
def category_theory.sigma.nat_trans {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : Type u₂} [category_theory.category D] {F G : (Σ (i : I), C i) ⥤ D} (h : Π (i : I), category_theory.sigma.incl i ⋙ F ⟶ category_theory.sigma.incl i ⋙ G) :
F ⟶ G

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

Equations
source
@[simp]
theorem category_theory.sigma.nat_trans_app {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : Type u₂} [category_theory.category D] {F G : (Σ (i : I), C i) ⥤ D} (h : Π (i : I), category_theory.sigma.incl i ⋙ F ⟶ category_theory.sigma.incl i ⋙ G) (i : I) (X : C i) :
(category_theory.sigma.nat_trans h).app ⟨i, X⟩ = (h i).app X
source
def category_theory.sigma.desc_map {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : Type u₂} [category_theory.category D] (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
source
@[simp]
theorem category_theory.sigma.desc_obj {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : Type u₂} [category_theory.category D] (F : Π (i : I), C i ⥤ D) (X : Σ (i : I), C i) :
(category_theory.sigma.desc F).obj X = (F X.fst).obj X.snd
source
def category_theory.sigma.desc {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : Type u₂} [category_theory.category D] (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
source
@[simp]
theorem category_theory.sigma.desc_map_mk {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : Type u₂} [category_theory.category D] (F : Π (i : I), C i ⥤ D) {i : I} (X Y : C i) (f : X ⟶ Y) :
(category_theory.sigma.desc F).map (category_theory.sigma.sigma_hom.mk f) = (F i).map f
source
def category_theory.sigma.incl_desc {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : Type u₂} [category_theory.category D] (F : Π (i : I), C i ⥤ D) (i : I) :
category_theory.sigma.incl i ⋙ category_theory.sigma.desc F ≅ F i

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

Equations
source
@[simp]
theorem category_theory.sigma.incl_desc_hom_app {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : Type u₂} [category_theory.category D] (F : Π (i : I), C i ⥤ D) (i : I) (X : C i) :
(category_theory.sigma.incl_desc F i).hom.app X = 𝟙 ((F i).obj X)
source
@[simp]
theorem category_theory.sigma.incl_desc_inv_app {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : Type u₂} [category_theory.category D] (F : Π (i : I), C i ⥤ D) (i : I) (X : C i) :
(category_theory.sigma.incl_desc F i).inv.app X = 𝟙 ((F i).obj X)
source
def category_theory.sigma.desc_uniq {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : Type u₂} [category_theory.category D] (F : Π (i : I), C i ⥤ D) (q : (Σ (i : I), C i) ⥤ D) (h : Π (i : I), category_theory.sigma.incl i ⋙ q ≅ F i) :
q ≅ category_theory.sigma.desc F

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

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

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

Equations
source
@[simp]
theorem category_theory.sigma.nat_iso_hom {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : Type u₂} [category_theory.category D] {q₁ q₂ : (Σ (i : I), C i) ⥤ D} (h : Π (i : I), category_theory.sigma.incl i ⋙ q₁ ≅ category_theory.sigma.incl i ⋙ q₂) :
(category_theory.sigma.nat_iso h).hom = category_theory.sigma.nat_trans (λ (i : I), (h i).hom)
source
def category_theory.sigma.map {I : Type w₁} (C : I → Type u₁) [Π (i : I), category_theory.category (C 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
source
@[simp]
theorem category_theory.sigma.map_obj {I : Type w₁} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₂} (g : J → I) (j : J) (X : C (g j)) :
(category_theory.sigma.map C g).obj ⟨j, X⟩ = ⟨g j, X⟩
source
@[simp]
theorem category_theory.sigma.map_map {I : Type w₁} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₂} (g : J → I) {j : J} {X Y : C (g j)} (f : X ⟶ Y) :
(category_theory.sigma.map C g).map (category_theory.sigma.sigma_hom.mk f) = category_theory.sigma.sigma_hom.mk f
source
@[simp]
theorem category_theory.sigma.incl_comp_map_hom_app {I : Type w₁} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₂} (g : J → I) (j : J) (X : C (g j)) :
(category_theory.sigma.incl_comp_map C g j).hom.app X = 𝟙 ⟨g j, X⟩
source
def category_theory.sigma.incl_comp_map {I : Type w₁} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₂} (g : J → I) (j : J) :
category_theory.sigma.incl j ⋙ category_theory.sigma.map C g ≅ category_theory.sigma.incl (g j)

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

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

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

Equations
source
@[simp]
theorem category_theory.sigma.map_id_inv_app (I : Type w₁) (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] (_x : Σ (i : I), (λ (i : I), (λ (i : I), C (id i)) i) i) :
(category_theory.sigma.map_id I C).inv.app _x = category_theory.sigma.nat_trans._match_1 (λ (i : I), (category_theory.nat_iso.of_components (λ (X : C i), category_theory.iso.refl ⟨i, X⟩) _).inv) _x
source
def category_theory.sigma.map_comp {I : Type w₁} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₂} {K : Type w₃} (f : K → J) (g : J → I) :
category_theory.sigma.map (C ∘ g) f ⋙ category_theory.sigma.map C g ≅ category_theory.sigma.map C (g ∘ f)

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

Equations
source
@[simp]
theorem category_theory.sigma.map_comp_inv_app {I : Type w₁} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₂} {K : Type w₃} (f : K → J) (g : J → I) (X : Σ (i : K), (λ (j : K), (C ∘ g) (f j)) i) :
(category_theory.sigma.map_comp C f g).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 ⋙ category_theory.sigma.map C g) (λ (k : K), category_theory.iso_whisker_right (category_theory.sigma.incl_comp_map (C ∘ g) f k) (category_theory.sigma.map C g) ≪≫ category_theory.sigma.incl_comp_map C g (f k)) X).inv
source
@[simp]
theorem category_theory.sigma.map_comp_hom_app {I : Type w₁} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₂} {K : Type w₃} (f : K → J) (g : J → I) (X : Σ (i : K), (λ (j : K), (C ∘ g) (f j)) i) :
(category_theory.sigma.map_comp C f g).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 ⋙ category_theory.sigma.map C g) (λ (k : K), category_theory.iso_whisker_right (category_theory.sigma.incl_comp_map (C ∘ g) f k) (category_theory.sigma.map C g) ≪≫ category_theory.sigma.incl_comp_map C g (f k)) X).hom
source
def category_theory.sigma.functor.sigma {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : I → Type u₁} [Π (i : I), category_theory.category (D 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
source
def category_theory.sigma.nat_trans.sigma {I : Type w₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : I → Type u₁} [Π (i : I), category_theory.category (D i)] {F G : Π (i : I), C i ⥤ D i} (α : Π (i : I), F i ⟶ G i) :
category_theory.sigma.functor.sigma F ⟶ category_theory.sigma.functor.sigma G

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

Equations