MvPolynomial challenge

Stream: Is there code for X?

[Anatole Dedecker]

Do we have everything necessary to prove this ? What about the version where we evaluate at any point rather than zero (I expect this to be harder since you can't just use docs#MvPolynomial.divMonomial) ?

import Mathlib

open Set RingHom in
theorem MvPolynomial.ker_aeval_zero {R σ : Type*} [CommRing R] :
    ker (eval (0 : σ → R)) = Ideal.span (Set.range .X) := sorry

[Riccardo Brasca]

In my opinion it shouldn't be very hard (but who knows...): one inclusion seems trivial, and for the other one I would use the degree. But this is only a guess

[Junyan Xu]

import Mathlib

open Set RingHom in
theorem MvPolynomial.ker_aeval_zero {R σ : Type*} [CommRing R] :
    ker (eval (0 : σ → R)) = Ideal.span (Set.range .X) := by
  ext; rw [← image_univ, mem_ideal_span_X_image, eval_zero, mem_ker, constantCoeff_eq,
    ← not_mem_support_iff, not_iff_comm]; push_neg
  refine ⟨fun ⟨m, hm, h0⟩ ↦ ?_, fun h ↦ ⟨0, h, fun _ _ ↦ rfl⟩⟩
  convert hm; ext; exact (h0 _ trivial).symm

docs#MvPolynomial.mem_ideal_span_X_image is the key lemma. On the other hand we know docs#MvPolynomial.vanishingIdeal_singleton_isMaximal but apparently don't have the explicit generators.

[Anatole Dedecker]

Thanks!

From my limited experience with this area of mathlib docs#MvPolynomial.mem_ideal_span_X_image doesn't seem very natural (compare with docs#Polynomial.ker_evalRingHom), I guess this is because we don't have docs#divByMonic for MvPolynomial ?

[Junyan Xu]

I think docs#MvPolynomial.mem_ideal_span_X_image should be thought of as a lemma about monomials (not monic polynomials) and there's even a generalization to any monomial ideal: docs#AddMonoidAlgebra.mem_ideal_span_of'_image.

We could prove the analogue of docs#Polynomial.ker_evalRingHom relatively easily using ker_aeval_zero above (shouldn't it be called ker_eval_zero)?

import Mathlib

namespace MvPolynomial

variable {R σ : Type*} [CommRing R] (x : σ → R)

open Set RingHom

theorem ker_eval_zero : ker (eval (0 : σ → R)) = Ideal.span (range X) := by
  ext; rw [← image_univ, mem_ideal_span_X_image, eval_zero, mem_ker, constantCoeff_eq,
    ← not_mem_support_iff, not_iff_comm]; push_neg
  refine ⟨fun ⟨m, hm, h0⟩ ↦ ?_, fun h ↦ ⟨0, h, fun _ _ ↦ rfl⟩⟩
  convert ← hm; ext; exact h0 _ trivial

@[simps!] noncomputable def addCAlgEquiv : MvPolynomial σ R ≃ₐ[R] MvPolynomial σ R :=
  .ofAlgHom (aeval fun i ↦ X i + C (x i)) (aeval fun i ↦ X i - C (x i)) (by ext; simp) (by ext; simp)

theorem aeval_zero_comp_addCAlgEquiv : (aeval (0 : σ → R)).comp (addCAlgEquiv x) = aeval (R := R) x := by
  ext; simp

theorem ker_eval : ker (eval x) = Ideal.span (range fun i ↦ X i - C (x i)) := show ker (aeval x) = _ by
  rw [← aeval_zero_comp_addCAlgEquiv x]
  change ker (comp (aeval 0).toRingHom _) = _
  erw [ker, ← Ideal.comap_comap, ← ker, ker_eval_zero, ← Ideal.map_symm _ (addCAlgEquiv x).toRingEquiv,
    Ideal.map_span, ← range_comp]
  congr!; change (addCAlgEquiv x).symm _ = _; simp

theorem vanishingIdeal_singleton {R} [Field R] (x : σ → R) :
    vanishingIdeal {x} = Ideal.span (range fun i ↦ X i - C (x i)) := by
  ext; rw [mem_vanishingIdeal_singleton_iff, ← ker_eval]; rfl

end MvPolynomial