English
The push-forward of an ideal I in R to R[X] along the inclusion map C: R → R[X] consists exactly of those polynomials all of whose coefficients lie in I.
Русский
Образообразование идеала I по включению C: R → R[X] совпадает с множеством всех многочленов, коэффициенты которых лежат в I.
LaTeX
$$$f \\in \\mathrm{map}(\\mathcal{C},I) \\iff \\forall n, \\operatorname{coeff}(f,n) \\in I$$$
Lean4
/-- The push-forward of an ideal `I` of `R` to `R[X]` via inclusion
is exactly the set of polynomials whose coefficients are in `I` -/
theorem mem_map_C_iff {I : Ideal R} {f : R[X]} :
f ∈ (Ideal.map (C : R →+* R[X]) I : Ideal R[X]) ↔ ∀ n : ℕ, f.coeff n ∈ I :=
by
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 [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 [← sum_monomial_eq f]
refine (I.map C : Ideal R[X]).sum_mem fun n _ => ?_
simp only [← C_mul_X_pow_eq_monomial]
rw [mul_comm]
exact (I.map C : Ideal R[X]).mul_mem_left _ (mem_map_of_mem _ (hf n))
