forget₂_addCommGrp_essSurj — Mathlib

English

The forgetful functor from the category of Z-modules to AddCommGrpCat is essentially surjective: every object A in AddCommGrpCat is isomorphic to the underlying abelian group of some Z-module.

Русский

У forget₂ из категории Z-модулей в AddCommGrpCat является фактически сурьективным: каждое объект AddCommGrpCat изоморфен базовой абелевой группе какого-либо Z-модуля.

LaTeX

$$$\forall A : \mathrm{AddCommGrpCat},\; \exists M : \mathrm{ModuleCat}_\mathbb{Z},\; \mathrm{Forget}(M) \cong A$$$

Lean4

/-- The forgetful functor from `ℤ` modules to `AddCommGrpCat` is essentially surjective. -/
instance forget₂_addCommGrp_essSurj : (forget₂ (ModuleCat ℤ) AddCommGrpCat.{u}).EssSurj where
  mem_essImage
    A :=
    ⟨ModuleCat.of ℤ A,
      ⟨{  hom := 𝟙 A
          inv := 𝟙 A }⟩⟩

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