English
An auxiliary construction provides an IsLimit for a cone obtained by applying a forgetful process from commutative groups to commutative monoids; this speeds up typechecking in limit arguments.
Русский
Дополнительная конструкция обеспечивает изоморфизм предела для конуса, полученного применением функторa забывания из коммутативных групп к коммутативным моноидам; это ускоряет проверки типов при работе с пределами.
LaTeX
$$$\\text{forget}_{CommGrpCat\\to CommMonCat}\\;\\text{mapCone}(\\limCone F)\\;\\text{isLimit}$$$
Lean4
/-- An auxiliary declaration to speed up typechecking. -/
@[to_additive AddCommGrpCat.forget₂AddCommMon_preservesLimitsAux /--
An auxiliary declaration to speed up typechecking. -/
]
noncomputable def forget₂CommMon_preservesLimitsAux [Small.{u} (F ⋙ forget CommGrpCat).sections] :
IsLimit ((forget₂ CommGrpCat.{u} CommMonCat.{u}).mapCone (limitCone.{v, u} F)) :=
letI : Small.{u} (Functor.sections ((F ⋙ forget₂ _ CommMonCat) ⋙ forget CommMonCat)) :=
inferInstanceAs <| Small (Functor.sections (F ⋙ forget CommGrpCat))
CommMonCat.limitConeIsLimit.{v, u} (F ⋙ forget₂ CommGrpCat.{u} CommMonCat.{u})
