ιObj — Mathlib

English

The inclusion morphism ιObj I κ f from X into obj I κ f exhibits the intermediate object used in the small object factorization.

Русский

Включение ιObj I κ f из X в obj I κ f демонстрирует промежуточный объект в факторизации малого объекта.

LaTeX

$$$\\iota_{\\mathrm{Obj}}: X \\to \\mathrm{obj}(I,\\kappa,f)$$$

Lean4

/-- The "inclusion" morphism in the factorization given by
the small object argument. -/
noncomputable def ιObj : X ⟶ obj I κ f :=
  ((ιIteration I κ).app (Arrow.mk f)).left

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