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) [inst : CategoryTheory.SmallCategory J] [inst_1 : 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 CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasCountableLimits C] : CategoryTheory.Limits.HasFiniteLimits C

Equations

• (_ : CategoryTheory.Limits.HasFiniteLimits C) = (_ : CategoryTheory.Limits.HasFiniteLimits C)

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

Equations

• (_ : CategoryTheory.Limits.HasCountableLimits C) = (_ : CategoryTheory.Limits.HasCountableLimits C)

instance CategoryTheory.Limits.instHasLimitsOfShape (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

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape J C) = (_ : CategoryTheory.Limits.HasLimitsOfShape J 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) [inst : CategoryTheory.SmallCategory J] [inst_1 : 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 CategoryTheory.Limits.hasFiniteColimits_of_hasCountableColimits (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasCountableColimits C] : CategoryTheory.Limits.HasFiniteColimits C

Equations

• (_ : CategoryTheory.Limits.HasFiniteColimits C) = (_ : CategoryTheory.Limits.HasFiniteColimits C)

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

Equations

• (_ : CategoryTheory.Limits.HasCountableColimits C) = (_ : CategoryTheory.Limits.HasCountableColimits C)

instance CategoryTheory.Limits.instHasColimitsOfShape (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

Equations

• (_ : CategoryTheory.Limits.HasColimitsOfShape J C) = (_ : CategoryTheory.Limits.HasColimitsOfShape J C)

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

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

Equations

• One or more equations did not get rendered due to their size.
• CategoryTheory.Limits.sequentialFunctor_obj J Nat.zero = Exists.choose (_ : ∃ (f : ℕ → J), Function.Surjective f) 0

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

noncomputable def CategoryTheory.Limits.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.

Equations

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

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

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

Equations

• (_ : CategoryTheory.Functor.Initial (CategoryTheory.Limits.sequentialFunctor J)) = (_ : CategoryTheory.Functor.Initial (CategoryTheory.Limits.sequentialFunctor J))