English
There is a specialized version mapRingHom of map when restricting to ring homomorphisms between polynomial rings, giving a RatFunc-ring homomorphism under appropriate hypotheses.
Русский
Существует версия mapRingHom изобразования map на случай гомоморфизмов колец между кольцами многочленов, образующая гомоморфизм колец RatFunc при соответствующих условиях.
LaTeX
$$$\mathrm{mapRingHom}:\, \mathrm{RatFunc}\,R \to \mathrm{RatFunc}\,S$$$
Lean4
/-- Lift a ring homomorphism that maps polynomials `φ : R[X] →+* S[X]`
to a `RatFunc R →+* RatFunc S`,
on the condition that `φ` maps non-zero-divisors to non-zero-divisors,
by mapping both the numerator and denominator and quotienting them. -/
def mapRingHom [RingHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap φ) : RatFunc R →+* RatFunc S :=
{
map φ
hφ with
map_zero' := by
simp_rw [MonoidHom.toFun_eq_coe, ← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰), ←
Localization.mk_zero (1 : S[X]⁰), map_apply_ofFractionRing_mk, map_zero, Localization.mk_eq_mk',
IsLocalization.mk'_zero]
map_add' := by
rintro ⟨x⟩ ⟨y⟩
induction x using Localization.induction_on
induction y using Localization.induction_on
·
simp only [← ofFractionRing_add, Localization.add_mk, map_add, map_mul, MonoidHom.toFun_eq_coe,
map_apply_ofFractionRing_mk, Submonoid.coe_mul,
-- We have to specify `S[X]⁰` to `mk_mul_mk`, otherwise it will try to rewrite
-- the wrong occurrence.
Submonoid.mk_mul_mk S[X]⁰] }
