English
There is a canonical natural transformation from the identity functor on the category of D-valued presheaves on C (i.e., from every presheaf P to P⁺) to the plus-construction, natural in P. In particular, for every presheaf P, there is a morphism P → P⁺ given by the universal plus-operation, and these morphisms form a natural transformation.
Русский
Существует каноническое естественное преобразование от тождественного функтору над категорией пресеоф-в значениях в D к операции plus, естественное по P. Конкретно: для каждого пресешефа P есть морфизм P → P⁺, и эти морфизмы образуют естественное преобразование.
LaTeX
$$$\\eta: \\mathrm{Id}_{(C^{\\mathrm{op}} \\to D)} \\Rightarrow J^{+} \\quad\\text{с } \\eta_P = J.toPlus P \\text{ для всех } P$$$
Lean4
/-- The natural transformation from the identity functor to `plus`. -/
@[simps]
def toPlusNatTrans : 𝟭 (Cᵒᵖ ⥤ D) ⟶ J.plusFunctor D where app P := J.toPlus P
