English
The kernel of the polynomial map map f equals the image under C of the kernel of f, i.e., ker(map f) = Ideal.map C (ker f).
Русский
Ядро отображения многочленов map f равно образу через C ядра f: ker(map f) = Ideal.map C (ker f).
LaTeX
$$$\ker(\mathrm{MvPolynomial.map} f) = \operatorname{Ideal.map} (\mathrm{C}) (\ker f)$$$
Lean4
/-- The push-forward of an ideal `I` of `R` to `MvPolynomial σ R` via inclusion
is exactly the set of polynomials whose coefficients are in `I` -/
theorem mem_map_C_iff {I : Ideal R} {f : MvPolynomial σ R} :
f ∈ (Ideal.map (C : R →+* MvPolynomial σ R) I : Ideal (MvPolynomial σ R)) ↔ ∀ m : σ →₀ ℕ, f.coeff m ∈ I := by
classical
constructor
· intro hf
refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
· intro f hf n
obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
rw [← hx.right, coeff_C]
by_cases h : n = 0
· simpa [h] using hx.left
· simp [Ne.symm h]
· simp
· exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]
· refine fun f g _ hg n => ?_
rw [smul_eq_mul, coeff_mul]
exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)
· intro hf
rw [as_sum f]
suffices ∀ m ∈ f.support, monomial m (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
exact Submodule.sum_mem _ this
intro m _
rw [← mul_one (coeff m f), ← C_mul_monomial]
suffices C (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by exact Ideal.mul_mem_right _ _ this
apply Ideal.mem_map_of_mem _
exact hf m
