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 (CategoryTheory.Discrete α)

Equations

• ⋯ = ⋯

class CategoryTheory.CountableCategory (J : Type u_1) [CategoryTheory.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')

theorem CategoryTheory.CountableCategory.countableObj {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] [self : CategoryTheory.CountableCategory J] : Countable J

theorem CategoryTheory.CountableCategory.countableHom {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] [self : CategoryTheory.CountableCategory J] (j : J) (j' : J) : Countable (j ⟶ j')

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

Equations

• ⋯ = ⋯

instance CategoryTheory.instCountableCategoryNat : CategoryTheory.CountableCategory ℕ

Equations

• CategoryTheory.instCountableCategoryNat = ⋯

@[reducible, inline]

abbrev CategoryTheory.CountableCategory.ObjAsType (α : Type u) [CategoryTheory.Category.{v, u} α] [CategoryTheory.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) [CategoryTheory.Category.{v, u} α] [CategoryTheory.CountableCategory α] : Countable (CategoryTheory.CountableCategory.ObjAsType α)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

The constructed category is indeed equivalent to α.

Equations

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

def CategoryTheory.CountableCategory.HomAsType (α : Type u) [CategoryTheory.Category.{v, u} α] [CategoryTheory.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) [CategoryTheory.Category.{v, u} α] [CategoryTheory.CountableCategory α] : CategoryTheory.LocallySmall.{0, v, 0} (CategoryTheory.CountableCategory.ObjAsType α)

Equations

• ⋯ = ⋯

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.CountableCategory.homAsTypeEquiv (α : Type u) [CategoryTheory.Category.{v, u} α] [CategoryTheory.CountableCategory α] : CategoryTheory.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) [CategoryTheory.Category.{u_1, u_1} α] [CategoryTheory.FinCategory α] : CategoryTheory.CountableCategory α

Equations

• ⋯ = ⋯

instance CategoryTheory.instCountableCategoryNat_1 : CategoryTheory.CountableCategory ℕ

Equations

• CategoryTheory.instCountableCategoryNat_1 = ⋯

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

The opposite of a countable category is countable.

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯