forget₂AddCommGroup_preservesLimitsAux

English

An auxiliary limit assertion speeds up type checking by encoding a limit cone condition in an auxiliary form.

Русский

Дополнительное утверждение о пределе ускоряет проверку типов за счет формализации условия предела во вспомогательной форме.

LaTeX

$$$\text{Auxiliary limit: } IsLimit((forget}(\mathrm{ModuleCat}\,R)).mapCone(\text{limitCone }F)$$$

Lean4

/-- An auxiliary declaration to speed up typechecking.
-/
def forget₂AddCommGroup_preservesLimitsAux : IsLimit ((forget₂ (ModuleCat R) AddCommGrpCat).mapCone (limitCone F)) :=
  letI : Small.{w} (Functor.sections ((F ⋙ forget₂ _ AddCommGrpCat) ⋙ forget _)) :=
    inferInstanceAs <| Small.{w} (Functor.sections (F ⋙ forget (ModuleCat R)))
  AddCommGrpCat.limitConeIsLimit (F ⋙ forget₂ (ModuleCat.{w} R) _ : J ⥤ AddCommGrpCat.{w})

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