English
There is a natural homomorphism map from Monoid M to Monoid N carrying units to units, induced by a MonoidHom f : M →* N.
Русский
Существует естественный гомоморфизм map от Моноида M к Моноиду N, отображающий единицы M в единицы N, индуцируемый гомоморфизмом f : M →* N.
LaTeX
$$$\\mathrm{map} : (M \\to^* N) \\to (\\mathrm{Units}\\,M \\to \\mathrm{Units}\,N)$$$
Lean4
/-- The group homomorphism on units induced by a `MonoidHom`. -/
@[to_additive /-- The additive homomorphism on `AddUnit`s induced by an `AddMonoidHom`. -/
]
def map (f : M →* N) : Mˣ →* Nˣ :=
MonoidHom.mk'
(fun u => ⟨f u.val, f u.inv, by rw [← f.map_mul, u.val_inv, f.map_one], by rw [← f.map_mul, u.inv_val, f.map_one]⟩)
fun x y => ext (f.map_mul x y)
