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 : I → Type u₁} [(i : I) → Category.{v₁, u₁} (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.

• mk {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {i : I} {X Y : C i} : (X ⟶ Y) → SigmaHom ⟨i, X⟩ ⟨i, Y⟩

def CategoryTheory.Sigma.SigmaHom.id {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] (X : (i : I) × C i) : SigmaHom X X

The identity morphism on an object.

Equations

• CategoryTheory.Sigma.SigmaHom.id ⟨fst, snd⟩ = CategoryTheory.Sigma.SigmaHom.mk (CategoryTheory.CategoryStruct.id snd)

instance CategoryTheory.Sigma.SigmaHom.instInhabited {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] (X : (i : I) × C i) : Inhabited (SigmaHom X X)

Equations

• CategoryTheory.Sigma.SigmaHom.instInhabited X = { default := CategoryTheory.Sigma.SigmaHom.id X }

def CategoryTheory.Sigma.SigmaHom.comp {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {X Y Z : (i : I) × C i} : SigmaHom X Y → SigmaHom Y Z → SigmaHom X Z

Composition of sigma homomorphisms.

Equations

• (CategoryTheory.Sigma.SigmaHom.mk f).comp (CategoryTheory.Sigma.SigmaHom.mk g) = CategoryTheory.Sigma.SigmaHom.mk (CategoryTheory.CategoryStruct.comp f g)

instance CategoryTheory.Sigma.SigmaHom.instCategoryStructSigma {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] : CategoryStruct.{max (max u₁ w₁) v₁, max u₁ w₁} ((i : I) × C 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 : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] (i : I) (X Y Z : C i) (f : X ⟶ Y) (g : Y ⟶ Z) : (mk f).comp (mk g) = mk (CategoryStruct.comp f g)

theorem CategoryTheory.Sigma.SigmaHom.assoc {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {X Y Z W : (i : I) × C i} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) : CategoryStruct.comp (CategoryStruct.comp f g) h = CategoryStruct.comp f (CategoryStruct.comp g h)

theorem CategoryTheory.Sigma.SigmaHom.id_comp {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {X Y : (i : I) × C i} (f : X ⟶ Y) : CategoryStruct.comp (CategoryStruct.id X) f = f

theorem CategoryTheory.Sigma.SigmaHom.comp_id {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {X Y : (i : I) × C i} (f : X ⟶ Y) : CategoryStruct.comp f (CategoryStruct.id Y) = f

instance CategoryTheory.Sigma.sigma {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] : Category.{max (max u₁ v₁) w₁, max u₁ w₁} ((i : I) × C i)

Equations

• CategoryTheory.Sigma.sigma = { toCategoryStruct := CategoryTheory.Sigma.SigmaHom.instCategoryStructSigma, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

def CategoryTheory.Sigma.incl {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] (i : I) : Functor (C i) ((i : I) × C i)

The inclusion functor into the disjoint union of categories.

Equations

• CategoryTheory.Sigma.incl i = { obj := fun (X : C i) => ⟨i, X⟩, map := fun {X Y : C i} => CategoryTheory.Sigma.SigmaHom.mk, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Sigma.incl_map {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] (i : I) {X✝ Y✝ : C i} (a✝ : X✝ ⟶ Y✝) : (incl i).map a✝ = SigmaHom.mk a✝

@[simp]

theorem CategoryTheory.Sigma.incl_obj {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {i : I} (X : C i) : (incl i).obj X = ⟨i, X⟩

instance CategoryTheory.Sigma.instFullSigmaIncl {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] (i : I) : (incl i).Full

instance CategoryTheory.Sigma.instFaithfulSigmaIncl {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] (i : I) : (incl i).Faithful

def CategoryTheory.Sigma.natTrans {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor ((i : I) × C i) D} (h : (i : I) → (incl i).comp F ⟶ (incl i).comp G) : F ⟶ G

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

Equations

• CategoryTheory.Sigma.natTrans h = { app := fun (x : (i : I) × C i) => match x with | ⟨j, X⟩ => (h j).app X, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Sigma.natTrans_app {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor ((i : I) × C i) D} (h : (i : I) → (incl i).comp F ⟶ (incl i).comp G) (i : I) (X : C i) : (natTrans h).app ⟨i, X⟩ = (h i).app X

def CategoryTheory.Sigma.descMap {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] (F : (i : I) → Functor (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

• CategoryTheory.Sigma.descMap F ⟨i, X⟩ ⟨i, Y⟩ (CategoryTheory.Sigma.SigmaHom.mk g) = (F ⟨i, X⟩.fst).map g

def CategoryTheory.Sigma.desc {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] (F : (i : I) → Functor (C i) D) : 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.

@[simp]

theorem CategoryTheory.Sigma.desc_obj {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] (F : (i : I) → Functor (C i) D) (X : (i : I) × C i) : (desc F).obj X = (F X.fst).obj X.snd

@[simp]

theorem CategoryTheory.Sigma.desc_map_mk {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] (F : (i : I) → Functor (C i) D) {i : I} (X Y : C i) (f : X ⟶ Y) : (desc F).map (SigmaHom.mk f) = (F i).map f

def CategoryTheory.Sigma.inclDesc {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] (F : (i : I) → Functor (C i) D) (i : I) : (incl i).comp (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

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

@[simp]

theorem CategoryTheory.Sigma.inclDesc_hom_app {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] (F : (i : I) → Functor (C i) D) (i : I) (X : C i) : (inclDesc F i).hom.app X = CategoryStruct.id ((F i).obj X)

@[simp]

theorem CategoryTheory.Sigma.inclDesc_inv_app {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] (F : (i : I) → Functor (C i) D) (i : I) (X : C i) : (inclDesc F i).inv.app X = CategoryStruct.id ((F i).obj X)

def CategoryTheory.Sigma.descUniq {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] (F : (i : I) → Functor (C i) D) (q : Functor ((i : I) × C i) D) (h : (i : I) → (incl i).comp q ≅ F i) : q ≅ desc F

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

Equations

• CategoryTheory.Sigma.descUniq F q h = CategoryTheory.NatIso.ofComponents (fun (x : (i : I) × C i) => match x with | ⟨i, X⟩ => (h i).app X) ⋯

@[simp]

theorem CategoryTheory.Sigma.descUniq_hom_app {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] (F : (i : I) → Functor (C i) D) (q : Functor ((i : I) × C i) D) (h : (i : I) → (incl i).comp q ≅ F i) (i : I) (X : C i) : (descUniq F q h).hom.app ⟨i, X⟩ = (h i).hom.app X

@[simp]

theorem CategoryTheory.Sigma.descUniq_inv_app {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] (F : (i : I) → Functor (C i) D) (q : Functor ((i : I) × C i) D) (h : (i : I) → (incl i).comp q ≅ F i) (i : I) (X : C i) : (descUniq F q h).inv.app ⟨i, X⟩ = (h i).inv.app X

def CategoryTheory.Sigma.natIso {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] {q₁ q₂ : Functor ((i : I) × C i) D} (h : (i : I) → (incl i).comp q₁ ≅ (incl i).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.

@[simp]

theorem CategoryTheory.Sigma.natIso_hom {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] {q₁ q₂ : Functor ((i : I) × C i) D} (h : (i : I) → (incl i).comp q₁ ≅ (incl i).comp q₂) : (natIso h).hom = natTrans fun (i : I) => (h i).hom

@[simp]

theorem CategoryTheory.Sigma.natIso_inv {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : Type u₂} [Category.{v₂, u₂} D] {q₁ q₂ : Functor ((i : I) × C i) D} (h : (i : I) → (incl i).comp q₁ ≅ (incl i).comp q₂) : (natIso h).inv = natTrans fun (i : I) => (h i).inv

def CategoryTheory.Sigma.map {I : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₂} (g : J → I) : 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

• CategoryTheory.Sigma.map C g = CategoryTheory.Sigma.desc fun (j : J) => CategoryTheory.Sigma.incl (g j)

@[simp]

theorem CategoryTheory.Sigma.map_obj {I : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₂} (g : J → I) (j : J) (X : C (g j)) : (map C g).obj ⟨j, X⟩ = ⟨g j, X⟩

@[simp]

theorem CategoryTheory.Sigma.map_map {I : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₂} (g : J → I) {j : J} {X Y : C (g j)} (f : X ⟶ Y) : (map C g).map (SigmaHom.mk f) = SigmaHom.mk f

def CategoryTheory.Sigma.inclCompMap {I : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₂} (g : J → I) (j : J) : (incl j).comp (map C g) ≅ incl (g j)

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

Equations

• CategoryTheory.Sigma.inclCompMap C g j = CategoryTheory.Iso.refl ((CategoryTheory.Sigma.incl j).comp (CategoryTheory.Sigma.map C g))

@[simp]

theorem CategoryTheory.Sigma.inclCompMap_inv_app {I : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₂} (g : J → I) (j : J) (X : C (g j)) : (inclCompMap C g j).inv.app X = CategoryStruct.id ⟨g j, X⟩

@[simp]

theorem CategoryTheory.Sigma.inclCompMap_hom_app {I : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₂} (g : J → I) (j : J) (X : C (g j)) : (inclCompMap C g j).hom.app X = CategoryStruct.id ⟨g j, X⟩

def CategoryTheory.Sigma.mapId (I : Type w₁) (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] : map C id ≅ 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.

@[simp]

theorem CategoryTheory.Sigma.mapId_inv_app (I : Type w₁) (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (x✝ : (i : I) × (fun (i : I) => C (id i)) i) : (mapId I C).inv.app x✝ = CategoryStruct.id ⟨x✝.fst, x✝.snd⟩

@[simp]

theorem CategoryTheory.Sigma.mapId_hom_app (I : Type w₁) (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (x✝ : (i : I) × (fun (i : I) => C (id i)) i) : (mapId I C).hom.app x✝ = CategoryStruct.id ⟨x✝.fst, x✝.snd⟩

def CategoryTheory.Sigma.mapComp {I : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₂} {K : Type w₃} (f : K → J) (g : J → I) : (map (fun (x : J) => C (g x)) f).comp (map C g) ≅ 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.

@[simp]

theorem CategoryTheory.Sigma.mapComp_inv_app {I : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₂} {K : Type w₃} (f : K → J) (g : J → I) (X : (i : K) × (fun (i : K) => C (g (f i))) i) : (mapComp C f g).inv.app X = CategoryStruct.id ⟨g (f X.fst), X.snd⟩

@[simp]

theorem CategoryTheory.Sigma.mapComp_hom_app {I : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₂} {K : Type w₃} (f : K → J) (g : J → I) (X : (i : K) × (fun (i : K) => C (g (f i))) i) : (mapComp C f g).hom.app X = CategoryStruct.id ⟨g (f X.fst), X.snd⟩

def CategoryTheory.Sigma.Functor.sigma {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₁} [(i : I) → Category.{v₁, u₁} (D i)] (F : (i : I) → Functor (C i) (D i)) : Functor ((i : I) × C i) ((i : I) × D i)

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

Equations

• CategoryTheory.Sigma.Functor.sigma F = CategoryTheory.Sigma.desc fun (i : I) => (F i).comp (CategoryTheory.Sigma.incl i)

def CategoryTheory.Sigma.natTrans.sigma {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₁} [(i : I) → Category.{v₁, u₁} (D i)] {F G : (i : I) → Functor (C i) (D i)} (α : (i : I) → F i ⟶ G i) : Functor.sigma F ⟶ Functor.sigma G

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

Equations

• CategoryTheory.Sigma.natTrans.sigma α = { app := fun (f : (i : I) × C i) => CategoryTheory.Sigma.SigmaHom.mk ((α f.fst).app f.snd), naturality := ⋯ }