English
Let M, N be monoids and f : M →* N a monoid homomorphism. Suppose g : M → Nˣ is a function into the unit group of N and h is a choice of lifts satisfying ↑(g x) = f x for all x ∈ M. Then for every x ∈ M, the product f(x) times the inverse of liftRight f g h x equals the identity in N.
Русский
Пусть M, N — моноиды, a приведёт в моноидомоморфизм f : M →* N. Пусть g : M → Nˣ — функция в группу единиц N, и пусть есть выбор подстановок h с условием ↑(g x) = f x для всех x ∈ M. Тогда для каждого x ∈ M выполняется равенство f(x) · (liftRight f g h x)⁻¹ = 1 в N.
LaTeX
$$$f(x) \\cdot (\\operatorname{liftRight} f g h\\, x)^{-1} = 1 \\quad\\text{for all } x, $$$
Lean4
@[to_additive (attr := simp)]
theorem mul_liftRight_inv {f : M →* N} {g : M → Nˣ} (h : ∀ x, ↑(g x) = f x) (x) : f x * ↑(liftRight f g h x)⁻¹ = 1 := by
rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]
