Categories of indexed families of objects.

We define the pointwise category structure on indexed families of objects in a category (and also the dependent generalization).

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

pi C gives the cartesian product of an indexed family of categories.

Equations

• CategoryTheory.pi C = CategoryTheory.Category.mk

@[inline, reducible]

instance CategoryTheory.pi' {I : Type v₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] : CategoryTheory.Category.{v₁, max u₁ v₁} ((i : I) → C i)

This provides some assistance to typeclass search in a common situation, which otherwise fails. (Without this CategoryTheory.Pi.has_limit_of_has_limit_comp_eval fails.)

Equations

• CategoryTheory.pi' C = CategoryTheory.pi C

@[simp]

theorem CategoryTheory.Pi.id_apply {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) : CategoryTheory.CategoryStruct.id ((i : I) → C i) CategoryTheory.Category.toCategoryStruct X i = CategoryTheory.CategoryStruct.id (X i)

@[simp]

theorem CategoryTheory.Pi.comp_apply {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) → C i} {Y : (i : I) → C i} {Z : (i : I) → C i} (f : X ⟶ Y) (g : Y ⟶ Z) (i : I) : CategoryTheory.CategoryStruct.comp ((i : I) → C i) CategoryTheory.Category.toCategoryStruct X Y (fun i => Z i) f g i = CategoryTheory.CategoryStruct.comp (f i) (g i)

theorem CategoryTheory.Pi.ext {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) → C i} {Y : (i : I) → C i} {f : X ⟶ Y} {g : X ⟶ Y} (w : ∀ (i : I), f i = g i) : f = g

@[simp]

theorem CategoryTheory.Pi.eval_obj {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I) (f : (i : I) → C i) : (CategoryTheory.Pi.eval C i).obj f = f i

@[simp]

theorem CategoryTheory.Pi.eval_map {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I) : ∀ {X Y : (i : I) → C i} (α : X ⟶ Y), (CategoryTheory.Pi.eval C i).map α = α i

def CategoryTheory.Pi.eval {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I) : CategoryTheory.Functor ((i : I) → C i) (C i)

The evaluation functor at i : I, sending an I-indexed family of objects to the object over i.

Equations

• CategoryTheory.Pi.eval C i = CategoryTheory.Functor.mk { obj := fun f => f i, map := fun {X Y} α => α i }

instance CategoryTheory.Pi.instForAllCategoryCompType {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (f : J → I) (j : J) : CategoryTheory.Category.{v₁, u₁} ((C ∘ f) j)

Equations

• CategoryTheory.Pi.instForAllCategoryCompType C f = id inferInstance

@[simp]

theorem CategoryTheory.Pi.comap_map {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) : ∀ {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J), ((i : I) → C i).map CategoryTheory.CategoryStruct.toQuiver ((j : J) → C (h j)) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Pi.comap C h).toPrefunctor X Y α i = α (h i)

@[simp]

theorem CategoryTheory.Pi.comap_obj {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) (f : (i : I) → C i) (i : J) : ((i : I) → C i).obj CategoryTheory.CategoryStruct.toQuiver ((j : J) → C (h j)) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Pi.comap C h).toPrefunctor f i = f (h i)

def CategoryTheory.Pi.comap {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) : CategoryTheory.Functor ((i : I) → C i) ((j : J) → C (h j))

Pull back an I-indexed family of objects to a J-indexed family, along a function J → I.

Equations

• CategoryTheory.Pi.comap C h = CategoryTheory.Functor.mk { obj := fun f i => f (h i), map := fun {X Y} α i => α (h i) }

@[simp]

theorem CategoryTheory.Pi.comapId_inv_app (I : Type w₀) (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) : ((i : I) → C i).app (CategoryTheory.pi fun i => C i) ((j : I) → C (id j)) (CategoryTheory.pi fun j => C (id j)) (CategoryTheory.Functor.id ((i : I) → C i)) (CategoryTheory.Pi.comap C id) (CategoryTheory.Pi.comapId I C).inv X i = CategoryTheory.CategoryStruct.id ((i : I) → C i) CategoryTheory.Category.toCategoryStruct X i

@[simp]

theorem CategoryTheory.Pi.comapId_hom_app (I : Type w₀) (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) : ((i : I) → C i).app (CategoryTheory.pi fun i => C i) ((j : I) → C (id j)) (CategoryTheory.pi fun j => C (id j)) (CategoryTheory.Pi.comap C id) (CategoryTheory.Functor.id ((i : I) → C i)) (CategoryTheory.Pi.comapId I C).hom X i = CategoryTheory.CategoryStruct.id ((i : I) → C i) CategoryTheory.Category.toCategoryStruct X i

def CategoryTheory.Pi.comapId (I : Type w₀) (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] : CategoryTheory.Pi.comap C id ≅ CategoryTheory.Functor.id ((i : I) → C i)

The natural isomorphism between pulling back a grading along the identity function, and the identity functor.

Equations

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

@[simp]

theorem CategoryTheory.Pi.comapComp_inv_app {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} {K : Type w₂} (f : K → J) (g : J → I) (X : (i : I) → C i) (b : K) : ((i : I) → C i).app (CategoryTheory.pi fun i => C i) ((j : K) → (C ∘ g) (f j)) (CategoryTheory.pi fun j => (C ∘ g) (f j)) (CategoryTheory.Pi.comap C (g ∘ f)) (CategoryTheory.Functor.comp (CategoryTheory.Pi.comap C g) (CategoryTheory.Pi.comap (C ∘ g) f)) (CategoryTheory.Pi.comapComp C f g).inv X b = CategoryTheory.CategoryStruct.id (X (g (f b)))

@[simp]

theorem CategoryTheory.Pi.comapComp_hom_app {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} {K : Type w₂} (f : K → J) (g : J → I) (X : (i : I) → C i) (b : K) : ((i : I) → C i).app (CategoryTheory.pi fun i => C i) ((j : K) → (C ∘ g) (f j)) (CategoryTheory.pi fun j => (C ∘ g) (f j)) (CategoryTheory.Functor.comp (CategoryTheory.Pi.comap C g) (CategoryTheory.Pi.comap (C ∘ g) f)) (CategoryTheory.Pi.comap C (g ∘ f)) (CategoryTheory.Pi.comapComp C f g).hom X b = CategoryTheory.CategoryStruct.id (X (g (f b)))

def CategoryTheory.Pi.comapComp {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} {K : Type w₂} (f : K → J) (g : J → I) : CategoryTheory.Functor.comp (CategoryTheory.Pi.comap C g) (CategoryTheory.Pi.comap (C ∘ g) f) ≅ CategoryTheory.Pi.comap C (g ∘ f)

The natural isomorphism comparing between pulling back along two successive functions, and pulling back along their composition

Equations

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

@[simp]

theorem CategoryTheory.Pi.comapEvalIsoEval_inv_app {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) (j : J) (X : (i : I) → C i) : (CategoryTheory.Pi.comapEvalIsoEval C h j).inv.app X = (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Pi.comap C h) (CategoryTheory.Pi.eval (C ∘ h) j)).obj X)).inv

@[simp]

theorem CategoryTheory.Pi.comapEvalIsoEval_hom_app {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) (j : J) (X : (i : I) → C i) : (CategoryTheory.Pi.comapEvalIsoEval C h j).hom.app X = (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Pi.comap C h) (CategoryTheory.Pi.eval (C ∘ h) j)).obj X)).hom

def CategoryTheory.Pi.comapEvalIsoEval {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) (j : J) : CategoryTheory.Functor.comp (CategoryTheory.Pi.comap C h) (CategoryTheory.Pi.eval (C ∘ h) j) ≅ CategoryTheory.Pi.eval C (h j)

The natural isomorphism between pulling back then evaluating, and just evaluating.

Equations

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

instance CategoryTheory.Pi.sumElimCategory {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (s : I ⊕ J) : CategoryTheory.Category.{v₁, u₁} (Sum.elim C D s)

Equations

• CategoryTheory.Pi.sumElimCategory C x = match x with | Sum.inl i => id inferInstance | Sum.inr j => id inferInstance

@[simp]

theorem CategoryTheory.Pi.sum_obj_obj {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (X : (i : I) → C i) (Y : (j : J) → D j) (s : I ⊕ J) : ((CategoryTheory.Pi.sum C).obj X).obj Y s = match s with | Sum.inl i => X i | Sum.inr j => Y j

@[simp]

theorem CategoryTheory.Pi.sum_obj_map {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (X : (i : I) → C i) {Y : (j : J) → D j} {Y' : (j : J) → D j} (f : Y ⟶ Y') (s : I ⊕ J) : ((CategoryTheory.Pi.sum C).obj X).map f s = match s with | Sum.inl i => CategoryTheory.CategoryStruct.id (X i) | Sum.inr j => f j

@[simp]

theorem CategoryTheory.Pi.sum_map_app {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] {X : (i : I) → C i} {X' : (i : I) → C i} (f : X ⟶ X') (Y : (j : J) → D j) (s : I ⊕ J) : ((CategoryTheory.Pi.sum C).map f).app Y s = match s with | Sum.inl i => f i | Sum.inr j => CategoryTheory.CategoryStruct.id (Y j)

def CategoryTheory.Pi.sum {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] : CategoryTheory.Functor ((i : I) → C i) (CategoryTheory.Functor ((j : J) → D j) ((s : I ⊕ J) → Sum.elim C D s))

The bifunctor combining an I-indexed family of objects with a J-indexed family of objects to obtain an I ⊕ J-indexed family of objects.

Equations

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

@[simp]

theorem CategoryTheory.Pi.isoApp_hom {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X ≅ Y) (i : I) : (CategoryTheory.Pi.isoApp f i).hom = ((i : I) → C i).hom (CategoryTheory.pi fun i => C i) X Y f i

@[simp]

theorem CategoryTheory.Pi.isoApp_inv {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X ≅ Y) (i : I) : (CategoryTheory.Pi.isoApp f i).inv = ((i : I) → C i).inv (CategoryTheory.pi fun i => C i) X Y f i

def CategoryTheory.Pi.isoApp {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X ≅ Y) (i : I) : X i ≅ Y i

An isomorphism between I-indexed objects gives an isomorphism between each pair of corresponding components.

Equations

• CategoryTheory.Pi.isoApp f i = CategoryTheory.Iso.mk (((i : I) → C i).hom (CategoryTheory.pi fun i => C i) X Y f i) (((i : I) → C i).inv (CategoryTheory.pi fun i => C i) X Y f i)

@[simp]

theorem CategoryTheory.Pi.isoApp_refl {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) : CategoryTheory.Pi.isoApp (CategoryTheory.Iso.refl X) i = CategoryTheory.Iso.refl (X i)

@[simp]

theorem CategoryTheory.Pi.isoApp_symm {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X ≅ Y) (i : I) : CategoryTheory.Pi.isoApp f.symm i = (CategoryTheory.Pi.isoApp f i).symm

@[simp]

theorem CategoryTheory.Pi.isoApp_trans {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) → C i} {Y : (i : I) → C i} {Z : (i : I) → C i} (f : X ≅ Y) (g : Y ≅ Z) (i : I) : CategoryTheory.Pi.isoApp (f ≪≫ g) i = CategoryTheory.Pi.isoApp f i ≪≫ CategoryTheory.Pi.isoApp g i

@[simp]

theorem CategoryTheory.Functor.pi_obj {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (D i)] (F : (i : I) → CategoryTheory.Functor (C i) (D i)) (f : (i : I) → C i) (i : I) : ((i : I) → C i).obj CategoryTheory.CategoryStruct.toQuiver ((i : I) → D i) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Functor.pi F).toPrefunctor f i = (F i).obj (f i)

@[simp]

theorem CategoryTheory.Functor.pi_map {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (D i)] (F : (i : I) → CategoryTheory.Functor (C i) (D i)) : ∀ {X Y : (i : I) → C i} (α : X ⟶ Y) (i : I), ((i : I) → C i).map CategoryTheory.CategoryStruct.toQuiver ((i : I) → D i) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Functor.pi F).toPrefunctor X Y α i = (F i).map (α i)

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

Equations

• CategoryTheory.Functor.pi F = CategoryTheory.Functor.mk { obj := fun f i => (F i).obj (f i), map := fun {X Y} α i => (F i).map (α i) }

@[simp]

theorem CategoryTheory.Functor.pi'_map {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₁} [CategoryTheory.Category.{u₁, u₁} A] (f : (i : I) → CategoryTheory.Functor A (C i)) : ∀ {X Y : A} (h : X ⟶ Y) (i : I), A.map CategoryTheory.CategoryStruct.toQuiver ((i : I) → C i) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Functor.pi' f).toPrefunctor X Y h i = (f i).map h

@[simp]

theorem CategoryTheory.Functor.pi'_obj {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₁} [CategoryTheory.Category.{u₁, u₁} A] (f : (i : I) → CategoryTheory.Functor A (C i)) (a : A) (i : I) : A.obj CategoryTheory.CategoryStruct.toQuiver ((i : I) → C i) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Functor.pi' f).toPrefunctor a i = (f i).obj a

def CategoryTheory.Functor.pi' {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₁} [CategoryTheory.Category.{u₁, u₁} A] (f : (i : I) → CategoryTheory.Functor A (C i)) : CategoryTheory.Functor A ((i : I) → C i)

Similar to pi, but all functors come from the same category A

Equations

• CategoryTheory.Functor.pi' f = CategoryTheory.Functor.mk { obj := fun a i => (f i).obj a, map := fun {X Y} h i => (f i).map h }

@[simp]

theorem CategoryTheory.Functor.eqToHom_proj {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {x : (i : I) → C i} {x' : (i : I) → C i} (h : x = x') (i : I) : CategoryTheory.eqToHom ((i : I) → C i) (CategoryTheory.pi fun i => C i) x x' h i = CategoryTheory.eqToHom (_ : x i = x' i)

@[simp]

theorem CategoryTheory.Functor.pi'_eval {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₁} [CategoryTheory.Category.{u₁, u₁} A] (f : (i : I) → CategoryTheory.Functor A (C i)) (i : I) : CategoryTheory.Functor.comp (CategoryTheory.Functor.pi' f) (CategoryTheory.Pi.eval C i) = f i

theorem CategoryTheory.Functor.pi_ext {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₁} [CategoryTheory.Category.{u₁, u₁} A] (f : CategoryTheory.Functor A ((i : I) → C i)) (f' : CategoryTheory.Functor A ((i : I) → C i)) (h : ∀ (i : I), CategoryTheory.Functor.comp f (CategoryTheory.Pi.eval C i) = CategoryTheory.Functor.comp f' (CategoryTheory.Pi.eval C i)) : f = f'

Two functors to a product category are equal iff they agree on every coordinate.

@[simp]

theorem CategoryTheory.NatTrans.pi_app {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (D 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) (f : (i : I) → C i) (i : I) : ((i : I) → C i).app (CategoryTheory.pi fun i => C i) ((i : I) → D i) (CategoryTheory.pi fun i => D i) (CategoryTheory.Functor.pi F) (CategoryTheory.Functor.pi G) (CategoryTheory.NatTrans.pi α) f i = (α i).app (f i)

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

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

Equations

• CategoryTheory.NatTrans.pi α = CategoryTheory.NatTrans.mk fun f i => (α i).app (f i)