English
If f : M →* N and g : M → Nˣ satisfy g x underlying equals f x, then liftRight f g h is a monoid hom from M to Units N. It lifts f, matching the unit-valued map g.
Русский
Если f : M →* N и g : M → Nˣ удовлетворяют условию, что подлежащие значения равны f x, то liftRight f g h задаёт моноид-гомоморфизм M → Units N, поднимая f в единицы.
LaTeX
$$$\\mathrm{liftRight}(f,g,h) : M \\to^* (N)^{\\times}$$$
Lean4
/-- If a map `g : M → Nˣ` agrees with a homomorphism `f : M →* N`, then
this map is a monoid homomorphism too. -/
@[to_additive /-- If a map `g : M → AddUnits N` agrees with a homomorphism `f : M →+ N`, then this map
is an AddMonoid homomorphism too. -/
]
def liftRight (f : M →* N) (g : M → Nˣ) (h : ∀ x, ↑(g x) = f x) : M →* Nˣ
where
toFun := g
map_one' := by ext; rw [h 1]; exact f.map_one
map_mul' x y := Units.ext <| by simp only [h, val_mul, f.map_mul]
