instLocallySmallTotal — Mathlib

English

For every j in J X, the diagonal presentation object (h.colimitPresentation X).diag.obj j is presentable.

Русский

Для каждого j из J X диагональный презентационный объект является презентируемым.

LaTeX

$$$\forall j : h.J X,\ IsPresentable((h.colimitPresentation X).diag.obj j)$$$

Lean4

instance [LocallySmall.{w} C] [LocallySmall.{w} J] : LocallySmall.{w} (Total P) where
  hom_small k
    l :=
    let f (x : k ⟶ l) : (k.1 ⟶ l.1) × ((P k.1).diag.obj k.2 ⟶ (P l.1).diag.obj l.2) := (x.base, x.hom)
    small_of_injective (f := f) (by grind [Function.Injective, Total.Hom.ext])

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