English
A variant form of left-exact preservation: the induced finite-limit preservation holds in the specified setting.
Русский
Вариант сохранения конечных пределов для левой точности в заданной конфигурации.
LaTeX
$$$\\text{PreservesFiniteLimits}(\\text{inverseAux.obj } F)$$$
Lean4
instance (F : C ⥤ₗ Type v) : PreservesFiniteLimits (inverseAux.obj F) where
preservesFiniteLimits J _
_ :=
have : PreservesLimitsOfShape J (inverseAux.obj F ⋙ forget AddCommGrpCat) :=
inferInstanceAs (PreservesLimitsOfShape J F.1)
preservesLimitsOfShape_of_reflects_of_preserves _ (forget AddCommGrpCat)
