feat(ring_theory/polynomial/basic): add quotient_equiv_quotient_mv_po…

…lynomial (#6287)

I've added `quotient_equiv_quotient_mv_polynomial` that says that `(R/I)[x_i] ≃+* (R[x_i])/I` where `I` is an ideal of `R`. I've included also a version for `R`-algebras. The proof is very similar to the case of (one variable) polynomials.

src/ring_theory/polynomial/basic.lean

@@ -761,6 +761,126 @@ begin
   simp only [monomial_eq, ϕ.map_pow, ϕ.map_prod, ϕ.comp_apply, ϕ.map_mul, finsupp.prod_pow],
 end
 
+lemma quotient_map_C_eq_zero {I : ideal R} {i : R} (hi : i ∈ I) :
+  (ideal.quotient.mk (ideal.map C I : ideal (mv_polynomial σ R))).comp C i = 0 :=
+begin
+  simp only [function.comp_app, ring_hom.coe_comp, ideal.quotient.eq_zero_iff_mem],
+  exact ideal.mem_map_of_mem hi
+end
+
+/-- If every coefficient of a polynomial is in an ideal `I`, then so is the polynomial itself,
+multivariate version. -/
+lemma mem_ideal_of_coeff_mem_ideal (I : ideal (mv_polynomial σ R)) (p : mv_polynomial σ R)
+  (hcoe : ∀ (m : σ →₀ ℕ), p.coeff m ∈ I.comap C) : p ∈ I :=
+begin
+  rw as_sum p,
+  suffices : ∀ m ∈ p.support, monomial m (mv_polynomial.coeff m p) ∈ I,
+  { exact submodule.sum_mem I this },
+  intros m hm,
+  rw [← mul_one (coeff m p), ← C_mul_monomial],
+  suffices : C (coeff m p) ∈ I,
+  { exact ideal.mul_mem_right I (monomial m 1) this },
+  simpa [ideal.mem_comap] using hcoe m
+end
+
+/-- 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` -/
+theorem mem_map_C_iff {I : ideal R} {f : mv_polynomial σ R} :
+  f ∈ (ideal.map C I : ideal (mv_polynomial σ R)) ↔ ∀ (m : σ →₀ ℕ), f.coeff m ∈ I :=
+begin
+  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 (n = 0),
+      { simpa [h] using hx.left },
+      { simp [ne.symm 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 as_sum f,
+    suffices : ∀ m ∈ f.support, monomial m (coeff m f) ∈
+      (ideal.map C I : ideal (mv_polynomial σ R)),
+    { exact submodule.sum_mem _ this },
+    intros m hm,
+    rw [← mul_one (coeff m f), ← C_mul_monomial],
+    suffices : C (coeff m f) ∈ (ideal.map C I : ideal (mv_polynomial σ R)),
+    { exact ideal.mul_mem_right _ _ this },
+    apply ideal.mem_map_of_mem _,
+    exact hf m }
+end
+
+lemma eval₂_C_mk_eq_zero {I : ideal R} {a : mv_polynomial σ R}
+  (ha : a ∈ (ideal.map C I : ideal (mv_polynomial σ R))) :
+  eval₂_hom (C.comp (ideal.quotient.mk I)) X a = 0 :=
+begin
+  rw as_sum a,
+  rw [coe_eval₂_hom, eval₂_sum],
+  refine finset.sum_eq_zero (λ n hn, _),
+  simp only [eval₂_monomial, function.comp_app, ring_hom.coe_comp],
+  refine mul_eq_zero_of_left _ _,
+  suffices : coeff n a ∈ I,
+  { rw [← @ideal.mk_ker R _ I, ring_hom.mem_ker] at this,
+    simp only [this, C_0] },
+  exact mem_map_C_iff.1 ha n
+end
+
+/-- If `I` is an ideal of `R`, then the ring `mv_polynomial σ I.quotient` is isomorphic to the
+quotient of `mv_polynomial σ R` by the ideal generated by `I`. -/
+def quotient_equiv_quotient_mv_polynomial (I : ideal R) :
+  mv_polynomial σ (I.quotient) ≃+* (ideal.map C I : ideal (mv_polynomial σ R)).quotient :=
+{ to_fun := eval₂_hom (ideal.quotient.lift I ((ideal.quotient.mk (ideal.map C I : ideal
+    (mv_polynomial σ R))).comp C) (λ i hi, quotient_map_C_eq_zero hi))
+    (λ i, ideal.quotient.mk (ideal.map C I : ideal (mv_polynomial σ R)) (X i)),
+  inv_fun := ideal.quotient.lift (ideal.map C I : ideal (mv_polynomial σ R))
+    (eval₂_hom (C.comp (ideal.quotient.mk I)) X) (λ a ha, eval₂_C_mk_eq_zero ha),
+  map_mul' := λ f g, by simp,
+  map_add' := λ f g, by simp,
+  left_inv := begin
+    intro f,
+    apply induction_on f,
+    { rintro ⟨r⟩,
+      rw [coe_eval₂_hom, eval₂_C],
+      simp only [eval₂_hom_eq_bind₂, submodule.quotient.quot_mk_eq_mk, ideal.quotient.lift_mk,
+        ideal.quotient.mk_eq_mk, bind₂_C_right, ring_hom.coe_comp] },
+    { simp_intros p q hp hq,
+      rw [hp, hq] },
+    { simp_intros p i hp,
+      simp only [hp, eval₂_hom_eq_bind₂, coe_eval₂_hom, ideal.quotient.lift_mk, bind₂_X_right,
+        eval₂_mul, ring_hom.map_mul, eval₂_X] }
+  end,
+  right_inv := begin
+    rintro ⟨f⟩,
+    apply induction_on f,
+    { intros r,
+      simp only [submodule.quotient.quot_mk_eq_mk, ideal.quotient.lift_mk, ideal.quotient.mk_eq_mk,
+        ring_hom.coe_comp, eval₂_hom_C] },
+    { simp_intros p q hp hq,
+      rw [hp, hq] },
+    { simp_intros p i hp,
+      simp only [hp] }
+  end,
+}
+
+/-- If `I` is an ideal of `R`, then the ring `mv_polynomial σ I.quotient` is isomorphic,
+as `R`-algebra, to the quotient of `mv_polynomial σ R` by the ideal generated by `I`. -/
+def quotient_alg_equiv_quotient_mv_polynomial (I : ideal R) :
+  algebra.comap R I.quotient (mv_polynomial σ (I.quotient)) ≃ₐ[R]
+  (ideal.map C I : ideal (mv_polynomial σ R)).quotient :=
+  { commutes' := begin
+    intro r,
+    change (algebra_map R (algebra.comap R I.quotient (mv_polynomial σ (I.quotient)))) r with
+      C (ideal.quotient.mk I r),
+    simpa [algebra_map, quotient_equiv_quotient_mv_polynomial],
+    end,
+    ..quotient_equiv_quotient_mv_polynomial I,
+  }
+
 end mv_polynomial
 
 namespace polynomial