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).

source
@[protected, 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
source
@[instance, reducible]
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.)

source
@[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)
source
@[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
source
@[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) :
(category_theory.pi.eval C i).obj f = f i
source
@[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) :
(category_theory.pi.eval C i).map α = α i
source
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
source
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
source
@[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)
source
@[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)
source
@[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) :
(category_theory.pi.comap_id I C).inv.app X i = 𝟙 X i
source
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
source
@[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) :
(category_theory.pi.comap_id I C).hom.app X i = 𝟙 X i
source
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) :
category_theory.pi.comap C g ⋙ category_theory.pi.comap (C ∘ g) f ≅ category_theory.pi.comap C (g ∘ f)

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

Equations
source
@[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)))
source
@[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)))
source
@[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) :
(category_theory.pi.comap_eval_iso_eval C h j).inv.app X = 𝟙 (X (h j))
source
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) :
category_theory.pi.comap C h ⋙ category_theory.pi.eval (C ∘ h) j ≅ category_theory.pi.eval C (h j)

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

Equations
source
@[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) :
(category_theory.pi.comap_eval_iso_eval C h j).hom.app X = 𝟙 (X (h j))
source
@[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) :
category_theory.category (sum.elim C D s)
Equations
source
@[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
source
@[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
source
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
source
@[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
source
@[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) :
(category_theory.pi.iso_app f i).hom = f.hom i
source
@[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) :
(category_theory.pi.iso_app f i).inv = f.inv i
source
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
source
@[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) :
category_theory.pi.iso_app (category_theory.iso.refl X) i = category_theory.iso.refl (X i)
source
@[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) :
category_theory.pi.iso_app f.symm i = (category_theory.pi.iso_app f i).symm
source
@[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) :
category_theory.pi.iso_app (f ≪≫ g) i = category_theory.pi.iso_app f i ≪≫ category_theory.pi.iso_app g i
source
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
source
@[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)
source
@[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)
source
@[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) :
(category_theory.functor.pi' f).obj a i = (f i).obj a
source
@[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) :
(category_theory.functor.pi' f).map h i = (f i).map h
source
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
source
@[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) :
category_theory.eq_to_hom h i = category_theory.eq_to_hom _
source
@[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) :
category_theory.functor.pi' f ⋙ category_theory.pi.eval C i = f i
source
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.

source
@[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)
source
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) :
category_theory.functor.pi F ⟶ category_theory.functor.pi G

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

Equations