mathlib3 documentation

category_theory.limits.pi

Limits in the category of indexed families of objects. #

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

Given a functor F : J ⥤ Π i, C i into a category of indexed families,

  1. we can assemble a collection of cones over F ⋙ pi.eval C i into a cone over F
  2. if all those cones are limit cones, the assembled cone is a limit cone, and
  3. if we have limits for each of F ⋙ pi.eval C i, we can produce a has_limit F instance
source
def category_theory.pi.cone_comp_eval {I : Type v₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {J : Type v₁} [category_theory.small_category J] {F : J ⥤ Π (i : I), C i} (c : category_theory.limits.cone F) (i : I) :
category_theory.limits.cone (F ⋙ category_theory.pi.eval C i)

A cone over F : J ⥤ Π i, C i has as its components cones over each of the F ⋙ pi.eval C i.

Equations
source
def category_theory.pi.cocone_comp_eval {I : Type v₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {J : Type v₁} [category_theory.small_category J] {F : J ⥤ Π (i : I), C i} (c : category_theory.limits.cocone F) (i : I) :
category_theory.limits.cocone (F ⋙ category_theory.pi.eval C i)

A cocone over F : J ⥤ Π i, C i has as its components cocones over each of the F ⋙ pi.eval C i.

Equations
source
def category_theory.pi.cone_of_cone_comp_eval {I : Type v₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {J : Type v₁} [category_theory.small_category J] {F : J ⥤ Π (i : I), C i} (c : Π (i : I), category_theory.limits.cone (F ⋙ category_theory.pi.eval C i)) :
category_theory.limits.cone F

Given a family of cones over the F ⋙ pi.eval C i, we can assemble these together as a cone F.

Equations
source
def category_theory.pi.cocone_of_cocone_comp_eval {I : Type v₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {J : Type v₁} [category_theory.small_category J] {F : J ⥤ Π (i : I), C i} (c : Π (i : I), category_theory.limits.cocone (F ⋙ category_theory.pi.eval C i)) :
category_theory.limits.cocone F

Given a family of cocones over the F ⋙ pi.eval C i, we can assemble these together as a cocone F.

Equations
source
def category_theory.pi.cone_of_cone_eval_is_limit {I : Type v₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {J : Type v₁} [category_theory.small_category J] {F : J ⥤ Π (i : I), C i} {c : Π (i : I), category_theory.limits.cone (F ⋙ category_theory.pi.eval C i)} (P : Π (i : I), category_theory.limits.is_limit (c i)) :
category_theory.limits.is_limit (category_theory.pi.cone_of_cone_comp_eval c)

Given a family of limit cones over the F ⋙ pi.eval C i, assembling them together as a cone F produces a limit cone.

Equations
source
def category_theory.pi.cocone_of_cocone_eval_is_colimit {I : Type v₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {J : Type v₁} [category_theory.small_category J] {F : J ⥤ Π (i : I), C i} {c : Π (i : I), category_theory.limits.cocone (F ⋙ category_theory.pi.eval C i)} (P : Π (i : I), category_theory.limits.is_colimit (c i)) :
category_theory.limits.is_colimit (category_theory.pi.cocone_of_cocone_comp_eval c)

Given a family of colimit cocones over the F ⋙ pi.eval C i, assembling them together as a cocone F produces a colimit cocone.

Equations
source
theorem category_theory.pi.has_limit_of_has_limit_comp_eval {I : Type v₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {J : Type v₁} [category_theory.small_category J] {F : J ⥤ Π (i : I), C i} [∀ (i : I), category_theory.limits.has_limit (F ⋙ category_theory.pi.eval C i)] :
category_theory.limits.has_limit F

If we have a functor F : J ⥤ Π i, C i into a category of indexed families, and we have limits for each of the F ⋙ pi.eval C i, then F has a limit.

source
theorem category_theory.pi.has_colimit_of_has_colimit_comp_eval {I : Type v₁} {C : I → Type u₁} [Π (i : I), category_theory.category (C i)] {J : Type v₁} [category_theory.small_category J] {F : J ⥤ Π (i : I), C i} [∀ (i : I), category_theory.limits.has_colimit (F ⋙ category_theory.pi.eval C i)] :
category_theory.limits.has_colimit F

If we have a functor F : J ⥤ Π i, C i into a category of indexed families, and colimits exist for each of the F ⋙ pi.eval C i, there is a colimit for F.

As an example, we can use this to construct particular shapes of limits in a category of indexed families.

With the addition of import category_theory.limits.shapes.types we can use:

local attribute [instance] has_limit_of_has_limit_comp_eval
example : has_binary_products (I → Type v₁) := ⟨by apply_instance⟩