English
If f: R → S is integral and injective, then f is a local hom.
Русский
Если f: R → S интегральна и инъективна, то f является локальным гомоморфизмом.
LaTeX
$$$\\text{IsIntegral}(f) \\wedge \\text{Injective}(f) \\Rightarrow \\text{IsLocalHom}(f)$$$
Lean4
theorem isLocalHom {f : R →+* S} (hf : f.IsIntegral) (inj : Function.Injective f) : IsLocalHom f where
map_nonunit a
ha := by
-- `f a` is invertible in `S`, and we need to show that `(f a)⁻¹` is of the form `f b`.
-- Let `p : R[X]` be monic with root `(f a)⁻¹`,
obtain ⟨p, p_monic, hp⟩ :=
hf
(ha.unit⁻¹ : _)
-- and `q` be `p` with coefficients reversed (so `q(a) = q'(a) * a + 1`).
-- We have `q(a) = 0`, so `-q'(a)` is the inverse of `a`.
refine isUnit_of_mul_eq_one _ (-p.reverse.divX.eval a) ?_
nth_rewrite 1 [mul_neg, ← eval_X (x := a), ← eval_mul, ← p_monic, ← coeff_zero_reverse, ← add_eq_zero_iff_neg_eq, ←
eval_C (a := p.reverse.coeff 0), ← eval_add, X_mul_divX_add, ← (injective_iff_map_eq_zero' _).mp inj, ← eval₂_hom]
rwa [← eval₂_reverse_eq_zero_iff] at hp
