English
In an integrally closed base ring, any g dividing f.map can be written as g' mapped times a constant coefficient.
Русский
В интегрально замкнутом основании существует разложение g = g' map * C(leadingCoeff g) для делителя g.
LaTeX
$$$\\text{eq\\_map\\_mul\\_C\\_of\\_dvd}$$$
Lean4
/-- If `K = Frac(R)` and `g : K[X]` divides a monic polynomial with coefficients in `R`, then
`g * (C g.leadingCoeff⁻¹)` has coefficients in `R` -/
theorem eq_map_mul_C_of_dvd [IsIntegrallyClosed R] {f : R[X]} (hf : f.Monic) {g : K[X]}
(hg : g ∣ f.map (algebraMap R K)) : ∃ g' : R[X], g'.map (algebraMap R K) * (C <| leadingCoeff g) = g :=
by
have g_ne_0 : g ≠ 0 := ne_zero_of_dvd_ne_zero (Monic.ne_zero <| hf.map (algebraMap R K)) hg
suffices lem : ∃ g' : R[X], g'.map (algebraMap R K) = g * C g.leadingCoeff⁻¹
by
obtain ⟨g', hg'⟩ := lem
use g'
rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]
have g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ f.map (algebraMap R K) :=
by
rwa [Associated.dvd_iff_dvd_left (show Associated (g * C g.leadingCoeff⁻¹) g from _)]
rw [associated_mul_isUnit_left_iff]
exact isUnit_C.mpr (inv_ne_zero <| leadingCoeff_ne_zero.mpr g_ne_0).isUnit
let algeq :=
(Subalgebra.equivOfEq _ _ <| integralClosure_eq_bot R _).trans
(Algebra.botEquivOfInjective <| IsFractionRing.injective R <| K)
have : (algebraMap R _).comp algeq.toAlgHom.toRingHom = (integralClosure R _).toSubring.subtype := by ext x;
(conv_rhs => rw [← algeq.symm_apply_apply x]); rfl
have H :=
(mem_lifts _).1 (integralClosure.mem_lifts_of_monic_of_dvd_map K hf (monic_mul_leadingCoeff_inv g_ne_0) g_mul_dvd)
refine ⟨map algeq.toAlgHom.toRingHom ?_, ?_⟩
· use! Classical.choose H
· rw [map_map, this]
exact Classical.choose_spec H
