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) [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) [SmallCategory J] [CountableCategory J] : 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) [Category.{u_3, u_1} C] [HasCountableLimits C] : HasFiniteLimits C

@[instance 100]

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

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

class CategoryTheory.Limits.HasCountableProducts (C : Type u_1) [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] : HasProductsOfShape J C

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

class CategoryTheory.Limits.HasCountableColimits (C : Type u_1) [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) [SmallCategory J] [CountableCategory J] : 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) [Category.{u_3, u_1} C] [HasCountableColimits C] : HasFiniteColimits C

@[instance 100]

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

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

class CategoryTheory.Limits.HasCountableCoproducts (C : Type u_1) [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] : HasCoproductsOfShape J C

@[instance 100]

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

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

@[instance 100]

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

@[instance 100]

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

noncomputable def CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj (J : Type u_2) [Countable J] [Preorder J] [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] [IsFiltered J] : Monotone (sequentialFunctor_obj J)

noncomputable def CategoryTheory.Limits.IsFiltered.sequentialFunctor (J : Type u_2) [Countable J] [Preorder J] [IsFiltered J] : 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] [IsFiltered J] (j : J) : ∃ (n : ℕ), j ≤ sequentialFunctor_obj J n

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

noncomputable def CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj (J : Type u_2) [Countable J] [Preorder J] [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] [IsCofiltered J] : Antitone (sequentialFunctor_obj J)

noncomputable def CategoryTheory.Limits.IsCofiltered.sequentialFunctor (J : Type u_2) [Countable J] [Preorder J] [IsCofiltered J] : 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] [IsCofiltered J] (j : J) : ∃ (n : ℕ), sequentialFunctor_obj J n ≤ j

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

@[deprecated CategoryTheory.Limits.IsCofiltered.sequentialFunctor (since := "2024-11-01")]

def CategoryTheory.Limits.sequentialFunctor (J : Type u_2) [Countable J] [Preorder J] [IsCofiltered J] : 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 (since := "2024-11-01")]

def CategoryTheory.Limits.sequentialFunctor_obj (J : Type u_2) [Countable J] [Preorder J] [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 (since := "2024-11-01")]

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

Alias of CategoryTheory.Limits.IsCofiltered.sequentialFunctor_map.

@[deprecated CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial_aux (since := "2024-11-01")]

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

Alias of CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial_aux.

@[deprecated CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial (since := "2024-11-01")]

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

Alias of CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial.