Theorems · Theorem · category theory

CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat_and_finite

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCountableCoproducts C]
  [CategoryTheory.Limits.HasFiniteLimits C]
  [∀ (J : Type) [inst_3 : Finite J], CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete J) C]
  [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ℕ) C], CategoryTheory.CountableAB4 C

Checking exactness of colimits of shape Discrete ℕ and Discrete J for finite J is enough for countable AB4.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Cited by

1 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasCountableCoproductsCategoryTheory.Limits.HasFiniteLimitsCategoryTheory.HasExactColimitsOfShapeCategoryTheory.HasExactColimitsOfShape