mathlib documentation

category_theory.​pi.​basic

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

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

@[simp]
theorem category_theory.​pi.​comap_obj {I : Type w₀} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₁} (h : J → I) (f : Π (i : I), C i) (i : J) :
(category_theory.pi.comap C h).obj f i = f (h i)

def category_theory.​pi.​comap {I : Type w₀} (C : I → Type u₁) [Π (i : I), category_theory.category (C 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_map {I : Type w₀} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₁} (h : J → I) (f g : Π (i : I), C i) (α : f g) (i : J) :
(category_theory.pi.comap C h).map α i = α (h i)

@[simp]
theorem category_theory.​pi.​comap_id_inv_app (I : Type w₀) (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] (X : Π (i : I), C i) :

@[simp]
theorem category_theory.​pi.​comap_id_hom_app (I : Type w₀) (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] (X : Π (i : I), C i) :

def category_theory.​pi.​comap_id (I : Type w₀) (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] :
category_theory.pi.comap C id 𝟭 (Π (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_comp_inv_app {I : Type w₀} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₁} {K : Type w₂} (f : K → J) (g : J → I) (X : Π (i : I), C i) (b : K) :
(category_theory.pi.comap_comp C f g).inv.app X b = 𝟙 (X (g (f b)))

def category_theory.​pi.​comap_comp {I : Type w₀} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₁} {K : Type w₂} (f : K → J) (g : J → I) :

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), category_theory.category (C i)] {J : Type w₁} {K : Type w₂} (f : K → J) (g : J → I) (X : Π (i : I), C i) (b : K) :
(category_theory.pi.comap_comp C f g).hom.app X b = 𝟙 (X (g (f b)))

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

@[simp]
theorem category_theory.​pi.​comap_eval_iso_eval_inv_app {I : Type w₀} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₁} (h : J → I) (j : J) (X : Π (i : I), C i) :

@[instance]
def category_theory.​pi.​sum_elim_category {I : Type w₀} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₀} {D : J → Type u₁} [Π (j : J), category_theory.category (D j)] (s : I J) :

Equations
@[simp]
theorem category_theory.​pi.​sum_map_app {I : Type w₀} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₀} {D : J → Type u₁} [Π (j : J), category_theory.category (D j)] (f f' : Π (i : I), C i) (α : f f') (g : Π (j : J), D j) (s : I J) :
((category_theory.pi.sum C).map α).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), category_theory.category (C i)] {J : Type w₀} {D : J → Type u₁} [Π (j : J), category_theory.category (D j)] (f : Π (i : I), C i) (g g' : Π (j : J), D j) (α : g g') (s : I J) :
((category_theory.pi.sum C).obj f).map α s = sum.rec (λ (i : I), 𝟙 (f i)) α s

@[simp]
theorem category_theory.​pi.​sum_obj_obj {I : Type w₀} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₀} {D : J → Type u₁} [Π (j : J), category_theory.category (D j)] (f : Π (i : I), C i) (g : Π (j : J), D j) (s : I J) :
((category_theory.pi.sum C).obj f).obj g s = sum.rec f g s

def category_theory.​pi.​sum {I : Type w₀} (C : I → Type u₁) [Π (i : I), category_theory.category (C i)] {J : Type w₀} {D : J → Type u₁} [Π (j : J), category_theory.category (D j)] :
(Π (i : I), C i) (Π (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
@[simp]
theorem category_theory.​functor.​pi_map {I : Type w₀} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : I → Type u₁} [Π (i : I), category_theory.category (D i)] (F : Π (i : I), C i D i) (f g : Π (i : I), C i) (α : f g) (i : I) :
(category_theory.functor.pi F).map α i = (F i).map (α i)

def category_theory.​functor.​pi {I : Type w₀} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : I → Type u₁} [Π (i : I), category_theory.category (D i)] :
(Π (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_obj {I : Type w₀} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : I → Type u₁} [Π (i : I), category_theory.category (D i)] (F : Π (i : I), C i D i) (f : Π (i : I), C i) (i : I) :
(category_theory.functor.pi F).obj f i = (F i).obj (f i)

def category_theory.​nat_trans.​pi {I : Type w₀} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : I → Type u₁} [Π (i : I), category_theory.category (D i)] {F G : Π (i : I), C i D i} :

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

Equations
@[simp]
theorem category_theory.​nat_trans.​pi_app {I : Type w₀} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {D : I → Type u₁} [Π (i : I), category_theory.category (D i)] {F G : Π (i : I), C i D i} (α : Π (i : I), F i G i) (f : Π (i : I), C i) (i : I) :
(category_theory.nat_trans.pi α).app f i = (α i).app (f i)