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

• (_ : Countable (CategoryTheory.Discrete α)) = (_ : Countable (CategoryTheory.Discrete α))

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')

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

Equations

• (_ : CategoryTheory.CountableCategory (CategoryTheory.Discrete J)) = (_ : CategoryTheory.CountableCategory (CategoryTheory.Discrete J))

@[inline, reducible]

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

• (_ : Countable (CategoryTheory.CountableCategory.ObjAsType α)) = (_ : Countable (CategoryTheory.CountableCategory.ObjAsType α))

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

Equations

• (_ : Countable (i ⟶ j)) = (_ : Countable ((equivShrink α).symm i ⟶ (equivShrink α).symm j))

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

Equations

• (_ : CategoryTheory.CountableCategory (CategoryTheory.CountableCategory.ObjAsType α)) = (_ : CategoryTheory.CountableCategory (CategoryTheory.CountableCategory.ObjAsType α))

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.Functor.asEquivalence (CategoryTheory.inducedFunctor ⇑(equivShrink α).symm)

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

Equations

• (_ : CategoryTheory.LocallySmall.{0, v, 0} (CategoryTheory.CountableCategory.ObjAsType α)) = (_ : CategoryTheory.LocallySmall.{0, v, 0} (CategoryTheory.CountableCategory.ObjAsType α))

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

Equations

• CategoryTheory.CountableCategory.instSmallCategoryHomAsType α = CategoryTheory.ShrinkHoms.instCategoryShrinkHoms (CategoryTheory.CountableCategory.ObjAsType α)

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

Equations

• (_ : Countable (CategoryTheory.CountableCategory.HomAsType α)) = (_ : Countable (CategoryTheory.CountableCategory.HomAsType α))

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

Equations

• (_ : Countable (i ⟶ j)) = (_ : Countable (i ⟶ j))

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

Equations

• (_ : CategoryTheory.CountableCategory (CategoryTheory.CountableCategory.HomAsType α)) = (_ : CategoryTheory.CountableCategory (CategoryTheory.CountableCategory.HomAsType α))

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

Equations

• (_ : CategoryTheory.CountableCategory α) = (_ : CategoryTheory.CountableCategory α)

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

• (_ : CategoryTheory.CountableCategory Jᵒᵖ) = (_ : CategoryTheory.CountableCategory Jᵒᵖ)

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

• (_ : CategoryTheory.CountableCategory (CategoryTheory.ULiftHom (ULift.{w, v} J))) = (_ : CategoryTheory.CountableCategory (CategoryTheory.ULiftHom (ULift.{w, v} J)))