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

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

Equations

• ⋯ = ⋯

@[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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

theorem CategoryTheory.Limits.HasCountableColimits.out {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} [self : CategoryTheory.Limits.HasCountableColimits C] (J : Type) [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : 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

Equations

• ⋯ = ⋯

@[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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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.Limits.sequentialFunctor J).Initial

Equations

• ⋯ = ⋯