feat(ring_theory/polynomial/basic): Isomorphism between polynomials o…

…ver a quotient and quotient over polynomials (#3847)

The main statement is `polynomial_quotient_equiv_quotient_polynomial`, which gives that If `I` is an ideal of `R`, then the ring polynomials over the quotient ring `I.quotient` is isomorphic to the quotient of `polynomial R` by the ideal `map C I`.

Also, `mem_map_C_iff` shows that `map C I` contains exactly the polynomials whose coefficients all lie in `I`

src/ring_theory/polynomial/basic.lean

@@ -178,6 +178,88 @@ variables {R : Type u} {σ : Type v} [comm_ring R]
 namespace ideal
 open polynomial
 
+/-- The push-forward of an ideal `I` of `R` to `polynomial R` via inclusion
+ is exactly the set of polynomials whose coefficients are in `I` -/
+theorem mem_map_C_iff {I : ideal R} {f : polynomial R} :
+  f ∈ (ideal.map C I : ideal (polynomial R)) ↔ ∀ n : ℕ, f.coeff n ∈ 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 [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 ← sum_monomial_eq f,
+    refine (map C I : ideal (polynomial R)).sum_mem (λ n hn, _),
+    simp [single_eq_C_mul_X],
+    rw mul_comm,
+    exact (map C I : ideal (polynomial R)).smul_mem _ (mem_map_of_mem (hf n)) }
+end
+
+lemma quotient_map_C_eq_zero {I : ideal R} :
+  ∀ a ∈ I, ((quotient.mk (map C I : ideal (polynomial R))).comp C) a = 0 :=
+begin
+  intros a ha,
+  rw [ring_hom.comp_apply, quotient.eq_zero_iff_mem],
+  exact mem_map_of_mem ha,
+end
+
+lemma eval₂_C_mk_eq_zero {I : ideal R} :
+  ∀ f ∈ (map C I : ideal (polynomial R)), eval₂_ring_hom (C.comp (quotient.mk I)) X f = 0 :=
+begin
+  intros a ha,
+  rw ← sum_monomial_eq a,
+  dsimp,
+  rw eval₂_sum (C.comp (quotient.mk I)) a monomial X,
+  refine finset.sum_eq_zero (λ n hn, _),
+  dsimp,
+  rw eval₂_monomial (C.comp (quotient.mk I)) X,
+  refine mul_eq_zero_of_left (polynomial.ext (λ m, _)) (X ^ n),
+  erw coeff_C,
+  by_cases h : m = 0,
+  { simpa [h] using quotient.eq_zero_iff_mem.2 ((mem_map_C_iff.1 ha) n) },
+  { simp [h] }
+end
+
+/-- If `I` is an ideal of `R`, then the ring polynomials over the quotient ring `I.quotient` is
+isomorphic to the quotient of `polynomial R` by the ideal `map C I`,
+where `map C I` contains exactly the polynomials whose coefficients all lie in `I` -/
+def polynomial_quotient_equiv_quotient_polynomial {I : ideal R} :
+  polynomial (I.quotient) ≃+* (map C I : ideal (polynomial R)).quotient :=
+{ to_fun := eval₂_ring_hom
+    (quotient.lift I ((quotient.mk (map C I : ideal (polynomial R))).comp C) quotient_map_C_eq_zero)
+    ((quotient.mk (map C I : ideal (polynomial R)) X)),
+  inv_fun := quotient.lift (map C I : ideal (polynomial R))
+    (eval₂_ring_hom (C.comp (quotient.mk I)) X) eval₂_C_mk_eq_zero,
+  map_mul' := λ f g, by simp,
+  map_add' := λ f g, by simp,
+  left_inv := begin
+    intro f,
+    apply polynomial.induction_on' f,
+    { simp_intros p q hp hq,
+      rw [hp, hq] },
+    { rintros n ⟨x⟩,
+      simp [monomial_eq_smul_X, C_mul'] }
+  end,
+  right_inv := begin
+    rintro ⟨f⟩,
+    apply polynomial.induction_on' f,
+    { simp_intros p q hp hq,
+      rw [hp, hq] },
+    { intros n a,
+      simp [monomial_eq_smul_X, ← C_mul' a (X ^ n)] },
+  end,
+}
+
 /-- Transport an ideal of `R[X]` to an `R`-submodule of `R[X]`. -/
 def of_polynomial (I : ideal (polynomial R)) : submodule R (polynomial R) :=
 { carrier := I.carrier,