Presentable objects in Type

In this file, we show that if κ : Cardinal.{u} is a regular cardinal, then X : Type u is κ-presentable in the category of types iff HasCardinalLT X κ holds, i.e. the cardinal number of X is less than κ.

theorem HasCardinalLT.isCardinalPresentable {X : Type u} {κ : Cardinal.{u}} (hX : HasCardinalLT X κ) [Fact κ.IsRegular] : CategoryTheory.IsCardinalPresentable X κ

@[reducible, inline]

abbrev HasCardinalLT.Set (X : Type u) (κ : Cardinal.{u}) : Type u

Given X : Type u and κ : Cardinal.{u} X, this is the preordered type of subsets of X of cardinality < κ.

Equations

• HasCardinalLT.Set X κ = { A : Set X // HasCardinalLT (↑A) κ }

instance HasCardinalLT.Set.instIsCardinalFiltered (X : Type u) (κ : Cardinal.{u}) [Fact κ.IsRegular] : CategoryTheory.IsCardinalFiltered (HasCardinalLT.Set X κ) κ

instance HasCardinalLT.Set.instIsFilteredOfFactIsRegular (X : Type u) (κ : Cardinal.{u}) [Fact κ.IsRegular] : CategoryTheory.IsFiltered (HasCardinalLT.Set X κ)

theorem HasCardinalLT.Set.isFiltered_of_aleph0_le (X : Type u) (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) : CategoryTheory.IsFiltered (HasCardinalLT.Set X κ)

def HasCardinalLT.Set.functor (X : Type u) (κ : Cardinal.{u}) : CategoryTheory.Functor (HasCardinalLT.Set X κ) (Type u)

The functor HasCardinalLT.Set X κ ⥤ Type u which sends a subset of X of cardinality κ to the corresponding subtype.

Equations

• HasCardinalLT.Set.functor X κ = ⋯.functor.comp Set.functorToTypes

@[simp]

theorem HasCardinalLT.Set.functor_map_hom_apply_coe (X : Type u) (κ : Cardinal.{u}) {X✝ Y✝ : HasCardinalLT.Set X κ} (f : X✝ ⟶ Y✝) (x✝ : ↑(⋯.functor.obj X✝)) : ↑((CategoryTheory.ConcreteCategory.hom ((functor X κ).map f)) x✝) = ↑x✝

@[simp]

theorem HasCardinalLT.Set.functor_obj (X : Type u) (κ : Cardinal.{u}) (X✝ : HasCardinalLT.Set X κ) : (functor X κ).obj X✝ = ↑↑X✝

def HasCardinalLT.Set.cocone (X : Type u) (κ : Cardinal.{u}) : CategoryTheory.Limits.Cocone (functor X κ)

The cocone for Set.functor X κ : HasCardinalLT.Set X κ ⥤ Type u with point X.

Equations

• HasCardinalLT.Set.cocone X κ = { pt := X, ι := { app := fun (x : HasCardinalLT.Set X κ) => TypeCat.ofHom Subtype.val, naturality := ⋯ } }

@[simp]

theorem HasCardinalLT.Set.cocone_pt (X : Type u) (κ : Cardinal.{u}) : (cocone X κ).pt = X

@[simp]

theorem HasCardinalLT.Set.cocone_ι_app (X : Type u) (κ : Cardinal.{u}) (x✝ : HasCardinalLT.Set X κ) : (cocone X κ).ι.app x✝ = TypeCat.ofHom Subtype.val

noncomputable def HasCardinalLT.Set.isColimitCocone (X : Type u) (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) : CategoryTheory.Limits.IsColimit (cocone X κ)

Any type X is the (filtered) colimit of its subsets of cardinality < κ when κ is an infinite cardinal. (This colimit is κ-filtered when κ is a regular cardinal.)

Equations

• HasCardinalLT.Set.isColimitCocone X κ hκ = CategoryTheory.Limits.Types.FilteredColimit.isColimitOf' (HasCardinalLT.Set.functor X κ) (HasCardinalLT.Set.cocone X κ) ⋯ ⋯

theorem CategoryTheory.Types.isCardinalPresentable_iff {X : Type u} (κ : Cardinal.{u}) [Fact κ.IsRegular] : IsCardinalPresentable X κ ↔ HasCardinalLT X κ

instance CategoryTheory.Types.instIsPresentable (X : Type u) : IsPresentable.{u, u, u + 1} X