# mathlib3documentation

category_theory.pi.basic

# Categories of indexed families of objects. #

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

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

@[protected, instance]
def category_theory.pi {I : Type w₀} (C : I Type u₁) [Π (i : I), ] :

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

Equations
@[instance, reducible]
def category_theory.pi' {I : Type v₁} (C : I Type u₁) [Π (i : 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
@[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))
@[protected, 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
@[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.functor.pi'_obj {I : Type w₀} {C : I Type u₁} [Π (i : I), ] {A : Type u₁} (f : Π (i : I), A C i) (a : A) (i : I) :
i = (f i).obj a
@[simp]
theorem category_theory.functor.pi'_map {I : Type w₀} {C : I Type u₁} [Π (i : I), ] {A : Type u₁} (f : Π (i : I), A C i) (a₁ a₂ : A) (h : a₁ a₂) (i : I) :
i = (f i).map h
def category_theory.functor.pi' {I : Type w₀} {C : I Type u₁} [Π (i : I), ] {A : Type u₁} (f : Π (i : I), A C i) :
A Π (i : I), C i

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

Equations
@[simp]
theorem category_theory.functor.eq_to_hom_proj {I : Type w₀} {C : I Type u₁} [Π (i : I), ] {x x' : Π (i : I), C i} (h : x = x') (i : I) :
@[simp]
theorem category_theory.functor.pi'_eval {I : Type w₀} {C : I Type u₁} [Π (i : I), ] {A : Type u₁} (f : Π (i : I), A C i) (i : I) :
theorem category_theory.functor.pi_ext {I : Type w₀} {C : I Type u₁} [Π (i : I), ] {A : Type u₁} (f f' : A Π (i : I), C i) (h : (i : I), = f' ) :
f = f'

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

@[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