English
From a MonoidWithZeroHom φ: Polynomial R → G0 and a witnessing condition hφ, there is a canonical MonoidWithZeroHom RatFunc R → G0 extending φ by sending a fraction to φ(n)/φ(d).
Русский
Из MonoidWithZeroHom φ с условием hφ существует каноническое продолжение до RatFunc: RatFunc(R) → G0, отправляющее дробь n/d в φ(n)/φ(d).
LaTeX
$$$\mathrm{liftMonoidWithZeroHom}\,φ\,hφ: \mathrm{RatFunc}\,R \to \mathrm{G0}$$$
Lean4
/-- Lift a monoid with zero homomorphism `R[X] →*₀ G₀` to a `RatFunc R →*₀ G₀`
on the condition that `φ` maps non-zero-divisors to non-zero-divisors,
by mapping both the numerator and denominator and quotienting them. -/
def liftMonoidWithZeroHom (φ : R[X] →*₀ G₀) (hφ : R[X]⁰ ≤ G₀⁰.comap φ) : RatFunc R →*₀ G₀
where
toFun
f :=
RatFunc.liftOn f (fun p q => φ p / φ q) fun {p q p' q'} hq hq' h =>
by
cases subsingleton_or_nontrivial R
· rw [Subsingleton.elim p q, Subsingleton.elim p' q, Subsingleton.elim q' q]
rw [div_eq_div_iff, ← map_mul, mul_comm p, h, map_mul, mul_comm] <;> exact nonZeroDivisors.ne_zero (hφ ‹_›)
map_one' := by
simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk, OneMemClass.coe_one, map_one,
div_one]
map_mul' x
y := by
obtain ⟨x⟩ := x
obtain ⟨y⟩ := y
cases x using Localization.induction_on
cases y using Localization.induction_on
rw [← ofFractionRing_mul, Localization.mk_mul]
simp only [liftOn_ofFractionRing_mk, div_mul_div_comm, map_mul, Submonoid.coe_mul]
map_zero' := by
simp_rw [← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰), liftOn_ofFractionRing_mk, map_zero, zero_div]
