instReflectsIsomorphismsAddCommGrpCatForget₂

English

The forgetful functor forget from ModuleCat R to Type (or AddCommGrpCat) reflects isomorphisms; explicit in particular for the forget₂ variant.

Русский

Забывающий функтор отражает изоморфизмы; в частности для forget₂.

LaTeX

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

Lean4

instance : (forget₂ (ModuleCat.{v} R) AddCommGrpCat.{v}).ReflectsIsomorphisms where
  reflects f
    _ :=
    by
    have : IsIso ((forget _).map f) :=
      by
      change IsIso ((forget _).map ((forget₂ _ AddCommGrpCat).map f))
      infer_instance
    apply isIso_of_reflects_iso _ (forget _)

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