English
If f is an injective morphism of monoids with zero, and S is a submonoid of M0 contained in the nonzero-divisors, then the image S.map f is contained in the nonzero-divisors of M0'.
Русский
Пусть f — инъективный морфизм между мономиями с нулём; если S ≤ M0⁰, то S.map f ≤ M0'⁰.
LaTeX
$$map_le_nonZeroDivisors_of_injective [NoZeroDivisors M0'] [MonoidWithZeroHomClass F M0 M0'] (f : F) (hf : Injective f) {S : Submonoid M0} (hS : S ≤ M0⁰) : S.map f ≤ M0'⁰$$
Lean4
theorem map_le_nonZeroDivisors_of_injective [NoZeroDivisors M₀'] [MonoidWithZeroHomClass F M₀ M₀'] (f : F)
(hf : Injective f) {S : Submonoid M₀} (hS : S ≤ M₀⁰) : S.map f ≤ M₀'⁰ :=
by
cases subsingleton_or_nontrivial M₀
· simp [Subsingleton.elim S ⊥]
· refine le_nonZeroDivisors_of_noZeroDivisors ?_
rintro ⟨x, hx, hx0⟩
exact zero_notMem_nonZeroDivisors <| hS <| map_eq_zero_iff f hf |>.mp hx0 ▸ hx
