instIsPresentableOfIsAccessibleCategory

English

If a category has IsAccessibleCategory, then every object is presentable (with a fixed κ).

Русский

Если категория имеет IsAccessibleCategory, то каждый объект представим (для фиксированного κ).

LaTeX

$$$\forall X\,\text{IsPresentable}(X)$$$

Lean4

instance [IsAccessibleCategory.{w} C] (X : C) : IsPresentable.{w} X :=
  by
  obtain ⟨κ, _, _⟩ := IsAccessibleCategory.exists_cardinal C
  obtain ⟨ι, G, h⟩ := HasCardinalFilteredGenerators.exists_generators C κ
  apply h.presentable

Похожие утверждения