instReflectsIsomorphismsForget — Mathlib

English

The forget₂ functor from ModuleCat to AddCommGrpCat reflects isomorphisms as well; isomorphisms in ModuleCat correspond to isomorphisms at the level of underlying abelian groups.

Русский

Forget₂ отражает изоморфизмы; изоморфизм в ModuleCat эквивалентен изоморфизму на уровне абелевых групп.

LaTeX

$$$\text{forget}_2: \mathrm{ModuleCat}(R) \to \mathrm{AddCommGrpCat}$ reflects isomorphisms.$$

Lean4

instance : (forget (ModuleCat.{v} R)).ReflectsIsomorphisms where
  reflects f
    _ :=
    (inferInstance :
      IsIso
        ((LinearEquiv.mk f.hom (asIso ((forget (ModuleCat R)).map f)).toEquiv.invFun (Equiv.left_inv _)
              (Equiv.right_inv _)).toModuleIso).hom)

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