presentable — Mathlib

English

There is a general presentability result: every X in LocallySmall C is presentable.

Русский

Существует общая презентабельность: каждый объект X из LocallySmall C презентируем.

LaTeX

$$$\forall X,\ IsPresentable X$$$

Lean4

theorem presentable [LocallySmall.{w} C] (X : C) : IsPresentable.{w} X :=
  by
  obtain ⟨κ', _, le, hκ'⟩ :
    ∃ (κ' : Cardinal.{w}) (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'), HasCardinalLT (Arrow (h.J X)) κ' :=
    by
    obtain ⟨κ', h₁, h₂⟩ :=
      HasCardinalLT.exists_regular_cardinal_forall.{w}
        (Sum.elim (fun (_ : Unit) ↦ Arrow (h.J X)) (fun (_ : Unit) ↦ κ.ord.toType))
    exact ⟨κ', ⟨h₁⟩, le_of_lt (by simpa [hasCardinalLT_iff_cardinal_mk_lt] using h₂ (Sum.inr ⟨⟩)), h₂ (Sum.inl ⟨⟩)⟩
  have := (h.colimitPresentation X).isCardinalPresentable κ (by infer_instance) κ' le hκ'
  exact isPresentable_of_isCardinalPresentable _ κ'

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