forget₂_map_homMk — Mathlib

English

The forgetful functor from ModuleCat R to AddCommGrpCat (and its forget₂ variant to AddCommGrpCat) reflects isomorphisms; i.e., if the underlying map is an isomorphism, then the original ModuleCat morphism is an isomorphism.

Русский

Забывающий функтор из ModuleCat R в AddCommGrpCat (и его forget₂) отражает изоморфизмы; если оснóвное отображение является изоморфизмом, то исходный морфизм в ModuleCat тоже изоморфизм.

LaTeX

$$$\text{Forget}(f) \text{ изоморфизм }\Rightarrow f \text{ изоморфизм in ModuleCat}$$$

Lean4

theorem forget₂_map_homMk : (forget₂ (ModuleCat R) AddCommGrpCat).map (homMk φ hφ) = φ :=
  rfl

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