Countable categories

A category is countable in this sense if it has countably many objects and countably many morphisms.

instance CategoryTheory.discreteCountable {α : Type u_1} [Countable α] : Countable (Discrete α)

class CategoryTheory.CountableCategory (J : Type u_1) [Category.{u_2, u_1} J] : Prop

A category with countably many objects and morphisms.

• countableObj : Countable J
• countableHom (j j' : J) : Countable (j ⟶ j')

instance CategoryTheory.countablerCategoryDiscreteOfCountable (J : Type u_1) [Countable J] : CountableCategory (Discrete J)

instance CategoryTheory.instCountableCategoryNat : CountableCategory ℕ

@[reducible, inline]

abbrev CategoryTheory.CountableCategory.ObjAsType (α : Type u) [Category.{v, u} α] [CountableCategory α] : Type

A countable category α is equivalent to a category with objects in Type.

Equations

• CategoryTheory.CountableCategory.ObjAsType α = CategoryTheory.InducedCategory α ⇑(equivShrink α).symm

instance CategoryTheory.CountableCategory.instCountableObjAsType (α : Type u) [Category.{v, u} α] [CountableCategory α] : Countable (ObjAsType α)

instance CategoryTheory.CountableCategory.instCountableHomObjAsType (α : Type u) [Category.{v, u} α] [CountableCategory α] {i j : ObjAsType α} : Countable (i ⟶ j)

instance CategoryTheory.CountableCategory.instObjAsType (α : Type u) [Category.{v, u} α] [CountableCategory α] : CountableCategory (ObjAsType α)

noncomputable def CategoryTheory.CountableCategory.objAsTypeEquiv (α : Type u) [Category.{v, u} α] [CountableCategory α] : ObjAsType α ≌ α

The constructed category is indeed equivalent to α.

Equations

• CategoryTheory.CountableCategory.objAsTypeEquiv α = (CategoryTheory.inducedFunctor ⇑(equivShrink α).symm).asEquivalence

def CategoryTheory.CountableCategory.HomAsType (α : Type u) [Category.{v, u} α] [CountableCategory α] : Type

A countable category α is equivalent to a small category with objects in Type.

Equations

• CategoryTheory.CountableCategory.HomAsType α = CategoryTheory.ShrinkHoms.{0} (CategoryTheory.CountableCategory.ObjAsType α)

instance CategoryTheory.CountableCategory.instLocallySmallObjAsType (α : Type u) [Category.{v, u} α] [CountableCategory α] : LocallySmall.{0, v, 0} (ObjAsType α)

instance CategoryTheory.CountableCategory.instSmallCategoryHomAsType (α : Type u) [Category.{v, u} α] [CountableCategory α] : SmallCategory (HomAsType α)

Equations

• CategoryTheory.CountableCategory.instSmallCategoryHomAsType α = inferInstanceAs (CategoryTheory.SmallCategory (CategoryTheory.ShrinkHoms.{0} (CategoryTheory.CountableCategory.ObjAsType α)))

instance CategoryTheory.CountableCategory.instCountableHomAsType (α : Type u) [Category.{v, u} α] [CountableCategory α] : Countable (HomAsType α)

instance CategoryTheory.CountableCategory.instCountableHomHomAsType (α : Type u) [Category.{v, u} α] [CountableCategory α] {i j : HomAsType α} : Countable (i ⟶ j)

instance CategoryTheory.CountableCategory.instHomAsType (α : Type u) [Category.{v, u} α] [CountableCategory α] : CountableCategory (HomAsType α)

noncomputable def CategoryTheory.CountableCategory.homAsTypeEquiv (α : Type u) [Category.{v, u} α] [CountableCategory α] : HomAsType α ≌ α

The constructed category is indeed equivalent to α.

Equations

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

instance CategoryTheory.instCountableCategoryOfFinCategory (α : Type u_1) [Category.{u_1, u_1} α] [FinCategory α] : CountableCategory α

instance CategoryTheory.instCountableCategoryNat_1 : CountableCategory ℕ

instance CategoryTheory.countableCategoryOpposite {J : Type u_1} [Category.{u_2, u_1} J] [CountableCategory J] : CountableCategory Jᵒᵖ

The opposite of a countable category is countable.

instance CategoryTheory.countableCategoryUlift {J : Type v} [Category.{u_1, v} J] [CountableCategory J] : CountableCategory (ULiftHom (ULift.{w, v} J))

Applying ULift to morphisms and objects of a category preserves countability.