The kernel of a mapped polynomial is the map of the kernel

Stream: Is there code for X?

[Eric Wieser]

Do we have the fact that (map f : mv_polynomial σ R →+* mv_polynomial σ S).ker = f.ker.map C?

I was able to show it with:

import data.mv_polynomial.basic
import ring_theory.ideal.operations

variables {σ R S : Type*} [comm_ring R] [comm_ring S]

open mv_polynomial

/-- The push-forward of an ideal `I` of `R` to `mv_polynomial σ R` via inclusion
is exactly the set of polynomials whose coefficients are in `I`.#check

This is the multivariate version of `ideal.mem_map_C_iff`. -/
theorem _root_.ideal.mem_map_mv_polynomial_C_iff {I : ideal R} {f : mv_polynomial σ R} :
  f ∈ (ideal.map C I : ideal (mv_polynomial σ R)) ↔ ∀ n : σ →₀ ℕ, f.coeff n ∈ I :=
begin
  -- this proof is just a copy-paste of `ideal.mem_map_C_iff` with minor adjustments
  classical,
  split,
  { intros hf,
    apply submodule.span_induction hf,
    { intros f hf n,
      cases (set.mem_image _ _ _).mp hf with x hx,
      rw [← hx.right, coeff_C],
      by_cases (0 = n),
      { simpa [h] using hx.left },
      { simp [h] } },
    { simp },
    { exact λ f g hf hg n, by simp [I.add_mem (hf n) (hg n)] },
    { refine λ f g hg n, _,
      rw [smul_eq_mul, coeff_mul],
      exact I.sum_mem (λ c hc, I.smul_mem (f.coeff c.fst) (hg c.snd)) } },
  { intros hf,
    rw ←f.support_sum_monomial_coeff,
    refine (I.map C : ideal (mv_polynomial σ R)).sum_mem (λ n hn, _),
    rw [←mul_one (coeff n f), ←C_mul_monomial],
    rw mul_comm,
    exact (I.map C : ideal (mv_polynomial σ R)).mul_mem_left _ (ideal.mem_map_of_mem _ (hf n)) }
end

lemma _root_.mv_polynomial.ker_map (f : R →+* S) :
  (map f : mv_polynomial σ R →+* mv_polynomial σ S).ker = f.ker.map C :=
begin
  ext,
  rw [ideal.mem_map_mv_polynomial_C_iff, ring_hom.mem_ker, mv_polynomial.ext_iff],
  simp_rw [coeff_map, coeff_zero, ring_hom.mem_ker],
end

but I'm not sure where a good home for this is

[Eric Wieser]

Given I need it in ring_theory.finiteness, my choices are only:

• ring_theory.adjoin.fg
• ring_theory.adjoin.polynomial
• ring_theory.algebra_tower
• ring_theory.polynomial.basic

# script to answer the above
import networkx as nx
import requests
import io

with requests.get("https://leanprover-community.github.io/mathlib_docs/import.gexf") as r:
    g = nx.read_gexf(io.StringIO(r.text))

ok = (
    nx.ancestors(g, 'mathlib:data.mv_polynomial.basic') &
    nx.ancestors(g, 'mathlib:ring_theory.ideal.basic') &
    nx.descendants(g, 'mathlib:ring_theory.finiteness'))
print(ok)

[Johan Commelin]

I think ring_theory.polynomial.basic is fine.
(You have a #check embedded in your docstring.)

[Eric Wieser]

Oh, we already have docs#mv_polynomial.mem_map_C_iff in that file!

[Eric Wieser]

I couldn't find it because the other lemma is called docs#ideal.mem_map_C_iff

[Eric Wieser]

#10160