forget₂AddCommGroupPreservesLimitsAux

English

An auxiliary statement asserting that the limit cone in RingCat, when mapped to AddCommGroup via forget₂, remains a limit cone.

Русский

Дополнительное предложение о том, что предельный конус RingCat, отображённый в AddCommGroup через forget₂, остаётся пределом.

LaTeX

$$$\text{IsLimit}((\mathrm{forget}\!_{RingCat}^{AddCommGrpCat})\circ (\text{limitCone } F))$$$

Lean4

/-- An auxiliary declaration to speed up typechecking.
-/
def forget₂AddCommGroupPreservesLimitsAux :
    IsLimit ((forget₂ RingCat.{u} AddCommGrpCat).mapCone (limitCone.{v, u} F)) :=
  by
  let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ RingCat.{u} AddCommGrpCat.{u}) ⋙ forget _)) :=
    inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
  apply AddCommGrpCat.limitConeIsLimit.{v, u} _

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