llp_rlp_ιObj — Mathlib

English

Let I be a morphism property of a category and κ a regular cardinal with the small object argument. Then the map ιObj(I, κ, f) has the left lifting property with respect to all morphisms in I.rlp, for every morphism f: X → Y in the category.

Русский

Пусть I — свойство морфизмов в произвольной категории, κ — регулярное кардинальное число и дан аргумент малого объекта. Тогда отображение ιObj(I, κ, f) имеет левую подстановку по отношению ко всем стрелкам из I.rlp для каждого морфизма f: X → Y.

LaTeX

$$$I.rlp.llp\ (\iotaObj I \kappa f)$$$

Lean4

theorem llp_rlp_ιObj : I.rlp.llp (ιObj I κ f) :=
  by
  apply I.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp κ.ord.toType
  apply transfiniteCompositionsOfShape_ιObj

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