feat(RingTheory/Finiteness): a finite and finitely presented algebra is finitely presented (#29781)

We show that if `S` is finite as a module over `R` and finitely presented as an algebra over `R`, then it is finitely presented as a module over `R`.

Author: chrisflav

Mathlib.lean

@@ -5612,6 +5612,7 @@ import Mathlib.RingTheory.Finiteness.Defs
 import Mathlib.RingTheory.Finiteness.Finsupp
 import Mathlib.RingTheory.Finiteness.Ideal
 import Mathlib.RingTheory.Finiteness.Lattice
+import Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
 import Mathlib.RingTheory.Finiteness.Nakayama
 import Mathlib.RingTheory.Finiteness.Nilpotent
 import Mathlib.RingTheory.Finiteness.Prod

Mathlib/Algebra/Algebra/Tower.lean

@@ -202,6 +202,25 @@ theorem restrictScalars_injective :
     Function.Injective (restrictScalars R : (A →ₐ[S] B) → A →ₐ[R] B) := fun _ _ h =>
   AlgHom.ext (AlgHom.congr_fun h :)
 
+section
+
+variable {R}
+
+/-- Any `f : A →ₐ[R] B` is also an `R ⧸ I`-algebra homomorphism if the `R`-algebra structure on
+`A` and `B` factors via `R ⧸ I`. -/
+@[simps! apply]
+def extendScalarsOfSurjective (h : Function.Surjective (algebraMap R S))
+    (f : A →ₐ[R] B) : A →ₐ[S] B where
+  toRingHom := f
+  commutes' := by simp [h.forall, ← IsScalarTower.algebraMap_apply]
+
+@[simp]
+lemma restrictScalars_extendScalarsOfSurjective (h : Function.Surjective (algebraMap R S))
+    (f : A →ₐ[R] B) :
+    (f.extendScalarsOfSurjective h).restrictScalars R = f := rfl
+
+end
+
 end AlgHom
 
 namespace AlgEquiv
@@ -236,6 +255,30 @@ lemma coe_restrictScalars_symm (f : A ≃ₐ[S] B) :
 lemma coe_restrictScalars_symm' (f : A ≃ₐ[S] B) :
     ((restrictScalars R f).symm : B → A) = f.symm := rfl
 
+section
+
+variable {R}
+
+/-- Any `f : A ≃ₐ[R] B` is also an `R ⧸ I`-algebra isomorphism if the `R`-algebra structure on
+`A` and `B` factors via `R ⧸ I`. -/
+@[simps! apply]
+def extendScalarsOfSurjective (h : Function.Surjective (algebraMap R S))
+    (f : A ≃ₐ[R] B) : A ≃ₐ[S] B where
+  toRingEquiv := f
+  commutes' := (f.toAlgHom.extendScalarsOfSurjective h).commutes'
+
+@[simp]
+lemma restrictScalars_extendScalarsOfSurjective (h : Function.Surjective (algebraMap R S))
+    (f : A ≃ₐ[R] B) :
+    (f.extendScalarsOfSurjective h).restrictScalars R = f := rfl
+
+@[simp]
+lemma extendScalarsOfSurjective_symm (h : Function.Surjective (algebraMap R S))
+    (f : A ≃ₐ[R] B) :
+    (f.extendScalarsOfSurjective h).symm = f.symm.extendScalarsOfSurjective h := rfl
+
+end
+
 end AlgEquiv
 
 end Homs

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -364,6 +364,10 @@ theorem aeval_X_left : aeval (X : R[X]) = AlgHom.id R R[X] :=
 theorem aeval_X_left_apply (p : R[X]) : aeval X p = p :=
   AlgHom.congr_fun (@aeval_X_left R _) p
 
+lemma aeval_X_left_eq_map [CommSemiring S] [Algebra R S] (p : R[X]) :
+    aeval X p = map (algebraMap R S) p :=
+  rfl
+
 theorem eval_unique (φ : R[X] →ₐ[R] A) (p) : φ p = eval₂ (algebraMap R A) (φ X) p := by
   rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]
 

Mathlib/RingTheory/Finiteness/ModuleFinitePresentation.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2025 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+import Mathlib.Algebra.Module.FinitePresentation
+import Mathlib.RingTheory.AdjoinRoot
+
+/-!
+# Finitely presented algebras and finitely presented modules
+
+In this file we establish relations between finitely presented as an algebra and
+finitely presented as a module.
+
+## Main results:
+
+- `Algebra.FinitePresentation.of_finitePresentation`: If `S` is finitely presented as a
+  module over `R`, then it is finitely presented as an algebra over `R`.
+- `Module.FinitePresentation.of_finite_of_finitePresentation`: If `S` is finite as a module over `R`
+  and finitely presented as an algebra over `R`, then it is finitely presented as a module over `R`.
+
+## References
+
+- [Grothendieck, EGA IV₁ 1.4.7][ega-iv-1]
+-/
+
+universe u
+
+variable (R : Type u) (S : Type*) [CommRing R] [CommRing S] [Algebra R S]
+
+/-- EGA IV₁, 1.4.7.1 -/
+lemma Module.Finite.exists_free_surjective [Module.Finite R S] :
+    ∃ (S' : Type u) (_ : CommRing S') (_ : Algebra R S') (_ : Module.Finite R S')
+      (_ : Module.Free R S') (_ : Algebra.FinitePresentation R S')
+      (f : S' →ₐ[R] S), Function.Surjective f := by
+  classical
+  obtain ⟨s, hs⟩ : (⊤ : Submodule R S).FG := Module.finite_def.mp inferInstance
+  suffices h : ∃ (S' : Type u) (_ : CommRing S') (_ : Algebra R S') (_ : Module.Finite R S')
+      (_ : Module.Free R S') (_ : Algebra.FinitePresentation R S')
+      (f : S' →ₐ[R] S), (s : Set S) ⊆ AlgHom.range f by
+    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := h
+    have hf : Function.Surjective f := by
+      have := (Submodule.span_le (p := LinearMap.range f.toLinearMap)).mpr hsf
+      rwa [hs, top_le_iff, LinearMap.range_eq_top] at this
+    use S', ‹_›, ‹_›, ‹_›, ‹_›, ‹_›, f
+  clear hs
+  induction s using Finset.induction with
+  | empty =>
+    exact ⟨R, _, _, inferInstance, inferInstance, inferInstance, Algebra.ofId R S, by simp⟩
+  | insert a s has IH =>
+    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := IH
+    have ha := Algebra.IsIntegral.isIntegral (R := R) a
+    have := ((minpoly.monic ha).map (algebraMap R S')).finite_adjoinRoot
+    have := ((minpoly.monic ha).map (algebraMap R S')).free_adjoinRoot
+    algebraize [f.toRingHom]
+    refine ⟨AdjoinRoot ((minpoly R a).map (algebraMap R S')), inferInstance, inferInstance,
+      .trans S' _, .trans (S := S'), .trans _ S' _,
+      (AdjoinRoot.liftAlgHom _ (Algebra.ofId _ _) a
+        (by simp [← Polynomial.aeval_def])).restrictScalars R, ?_⟩
+    simp only [Finset.coe_insert, AlgHom.coe_range, AlgHom.coe_restrictScalars',
+      Set.insert_subset_iff, Set.mem_range]
+    exact ⟨⟨.root _, by simp⟩, hsf.trans fun y ⟨x, hx⟩ ↦ ⟨.of _ x, by simpa⟩⟩
+
+/-- If `S` is finitely presented as a module over `R`, it is finitely
+presented as an algebra over `R`. -/
+instance Algebra.FinitePresentation.of_finitePresentation
+    [Module.FinitePresentation R S] : Algebra.FinitePresentation R S := by
+  obtain ⟨S', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S
+  refine .of_surjective hf ?_
+  apply Submodule.FG.of_restrictScalars R
+  exact Module.FinitePresentation.fg_ker f.toLinearMap hf
+
+/-- If `S` is finite as a module over `R` and finitely presented as an algebra over `R`, then
+it is finitely presented as a module over `R`. -/
+@[stacks 0564 "The case M = S"]
+lemma Module.FinitePresentation.of_finite_of_finitePresentation
+    [Module.Finite R S] [Algebra.FinitePresentation R S] :
+    Module.FinitePresentation R S := by
+  classical
+  obtain ⟨R', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S
+  letI := f.toRingHom.toAlgebra
+  have : IsScalarTower R R' S := .of_algebraMap_eq' f.comp_algebraMap.symm
+  have : Module.FinitePresentation R R' :=
+    Module.finitePresentation_of_projective R R'
+  have : Module.FinitePresentation R' S :=
+    Module.finitePresentation_of_surjective (Algebra.linearMap R' S) hf
+      (Algebra.FinitePresentation.ker_fG_of_surjective f hf)
+  exact .trans R S R'
+
+/-- If `S` is a finite `R`-algebra, finitely presented as a module and as an algebra
+is equivalent. -/
+lemma Module.FinitePresentation.iff_finitePresentation_of_finite [Module.Finite R S] :
+    Module.FinitePresentation R S ↔ Algebra.FinitePresentation R S :=
+  ⟨fun _ ↦ .of_finitePresentation R S, fun _ ↦ .of_finite_of_finitePresentation R S⟩

Mathlib/RingTheory/Polynomial/Basic.lean

@@ -759,6 +759,9 @@ end Polynomial
 
 namespace MvPolynomial
 
+instance {ι R : Type*} [CommSemiring R] [IsEmpty ι] : Module.Finite R (MvPolynomial ι R) :=
+  Module.Finite.equiv (MvPolynomial.isEmptyAlgEquiv R ι).toLinearEquiv.symm
+
 private theorem prime_C_iff_of_fintype {R : Type u} (σ : Type v) {r : R} [CommRing R] [Fintype σ] :
     Prime (C r : MvPolynomial σ R) ↔ Prime r := by
   rw [← MulEquiv.prime_iff (renameEquiv R (Fintype.equivFin σ))]

docs/references.bib

@@ -1559,6 +1559,25 @@ @Article{         Echenique2005
   doi           = {10.1007/s001820400192}
 }
 
+@Article{         ega-iv-1,
+  author        = {Grothendieck, A.},
+  title         = {{\'E}l{\'e}ments de g{\'e}om{\'e}trie alg{\'e}brique.
+                  {IV}: {\'E}tude locale des sch{\'e}mas et des morphismes de
+                  sch{\'e}mas. ({Premi{\`e}re} partie). {R{\'e}dig{\'e}} avec
+                  la colloboration de {J}. {Dieudonn{\'e}}},
+  fjournal      = {Publications Math{\'e}matiques},
+  journal       = {Publ. Math., Inst. Hautes {\'E}tud. Sci.},
+  issn          = {0073-8301},
+  volume        = {20},
+  pages         = {101--355},
+  year          = {1964},
+  language      = {French},
+  doi           = {10.1007/BF02684747},
+  keywords      = {14-02,14Axx},
+  zbmath        = {3220890},
+  zbl           = {0136.15901}
+}
+
 @Book{            egno15,
   author        = {Etingof, Pavel and Gelaki, Shlomo and Nikshych, Dmitri and
                   Ostrik, Victor},