mathlib3 documentation

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), category_theory.category (C 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), category_theory.category (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_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.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
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_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)
@[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) (i : I) :
def category_theory.pi.comap_id (I : Type w₀) (C : I Type u₁) [Π (i : I), category_theory.category (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), category_theory.category (C i)] (X : Π (i : I), C i) (i : I) :
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)))
@[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)))
@[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) :
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) :
@[protected, 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
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.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
@[simp]
theorem category_theory.pi.iso_app_hom {I : Type w₀} {C : I Type u₁} [Π (i : I), category_theory.category (C i)] {X Y : Π (i : I), C i} (f : X Y) (i : I) :
@[simp]
theorem category_theory.pi.iso_app_inv {I : Type w₀} {C : I Type u₁} [Π (i : I), category_theory.category (C i)] {X Y : Π (i : I), C i} (f : X Y) (i : I) :
def category_theory.pi.iso_app {I : Type w₀} {C : I Type u₁} [Π (i : I), category_theory.category (C 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), category_theory.category (C 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), category_theory.category (C 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), category_theory.category (C 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), category_theory.category (C i)] {D : I Type u₁} [Π (i : I), category_theory.category (D 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), 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)
@[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)
@[simp]
theorem category_theory.functor.pi'_obj {I : Type w₀} {C : I Type u₁} [Π (i : I), category_theory.category (C i)] {A : Type u₁} [category_theory.category A] (f : Π (i : I), A C i) (a : A) (i : I) :
@[simp]
theorem category_theory.functor.pi'_map {I : Type w₀} {C : I Type u₁} [Π (i : I), category_theory.category (C i)] {A : Type u₁} [category_theory.category A] (f : Π (i : I), A C i) (a₁ a₂ : A) (h : a₁ a₂) (i : I) :
def category_theory.functor.pi' {I : Type w₀} {C : I Type u₁} [Π (i : I), category_theory.category (C i)] {A : Type u₁} [category_theory.category A] (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), category_theory.category (C 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), category_theory.category (C i)] {A : Type u₁} [category_theory.category A] (f : Π (i : I), A C i) (i : I) :
theorem category_theory.functor.pi_ext {I : Type w₀} {C : I Type u₁} [Π (i : I), category_theory.category (C i)] {A : Type u₁} [category_theory.category A] (f f' : A Π (i : I), C i) (h : (i : I), f category_theory.pi.eval C i = f' category_theory.pi.eval C i) :
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), 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)
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} (α : Π (i : I), F i G i) :

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

Equations