English
Given a monoid homomorphism φ that maps non-zero-divisors to non-zero-divisors, there is a functorial lift to RatFunc: a ring homomorphism map φ: RatFunc(R) → RatFunc(S) which sends a fraction n/d to φ(n)/φ(d).
Русский
При наличии гомоморизма мономодов φ, сохраняющего нулевые делители, существует каноническое отображение RatFunc(R) → RatFunc(S), переводя дробь n/d в φ(n)/φ(d).
LaTeX
$$$\mathrm{map}:\,\mathrm{RatFunc}\,R \to \mathrm{RatFunc}\,S$$$
Lean4
/-- Lift a monoid 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 map [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap φ) : RatFunc R →* RatFunc S
where
toFun
f :=
RatFunc.liftOn f (fun n d => if h : φ d ∈ S[X]⁰ then ofFractionRing (Localization.mk (φ n) ⟨φ d, h⟩) else 0)
fun {p q p' q'} hq hq' h =>
by
simp only [Submonoid.mem_comap.mp (hφ hq), Submonoid.mem_comap.mp (hφ hq'), dif_pos, ofFractionRing.injEq,
Localization.mk_eq_mk_iff]
refine Localization.r_of_eq ?_
simpa only [map_mul] using congr_arg φ h
map_one' := by
simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk, OneMemClass.coe_one, map_one,
OneMemClass.one_mem, dite_true, ofFractionRing.injEq, Localization.mk_one, Localization.mk_eq_monoidOf_mk',
Submonoid.LocalizationMap.mk'_self]
map_mul' x
y := by
obtain ⟨x⟩ := x; obtain ⟨y⟩ := y
cases x using Localization.induction_on with
| _ pq
cases y using Localization.induction_on with
| _ p'q'
obtain ⟨p, q⟩ := pq
obtain ⟨p', q'⟩ := p'q'
have hq : φ q ∈ S[X]⁰ := hφ q.prop
have hq' : φ q' ∈ S[X]⁰ := hφ q'.prop
have hqq' : φ ↑(q * q') ∈ S[X]⁰ := by simpa using Submonoid.mul_mem _ hq hq'
simp_rw [← ofFractionRing_mul, Localization.mk_mul, liftOn_ofFractionRing_mk, dif_pos hq, dif_pos hq', dif_pos hqq',
← ofFractionRing_mul, Submonoid.coe_mul, map_mul, Localization.mk_mul, Submonoid.mk_mul_mk]
