# Documentation

Mathlib.CategoryTheory.Pi.Basic

# 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 : IType u₁) [(i : I) → ] :

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

@[inline, reducible]
instance CategoryTheory.pi' {I : Type v₁} (C : IType u₁) [(i : 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.)

@[simp]
theorem CategoryTheory.Pi.id_apply {I : Type w₀} (C : IType u₁) [(i : I) → ] (X : (i : I) → C i) (i : I) :
CategoryTheory.CategoryStruct.id ((i : I) → C i) CategoryTheory.Category.toCategoryStruct X i =
@[simp]
theorem CategoryTheory.Pi.comp_apply {I : Type w₀} (C : IType u₁) [(i : 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 : IType u₁) [(i : 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 : IType u₁) [(i : I) → ] (i : I) (f : (i : I) → C i) :
().obj f = f i
@[simp]
theorem CategoryTheory.Pi.eval_map {I : Type w₀} (C : IType u₁) [(i : I) → ] (i : I) :
∀ {X Y : (i : I) → C i} (α : X Y), ().map α = α i
def CategoryTheory.Pi.eval {I : Type w₀} (C : IType u₁) [(i : 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.

Instances For
instance CategoryTheory.Pi.instForAllCategoryCompType {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (f : JI) (j : J) :
@[simp]
theorem CategoryTheory.Pi.comap_map {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) :
∀ {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 ().toPrefunctor X Y α i = α (h i)
@[simp]
theorem CategoryTheory.Pi.comap_obj {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) (f : (i : I) → C i) (i : J) :
((i : I) → C i).obj CategoryTheory.CategoryStruct.toQuiver ((j : J) → C (h j)) CategoryTheory.CategoryStruct.toQuiver ().toPrefunctor f i = f (h i)
def CategoryTheory.Pi.comap {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) :
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.

Instances For
@[simp]
theorem CategoryTheory.Pi.comapId_inv_app (I : Type w₀) (C : IType u₁) [(i : 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)) () ().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 : IType u₁) [(i : 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)) ().hom X i = CategoryTheory.CategoryStruct.id ((i : I) → C i) CategoryTheory.Category.toCategoryStruct X i
def CategoryTheory.Pi.comapId (I : Type w₀) (C : IType u₁) [(i : I) → ] :
CategoryTheory.Functor.id ((i : I) → C i)

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

Instances For
@[simp]
theorem CategoryTheory.Pi.comapComp_inv_app {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} {K : Type w₂} (f : KJ) (g : JI) (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)) () ().inv X b = CategoryTheory.CategoryStruct.id (X (g (f b)))
@[simp]
theorem CategoryTheory.Pi.comapComp_hom_app {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} {K : Type w₂} (f : KJ) (g : JI) (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)) ().hom X b = CategoryTheory.CategoryStruct.id (X (g (f b)))
def CategoryTheory.Pi.comapComp {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} {K : Type w₂} (f : KJ) (g : JI) :

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

Instances For
@[simp]
theorem CategoryTheory.Pi.comapEvalIsoEval_inv_app {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) (j : J) (X : (i : I) → C i) :
().inv.app X = (CategoryTheory.Iso.refl (().obj X)).inv
@[simp]
theorem CategoryTheory.Pi.comapEvalIsoEval_hom_app {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) (j : J) (X : (i : I) → C i) :
().hom.app X = (CategoryTheory.Iso.refl (().obj X)).hom
def CategoryTheory.Pi.comapEvalIsoEval {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) (j : J) :

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

Instances For
instance CategoryTheory.Pi.sumElimCategory {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₀} {D : JType u₁} [(j : J) → ] (s : I J) :
@[simp]
theorem CategoryTheory.Pi.sum_obj_obj {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₀} {D : JType u₁} [(j : J) → ] (X : (i : I) → C i) (Y : (j : J) → D j) (s : I J) :
(().obj X).obj Y s = match s with | => X i | => Y j
@[simp]
theorem CategoryTheory.Pi.sum_obj_map {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₀} {D : JType u₁} [(j : J) → ] (X : (i : I) → C i) {Y : (j : J) → D j} {Y' : (j : J) → D j} (f : Y Y') (s : I J) :
(().obj X).map f s = match s with | => | => f j
@[simp]
theorem CategoryTheory.Pi.sum_map_app {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₀} {D : JType u₁} [(j : J) → ] {X : (i : I) → C i} {X' : (i : I) → C i} (f : X X') (Y : (j : J) → D j) (s : I J) :
(().map f).app Y s = match s with | => f i | =>
def CategoryTheory.Pi.sum {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₀} {D : JType u₁} [(j : 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.

Instances For
@[simp]
theorem CategoryTheory.Pi.isoApp_hom {I : Type w₀} {C : IType u₁} [(i : I) → ] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X Y) (i : 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 : IType u₁} [(i : I) → ] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X Y) (i : 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 : IType u₁} [(i : 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.

Instances For
@[simp]
theorem CategoryTheory.Pi.isoApp_refl {I : Type w₀} {C : IType u₁} [(i : I) → ] (X : (i : I) → C i) (i : I) :
@[simp]
theorem CategoryTheory.Pi.isoApp_symm {I : Type w₀} {C : IType u₁} [(i : I) → ] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X Y) (i : I) :
CategoryTheory.Pi.isoApp f.symm i = ().symm
@[simp]
theorem CategoryTheory.Pi.isoApp_trans {I : Type w₀} {C : IType u₁} [(i : I) → ] {X : (i : I) → C i} {Y : (i : I) → C i} {Z : (i : I) → C i} (f : X Y) (g : Y Z) (i : I) :
@[simp]
theorem CategoryTheory.Functor.pi_obj {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₁} [(i : 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 ().toPrefunctor f i = (F i).obj (f i)
@[simp]
theorem CategoryTheory.Functor.pi_map {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₁} [(i : 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 ().toPrefunctor X Y α i = (F i).map (α i)
def CategoryTheory.Functor.pi {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 pi types.

Instances For
@[simp]
theorem CategoryTheory.Functor.pi'_map {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u₁} [] (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 ().toPrefunctor X Y h i = (f i).map h
@[simp]
theorem CategoryTheory.Functor.pi'_obj {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u₁} [] (f : (i : I) → CategoryTheory.Functor A (C i)) (a : A) (i : I) :
A.obj CategoryTheory.CategoryStruct.toQuiver ((i : I) → C i) CategoryTheory.CategoryStruct.toQuiver ().toPrefunctor a i = (f i).obj a
def CategoryTheory.Functor.pi' {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u₁} [] (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

Instances For
@[simp]
theorem CategoryTheory.Functor.eqToHom_proj {I : Type w₀} {C : IType u₁} [(i : 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 : IType u₁} [(i : I) → ] {A : Type u₁} [] (f : (i : I) → CategoryTheory.Functor A (C i)) (i : I) :
theorem CategoryTheory.Functor.pi_ext {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u₁} [] (f : CategoryTheory.Functor A ((i : I) → C i)) (f' : CategoryTheory.Functor A ((i : I) → C i)) (h : ∀ (i : 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 : 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) (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) () () () f i = (α i).app (f i)
def CategoryTheory.NatTrans.pi {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.

Instances For