isCardinalPresentable — Mathlib

English

If every diagram object p.diag.obj j is κ-presentable and κ ≤ κ', along with a cardinal-limited condition on Arrow J, then X is κ'-presentable.

Русский

Если каждый объект диаграммы p.diag.obj j является κ-представимым и κ ≤ κ', а также выполняются требования HasCardinalLT для Arrow J, то X является κ'-представимым.

LaTeX

$$$\forall j:\, J,\ IsCardinalPresentable (p.diag.obj j) \kappa \Rightarrow [\kappa \le \kappa'] (HasCardinalLT (Arrow J) \kappa') \Rightarrow IsCardinalPresentable X \kappa'$$$

Lean4

theorem isCardinalPresentable {X : C} {J : Type w} [SmallCategory J] (p : ColimitPresentation J X) (κ : Cardinal.{w})
    [Fact κ.IsRegular] (h : ∀ (j : J), IsCardinalPresentable (p.diag.obj j) κ) [LocallySmall.{w} C] (κ' : Cardinal.{w})
    [Fact κ'.IsRegular] (h : κ ≤ κ') (hJ : HasCardinalLT (Arrow J) κ') : IsCardinalPresentable X κ' :=
  have (k : J) : IsCardinalPresentable (p.diag.obj k) κ' := isCardinalPresentable_of_le _ h
  isCardinalPresentable_of_isColimit _ p.isColimit κ' hJ

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