forget₂AddCommGroup_preservesLimits

English

Auxiliary declaration providing an IsLimit for the forget₂ AddCommGroup cone after forgetting RingCat.

Русский

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

LaTeX

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

Lean4

instance forget₂AddCommGroup_preservesLimits : PreservesLimits (forget₂ RingCat AddCommGrpCat.{u}) :=
  RingCat.forget₂AddCommGroup_preservesLimitsOfSize.{u, u}

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