forget₂AddCommGroupIsEquivalence

English

The forgetful functor from the category of Z-modules to AddCommGrpCat is an equivalence of categories.

Русский

Функтор забывания из Z-модулей в AddCommGrpCat является эквивалентностью категорий.

LaTeX

$$$\text{forget}_{\mathbb{Z}} : \mathbf{Mod}_{\mathbb{Z}} \simeq \mathrm{AddCommGrpCat}$$$

Lean4

noncomputable instance forget₂AddCommGroupIsEquivalence : (forget₂ (ModuleCat ℤ) AddCommGrpCat.{u}).IsEquivalence where

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