# mathlibdocumentation

category_theory.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]
def category_theory.pi {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] :
category_theory.category (Π (i : I), C i)

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

Equations
@[instance]
def category_theory.pi' {I : Type v₁} (C : I → Type u₁) [Π (i : I), ] :
category_theory.category (Π (i : I), C i)

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

@[simp]
theorem category_theory.pi.id_apply {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] (X : Π (i : I), C i) (i : I) :
𝟙 X i = 𝟙 (X i)
@[simp]
theorem category_theory.pi.comp_apply {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {X Y Z : Π (i : I), C i} (f : X Y) (g : Y Z) (i : I) :
(f g) i = f i g i
@[simp]
theorem category_theory.pi.eval_obj {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] (i : I) (f : Π (i : I), C i) :
.obj f = f i
@[simp]
theorem category_theory.pi.eval_map {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] (i : I) (f g : Π (i : I), C i) (α : f g) :
.map α = α i
def category_theory.pi.eval {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] (i : I) :
(Π (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
def category_theory.pi.comap {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {J : Type w₁} (h : J → I) :
(Π (i : I), C i) Π (j : J), C (h j)

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

Equations
• = {obj := λ (f : Π (i : I), C i) (i : J), f (h i), map := λ (f g : Π (i : I), C i) (α : f g) (i : J), α (h i), map_id' := _, map_comp' := _}
@[simp]
theorem category_theory.pi.comap_obj {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {J : Type w₁} (h : J → I) (f : Π (i : I), C i) (i : J) :
.obj f i = f (h i)
@[simp]
theorem category_theory.pi.comap_map {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {J : Type w₁} (h : J → I) (f g : Π (i : I), C i) (α : f g) (i : J) :
.map α i = α (h i)
@[simp]
theorem category_theory.pi.comap_id_inv_app (I : Type w₀) (C : I → Type u₁) [Π (i : I), ] (X : Π (i : I), C i) (i : I) :
X i = 𝟙 X i
def category_theory.pi.comap_id (I : Type w₀) (C : I → Type u₁) [Π (i : I), ] :
𝟭 (Π (i : I), C i)

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

Equations
@[simp]
theorem category_theory.pi.comap_id_hom_app (I : Type w₀) (C : I → Type u₁) [Π (i : I), ] (X : Π (i : I), C i) (i : I) :
X i = 𝟙 X i
def category_theory.pi.comap_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 natural isomorphism comparing between pulling back along two successive functions, and pulling back along their composition

Equations
@[simp]
theorem category_theory.pi.comap_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 : I), C i) (b : K) :
.hom.app X b = 𝟙 (X (g (f b)))
@[simp]
theorem category_theory.pi.comap_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 : I), C i) (b : K) :
.inv.app X b = 𝟙 (X (g (f b)))
@[simp]
theorem category_theory.pi.comap_eval_iso_eval_inv_app {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {J : Type w₁} (h : J → I) (j : J) (X : Π (i : I), C i) :
X = 𝟙 (X (h j))
def category_theory.pi.comap_eval_iso_eval {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {J : Type w₁} (h : J → I) (j : J) :

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

Equations
@[simp]
theorem category_theory.pi.comap_eval_iso_eval_hom_app {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {J : Type w₁} (h : J → I) (j : J) (X : Π (i : I), C i) :
X = 𝟙 (X (h j))
@[instance]
def category_theory.pi.sum_elim_category {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {J : Type w₀} {D : J → Type u₁} [Π (j : J), ] (s : I J) :
Equations
• = id (_inst_2 j)
• = id (_inst_1 i)
@[simp]
theorem category_theory.pi.sum_map_app {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {J : Type w₀} {D : J → Type u₁} [Π (j : J), ] (f f' : Π (i : I), C i) (α : f f') (g : Π (j : J), D j) (s : I J) :
α).app g s = sum.rec α (λ (j : J), 𝟙 (g j)) s
@[simp]
theorem category_theory.pi.sum_obj_map {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {J : Type w₀} {D : J → Type u₁} [Π (j : J), ] (f : Π (i : I), C i) (g g' : Π (j : J), D j) (α : g g') (s : I J) :
f).map α s = sum.rec (λ (i : I), 𝟙 (f i)) α s
def category_theory.pi.sum {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {J : Type w₀} {D : J → Type u₁} [Π (j : J), ] :
(Π (i : I), C i) (Π (j : J), D j) Π (s : I J), 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
@[simp]
theorem category_theory.pi.sum_obj_obj {I : Type w₀} (C : I → Type u₁) [Π (i : I), ] {J : Type w₀} {D : J → Type u₁} [Π (j : J), ] (f : Π (i : I), C i) (g : Π (j : J), D j) (s : I J) :
f).obj g s = sum.rec f g s
@[simp]
theorem category_theory.pi.iso_app_hom {I : Type w₀} {C : I → Type u₁} [Π (i : I), ] {X Y : Π (i : I), C i} (f : X Y) (i : I) :
= f.hom i
@[simp]
theorem category_theory.pi.iso_app_inv {I : Type w₀} {C : I → Type u₁} [Π (i : I), ] {X Y : Π (i : I), C i} (f : X Y) (i : I) :
= f.inv i
def category_theory.pi.iso_app {I : Type w₀} {C : I → Type u₁} [Π (i : I), ] {X 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
@[simp]
theorem category_theory.pi.iso_app_refl {I : Type w₀} {C : I → Type u₁} [Π (i : I), ] (X : Π (i : I), C i) (i : I) :
@[simp]
theorem category_theory.pi.iso_app_symm {I : Type w₀} {C : I → Type u₁} [Π (i : I), ] {X Y : Π (i : I), C i} (f : X Y) (i : I) :
@[simp]
theorem category_theory.pi.iso_app_trans {I : Type w₀} {C : I → Type u₁} [Π (i : I), ] {X Y Z : Π (i : I), C i} (f : X Y) (g : Y Z) (i : I) :
def category_theory.functor.pi {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 pi types.

Equations
• = {obj := λ (f : Π (i : I), C i) (i : I), (F i).obj (f i), map := λ (f g : Π (i : I), C i) (α : f g) (i : I), (F i).map (α i), map_id' := _, map_comp' := _}
@[simp]
theorem category_theory.functor.pi_map {I : Type w₀} {C : I → Type u₁} [Π (i : I), ] {D : I → Type u₁} [Π (i : I), ] (F : Π (i : I), C i D i) (f g : Π (i : I), C i) (α : f g) (i : I) :
i = (F i).map (α i)
@[simp]
theorem category_theory.functor.pi_obj {I : Type w₀} {C : I → Type u₁} [Π (i : I), ] {D : I → Type u₁} [Π (i : I), ] (F : Π (i : I), C i D i) (f : Π (i : I), C i) (i : I) :
i = (F i).obj (f i)
@[simp]
theorem category_theory.nat_trans.pi_app {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) (f : Π (i : I), C i) (i : I) :
i = (α i).app (f i)
def category_theory.nat_trans.pi {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