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.
@[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) :
@[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) :
@[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
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.
@[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
@[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.
@[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) :
(category_theory.pi.comap_id I C).inv.app X = 𝟙 X
@[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) :
(category_theory.pi.comap_id I C).hom.app X = 𝟙 X
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
- category_theory.pi.comap_id I C = {hom := {app := λ (X : Π (i : I), C i), 𝟙 X, naturality' := _}, inv := {app := λ (X : Π (i : I), C i), 𝟙 X, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[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) :
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
- category_theory.pi.comap_comp C f g = {hom := {app := λ (X : Π (i : I), C i) (b : K), 𝟙 (X (g (f b))), naturality' := _}, inv := {app := λ (X : Π (i : I), C i) (b : K), 𝟙 (X (g (f b))), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[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) :
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
- category_theory.pi.comap_eval_iso_eval C h j = category_theory.nat_iso.of_components (λ (f : Π (i : I), C i), category_theory.iso.refl ((category_theory.pi.comap C h ⋙ category_theory.pi.eval (C ∘ h) j).obj f)) _
@[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 = ((λ (f : Π (i : I), C i), category_theory.iso.refl ((category_theory.pi.comap C h ⋙ category_theory.pi.eval (C ∘ h) j).obj f)) X).hom
@[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 = category_theory.is_iso.inv ({app := λ (X : Π (i : I), C i), ((λ (f : Π (i : I), C i), category_theory.iso.refl ((category_theory.pi.comap C h ⋙ category_theory.pi.eval (C ∘ h) j).obj f)) X).hom, naturality' := _}.app X)
@[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
- category_theory.pi.sum_elim_category C (sum.inr j) = id (_inst_2 j)
- category_theory.pi.sum_elim_category C (sum.inl i) = id (_inst_1 i)
@[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)] :
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
- category_theory.pi.sum C = {obj := λ (f : Π (i : I), C i), {obj := λ (g : Π (j : J), D j) (s : I ⊕ J), sum.rec f g s, map := λ (g g' : Π (j : J), D j) (α : g ⟶ g') (s : I ⊕ J), sum.rec (λ (i : I), 𝟙 (f i)) α s, map_id' := _, map_comp' := _}, map := λ (f f' : Π (i : I), C i) (α : f ⟶ f'), {app := λ (g : Π (j : J), D j) (s : I ⊕ J), sum.rec α (λ (j : J), 𝟙 (g j)) s, naturality' := _}, map_id' := _, map_comp' := _}
@[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)] :
Assemble an I-indexed family of functors into a functor between the pi types.
@[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} :
(Π (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
- category_theory.nat_trans.pi α = {app := λ (f : Π (i : I), C i) (i : I), (α i).app (f i), naturality' := _}
@[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)