English
If M₀ is a nontrivial monoid, then any MonoidWithZero hom f from GroupWithZero G₀ to M₀ is a local hom.
Русский
Если M₀ небезразличный однообразный моной, то любой гомоморфизм MonoidWithZero из GroupWithZero в M₀ является локальным гомоморфизмом.
LaTeX
$$$\\text{GroupWithZero } G_0 \\\\Rightarrow \\text{MonoidWithZero } M_0 \\\\Rightarrow \\text{IsLocalHom } f$ (при допущении nontrivial $M_0$)$$
Lean4
theorem isLocalHom_of_exists_map_ne_one [FunLike F G₀ M] [MonoidHomClass F G₀ M] {f : F} (hf : ∃ x : G₀, f x ≠ 1) :
IsLocalHom f where
map_nonunit a
h := by
rcases eq_or_ne a 0 with (rfl | h)
· obtain ⟨t, ht⟩ := hf
refine (ht ?_).elim
have := map_mul f t 0
rw [← one_mul (f (t * 0)), mul_zero] at this
exact (h.mul_right_cancel this).symm
· exact ⟨⟨a, a⁻¹, mul_inv_cancel₀ h, inv_mul_cancel₀ h⟩, rfl⟩
