forget₂CommSemiRingPreservesLimitsAux

English

Auxiliary IsLimit for the forget₂ CommRingCat CommSemiRingCat cone with limitCone F.

Русский

Вспомогательное утверждение о том, что конус забывания удовлетворяет свойству IsLimit.

LaTeX

$$$\text{forget}_2\text{CommSemiRingPreservesLimitsAux} : \text{IsLimit}((\mathrm{forget}\,CommRingCat\,CommSemiRingCat)\circ \text{limitCone }F)$$$

Lean4

/-- An auxiliary declaration to speed up typechecking.
-/
def forget₂CommSemiRingPreservesLimitsAux : IsLimit ((forget₂ CommRingCat CommSemiRingCat).mapCone (limitCone F)) :=
  by
  let _ : Small.{u} ((F ⋙ forget₂ _ CommSemiRingCat) ⋙ forget _).sections :=
    inferInstanceAs <| Small.{u} (F ⋙ forget _).sections
  apply CommSemiRingCat.limitConeIsLimit (F ⋙ forget₂ CommRingCat CommSemiRingCat.{u})

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