English
Let f be a ring homomorphism between rings, and q monic. Then mapping preserves monic-division: map(f)(p /ₘ q) = map(f)(p) /ₘ map(f)(q) and similarly for the remainder: map(p %ₘ q) = map(p) %ₘ map(q).
Русский
Пусть имеется гомоморфизм колец f и мономический q. Тогда отображение сохраняет деление по мономическому и остаток: map(f)(p /ₘ q) = map(f)(p) /ₘ map(f)(q) и map(f)(p %ₘ q) = map(f)(p) %ₘ map(f)(q).
LaTeX
$$$$ \\text{map } f\\left(p /ₘ q\\right) = (\\text{map } f(p)) /ₘ (\\text{map } f(q) ) \\land \\text{map } f\\left(p %ₘ q\\right) = (\\text{map } f(p)) %ₘ (\\text{map } f(q)). $$$$
Lean4
theorem map_mod_divByMonic [Ring S] (f : R →+* S) (hq : Monic q) :
(p /ₘ q).map f = p.map f /ₘ q.map f ∧ (p %ₘ q).map f = p.map f %ₘ q.map f :=
by
nontriviality S
haveI : Nontrivial R := f.domain_nontrivial
have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q) :=
div_modByMonic_unique ((p /ₘ q).map f) _ (hq.map f)
⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div _ hq],
calc
_ ≤ degree (p %ₘ q) := degree_map_le
_ < degree q := (degree_modByMonic_lt _ hq)
_ = _ :=
Eq.symm <| degree_map_eq_of_leadingCoeff_ne_zero _ (by rw [Monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩
exact ⟨this.1.symm, this.2.symm⟩
