Countable limits and colimits

A typeclass for categories with all countable (co)limits.

We also prove that all cofiltered limits over countable preorders are isomorphic to sequential limits, see sequentialFunctor_initial.

Projects

• There is a series of proof_wanted at the bottom of this file, implying that all cofiltered limits over countable categories are isomorphic to sequential limits.

• Prove the dual result for filtered colimits.

class CategoryTheory.Limits.HasCountableLimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] : Prop

A category has all countable limits if every functor J ⥤ C with a CountableCategory J instance and J : Type has a limit.

• out (J : Type) [CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J] : CategoryTheory.Limits.HasLimitsOfShape J C

  C has all limits over any type J whose objects and morphisms lie in the same universe and which has countably many objects and morphisms

@[instance 100]

instance CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasCountableLimits C] : CategoryTheory.Limits.HasFiniteLimits C

@[instance 100]

instance CategoryTheory.Limits.hasCountableLimits_of_hasLimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasLimits C] : CategoryTheory.Limits.HasCountableLimits C

instance CategoryTheory.Limits.instHasLimitsOfShapeOfCountableCategoryOfHasCountableLimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (J : Type u_2) [CategoryTheory.Category.{v, u_2} J] [CategoryTheory.CountableCategory J] [CategoryTheory.Limits.HasCountableLimits C] : CategoryTheory.Limits.HasLimitsOfShape J C

class CategoryTheory.Limits.HasCountableProducts (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] : Prop

A category has countable products if it has all products indexed by countable types.

• out (J : Type) [Countable J] : CategoryTheory.Limits.HasProductsOfShape J C

instance CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProducts (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (J : Type u_2) [Countable J] [CategoryTheory.Limits.HasCountableProducts C] : CategoryTheory.Limits.HasProductsOfShape J C

@[instance 100]

instance CategoryTheory.Limits.hasCountableProducts_of_hasProducts (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Limits.HasCountableProducts C

@[instance 100]

instance CategoryTheory.Limits.hasCountableProducts_of_hasCountableLimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasCountableLimits C] : CategoryTheory.Limits.HasCountableProducts C

@[instance 100]

instance CategoryTheory.Limits.hasFiniteProducts_of_hasCountableProducts (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasCountableProducts C] : CategoryTheory.Limits.HasFiniteProducts C

class CategoryTheory.Limits.HasCountableColimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] : Prop

A category has all countable colimits if every functor J ⥤ C with a CountableCategory J instance and J : Type has a colimit.

• out (J : Type) [CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J] : CategoryTheory.Limits.HasColimitsOfShape J C

  C has all limits over any type J whose objects and morphisms lie in the same universe and which has countably many objects and morphisms

@[instance 100]

instance CategoryTheory.Limits.hasFiniteColimits_of_hasCountableColimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasCountableColimits C] : CategoryTheory.Limits.HasFiniteColimits C

@[instance 100]

instance CategoryTheory.Limits.hasCountableColimits_of_hasColimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasColimits C] : CategoryTheory.Limits.HasCountableColimits C

instance CategoryTheory.Limits.instHasColimitsOfShapeOfCountableCategoryOfHasCountableColimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (J : Type u_2) [CategoryTheory.Category.{v, u_2} J] [CategoryTheory.CountableCategory J] [CategoryTheory.Limits.HasCountableColimits C] : CategoryTheory.Limits.HasColimitsOfShape J C

class CategoryTheory.Limits.HasCountableCoproducts (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] : Prop

A category has countable coproducts if it has all coproducts indexed by countable types.

• out (J : Type) [Countable J] : CategoryTheory.Limits.HasCoproductsOfShape J C

@[instance 100]

instance CategoryTheory.Limits.hasCountableCoproducts_of_hasCoproducts (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasCoproducts C] : CategoryTheory.Limits.HasCountableCoproducts C

instance CategoryTheory.Limits.instHasCoproductsOfShapeOfHasCountableCoproducts (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (J : Type u_2) [Countable J] [CategoryTheory.Limits.HasCountableCoproducts C] : CategoryTheory.Limits.HasCoproductsOfShape J C

@[instance 100]

instance CategoryTheory.Limits.hasCountableCoproducts_of_hasCountableColimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasCountableColimits C] : CategoryTheory.Limits.HasCountableCoproducts C

@[instance 100]

instance CategoryTheory.Limits.hasFiniteCoproducts_of_hasCountableCoproducts (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasCountableCoproducts C] : CategoryTheory.Limits.HasFiniteCoproducts C

noncomputable def CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsFiltered J] : ℕ → J

The object part of the initial functor ℕᵒᵖ ⥤ J

Equations

• CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj J Nat.zero = ⋯.choose 0
• CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj J n.succ = ⋯.choose

theorem CategoryTheory.Limits.IsFiltered.sequentialFunctor_map (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsFiltered J] : Monotone (CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj J)

noncomputable def CategoryTheory.Limits.IsFiltered.sequentialFunctor (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsFiltered J] : CategoryTheory.Functor ℕ J

The initial functor ℕᵒᵖ ⥤ J, which allows us to turn cofiltered limits over countable preorders into sequential limits.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.IsFiltered.sequentialFunctor_final_aux (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsFiltered J] (j : J) : ∃ (n : ℕ), j ≤ CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj J n

instance CategoryTheory.Limits.IsFiltered.sequentialFunctor_final (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsFiltered J] : (CategoryTheory.Limits.IsFiltered.sequentialFunctor J).Final

noncomputable def CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsCofiltered J] : ℕ → J

The object part of the initial functor ℕᵒᵖ ⥤ J

Equations

• CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj J Nat.zero = ⋯.choose 0
• CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj J n.succ = ⋯.choose

theorem CategoryTheory.Limits.IsCofiltered.sequentialFunctor_map (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsCofiltered J] : Antitone (CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj J)

noncomputable def CategoryTheory.Limits.IsCofiltered.sequentialFunctor (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsCofiltered J] : CategoryTheory.Functor ℕᵒᵖ J

The initial functor ℕᵒᵖ ⥤ J, which allows us to turn cofiltered limits over countable preorders into sequential limits.

TODO: redefine this as (IsFiltered.sequentialFunctor Jᵒᵖ).leftOp. This would need API for initial/ final functors of the form leftOp/rightOp.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial_aux (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsCofiltered J] (j : J) : ∃ (n : ℕ), CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj J n ≤ j

instance CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsCofiltered J] : (CategoryTheory.Limits.IsCofiltered.sequentialFunctor J).Initial

@[deprecated CategoryTheory.Limits.IsCofiltered.sequentialFunctor]

def CategoryTheory.Limits.sequentialFunctor (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsCofiltered J] : CategoryTheory.Functor ℕᵒᵖ J

Alias of CategoryTheory.Limits.IsCofiltered.sequentialFunctor.

---

The initial functor ℕᵒᵖ ⥤ J, which allows us to turn cofiltered limits over countable preorders into sequential limits.

TODO: redefine this as (IsFiltered.sequentialFunctor Jᵒᵖ).leftOp. This would need API for initial/ final functors of the form leftOp/rightOp.

Equations

• CategoryTheory.Limits.sequentialFunctor = CategoryTheory.Limits.IsCofiltered.sequentialFunctor

@[deprecated CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj]

def CategoryTheory.Limits.sequentialFunctor_obj (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsCofiltered J] : ℕ → J

Alias of CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj.

---

The object part of the initial functor ℕᵒᵖ ⥤ J

Equations

• CategoryTheory.Limits.sequentialFunctor_obj = CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj

@[deprecated CategoryTheory.Limits.IsCofiltered.sequentialFunctor_map]

theorem CategoryTheory.Limits.sequentialFunctor_map (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsCofiltered J] : Antitone (CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj J)

Alias of CategoryTheory.Limits.IsCofiltered.sequentialFunctor_map.

@[deprecated CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial_aux]

theorem CategoryTheory.Limits.sequentialFunctor_initial_aux (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsCofiltered J] (j : J) : ∃ (n : ℕ), CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj J n ≤ j

Alias of CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial_aux.

@[deprecated CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial]

theorem CategoryTheory.Limits.sequentialFunctor_initial (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsCofiltered J] : (CategoryTheory.Limits.IsCofiltered.sequentialFunctor J).Initial

Alias of CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial.