feat(ring_theory/finiteness): add mv_polynomial_of_finite_presentation (#6512)

Add `mv_polynomial_of_finite_presentation`: the polynomial ring over a finitely presented algebra is finitely presented.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: riccardobrasca

src/ring_theory/finiteness.lean

@@ -277,6 +277,17 @@ lemma of_surjective {f : A →ₐ[R] B} (hf : function.surjective f) (hker : f.t
   (hfp : finite_presentation R A) : finite_presentation R B :=
 equiv (quotient hker hfp) (ideal.quotient_ker_alg_equiv_of_surjective hf)
 
+
+lemma iff : finite_presentation R A ↔
+  ∃ n (I : ideal (_root_.mv_polynomial (fin n) R)) (e : I.quotient ≃ₐ[R] A), I.fg :=
+begin
+  refine ⟨λ h,_, λ h, _⟩,
+  { obtain ⟨n, f, hf⟩ := h,
+    use [n, f.to_ring_hom.ker, ideal.quotient_ker_alg_equiv_of_surjective hf.1, hf.2] },
+  { obtain ⟨n, I, e, hfg⟩ := h,
+    exact equiv (quotient hfg (mv_polynomial R _)) e }
+end
+
 /-- An algebra is finitely presented if and only if it is a quotient of a polynomial ring whose
 variables are indexed by a fintype by a finitely generated ideal. -/
 lemma iff_quotient_mv_polynomial' : finite_presentation R A ↔ ∃ (ι : Type u_2) [fintype ι]
@@ -301,6 +312,26 @@ begin
     exact ring_hom.ker_coe_equiv (equiv.symm.to_ring_equiv), }
 end
 
+/-- If `A` is a finitely presented `R`-algebra, then `mv_polynomial (fin n) A` is finitely presented
+as `R`-algebra. -/
+lemma mv_polynomial_of_finite_presentation (hfp : finite_presentation R A) (ι : Type*)
+  [fintype ι] : finite_presentation R (_root_.mv_polynomial ι A) :=
+begin
+  obtain ⟨n, e⟩ := fintype.exists_equiv_fin ι,
+  replace e := (mv_polynomial.rename_equiv A (nonempty.some e)).restrict_scalars R,
+  refine equiv _ e.symm,
+  obtain ⟨m, I, e, hfg⟩ := iff.1 hfp,
+  refine equiv _ (mv_polynomial.map_alg_equiv (fin n) e),
+  letI : is_scalar_tower R (_root_.mv_polynomial (fin m) R)
+    (@ideal.map _ (_root_.mv_polynomial (fin n) (_root_.mv_polynomial (fin m) R))
+    _ _ mv_polynomial.C I).quotient := is_scalar_tower.comap,
+  refine equiv _ ((@mv_polynomial.quotient_equiv_quotient_mv_polynomial
+    _ (fin n) _ I).restrict_scalars R).symm,
+  refine quotient (submodule.map_fg_of_fg I hfg _) _,
+  refine equiv _ (mv_polynomial.sum_alg_equiv _ _ _),
+  exact equiv (mv_polynomial R (fin (n + m))) (mv_polynomial.rename_equiv R sum_fin_sum_equiv).symm
+end
+
 end finite_presentation
 
 end algebra

src/ring_theory/noetherian.lean

@@ -201,6 +201,30 @@ begin
     { exact zero_smul _ }, { exact λ _ _ _, add_smul _ _ _ } }
 end
 
+/-- The image of a finitely generated ideal is finitely generated. -/
+lemma map_fg_of_fg {R S : Type*} [comm_ring R] [comm_ring S] (I : ideal R) (h : I.fg) (f : R →+* S)
+  : (I.map f).fg :=
+begin
+  obtain ⟨X, hXfin, hXgen⟩ := fg_def.1 h,
+  apply fg_def.2,
+  refine ⟨set.image f X, finite.image ⇑f hXfin, _⟩,
+  rw [ideal.map, ideal.span, ← hXgen],
+  refine le_antisymm (submodule.span_mono (image_subset _ ideal.subset_span)) _,
+  rw [submodule.span_le, image_subset_iff],
+  intros i hi,
+  refine submodule.span_induction hi (λ x hx, _) _ (λ x y hx hy, _) (λ r x hx, _),
+  { simp only [mem_coe, mem_preimage],
+    suffices : f x ∈ f '' X, { exact ideal.subset_span this },
+    exact mem_image_of_mem ⇑f hx },
+  { simp only [mem_coe, ring_hom.map_zero, mem_preimage, zero_mem] },
+  { simp only [mem_coe, mem_preimage] at hx hy,
+    simp only [ring_hom.map_add, mem_coe, mem_preimage],
+    exact submodule.add_mem _ hx hy },
+  { simp only [mem_coe, mem_preimage] at hx,
+    simp only [algebra.id.smul_eq_mul, mem_coe, mem_preimage, ring_hom.map_mul],
+    exact submodule.smul_mem _ _ hx }
+end
+
 /-- The kernel of the composition of two linear maps is finitely generated if both kernels are and
 the first morphism is surjective. -/
 lemma fg_ker_comp {R M N P : Type*} [ring R] [add_comm_group M] [module R M]