feat(RingTheory/Presentation): core of a presentation (#24794)

If `P` is a presentation of `S` as an `R`-algebra and `R₀` a subring of `R` containing the coefficients of the relations of `P`, then there exists an `R₀`-algebra `S₀` such that `S` is isomorphic to the base change of `S₀` to `R`.

This is a tool to remove Noetherian hypothesis in certain situations.

Author: chrisflav

Mathlib.lean

@@ -5506,6 +5506,7 @@ import Mathlib.RingTheory.Extension.Cotangent.Basic
 import Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
 import Mathlib.RingTheory.Extension.Generators
 import Mathlib.RingTheory.Extension.Presentation.Basic
+import Mathlib.RingTheory.Extension.Presentation.Core
 import Mathlib.RingTheory.Extension.Presentation.Submersive
 import Mathlib.RingTheory.FilteredAlgebra.Basic
 import Mathlib.RingTheory.Filtration

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -832,6 +832,11 @@ theorem algebraMap_mk {R A : Type*} [CommSemiring R] [CommSemiring A] [Semiring
     [Algebra R A] [Algebra A α] {S : Subalgebra R A} (a : A) (ha : a ∈ S) :
   algebraMap S α (⟨a, ha⟩ : S) = algebraMap A α a := rfl
 
+@[simp]
+lemma algebraMap_apply {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
+    (S : Subalgebra R A) (x : S) : algebraMap S A x = x :=
+  rfl
+
 @[simp]
 theorem rangeS_algebraMap {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
     (S : Subalgebra R A) : (algebraMap S A).rangeS = S.toSubsemiring := by
@@ -844,6 +849,11 @@ theorem range_algebraMap {R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
   rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubring_subtype,
     Subring.range_subtype]
 
+@[simp]
+lemma setRange_algebraMap {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
+    (S : Subalgebra R A) : Set.range (algebraMap S A) = (S : Set A) :=
+  SetLike.ext'_iff.mp S.rangeS_algebraMap
+
 instance noZeroSMulDivisors_top [NoZeroDivisors A] (S : Subalgebra R A) : NoZeroSMulDivisors S A :=
   ⟨fun {c} x h =>
     have : (c : A) = 0 ∨ x = 0 := eq_zero_or_eq_zero_of_mul_eq_zero h

Mathlib/Algebra/Algebra/Subalgebra/Tower.lean

@@ -79,7 +79,7 @@ variable [IsScalarTower R S A] [IsScalarTower R S B]
 def restrictScalars (U : Subalgebra S A) : Subalgebra R A :=
   { U with
     algebraMap_mem' := fun x ↦ by
-      rw [algebraMap_apply R S A]
+      rw [IsScalarTower.algebraMap_apply R S A]
       exact U.algebraMap_mem _ }
 
 @[simp]

Mathlib/Algebra/Algebra/Tower.lean

@@ -225,6 +225,17 @@ theorem restrictScalars_injective :
     Function.Injective (restrictScalars R : (A ≃ₐ[S] B) → A ≃ₐ[R] B) := fun _ _ h =>
   AlgEquiv.ext (AlgEquiv.congr_fun h :)
 
+lemma restrictScalars_symm_apply (f : A ≃ₐ[S] B) (x : B) :
+    (f.restrictScalars R).symm x = f.symm x := rfl
+
+@[simp]
+lemma coe_restrictScalars_symm (f : A ≃ₐ[S] B) :
+    ((f.restrictScalars R).symm : B ≃+* A) = f.symm := rfl
+
+@[simp]
+lemma coe_restrictScalars_symm' (f : A ≃ₐ[S] B) :
+    ((restrictScalars R f).symm : B → A) = f.symm := rfl
+
 end AlgEquiv
 
 end Homs

Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean

@@ -170,7 +170,7 @@ theorem sumElim_iff {ι'} {y : ι' → A} : AlgebraicIndependent R (Sum.elim y x
   · exact ⟨fun h ↦ (hx <| by apply h.comp _ Sum.inr_injective).elim, fun h ↦ (hx h.1).elim⟩
   let e := (sumAlgEquiv R ι' ι).trans (mapAlgEquiv _ hx.aevalEquiv)
   have : aeval (Sum.elim y x) = ((aeval y).restrictScalars R).comp e.toAlgHom := by
-    ext (_ | _) <;> simp [e, algebraMap_aevalEquiv]
+    ext (_ | _) <;> simp [e]
   simp_rw [hx, AlgebraicIndependent, this]; simp
 
 theorem iff_adjoin_image (s : Set ι) :
@@ -205,7 +205,7 @@ theorem sumElim_of_tower {ι'} {y : ι' → A} (hxS : range x ⊆ range (algebra
   set Rx := adjoin R (range x)
   let _ : Algebra Rx S :=
     (e.symm.toAlgHom.comp <| Subalgebra.inclusion <| adjoin_le hxS).toAlgebra
-  have : IsScalarTower Rx S A := .of_algebraMap_eq fun x ↦ show _ = (e (e.symm _)).1 by simp; rfl
+  have : IsScalarTower Rx S A := .of_algebraMap_eq fun x ↦ show _ = (e (e.symm _)).1 by simp
   refine hx.sumElim (hy.restrictScalars (e.symm.injective.comp ?_))
   simpa only [AlgHom.coe_toRingHom] using Subalgebra.inclusion_injective _
 

Mathlib/RingTheory/Extension/Presentation/Core.lean

@@ -0,0 +1,204 @@
+/-
+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.RingTheory.Extension.Presentation.Basic
+
+/-!
+# Presentations on subrings
+
+In this file we establish the API for realising a presentation over a
+subring of `R`. We define a property `HasCoeffs R₀` for a presentation `P` to mean
+the (sub)ring `R₀` contains the coefficients of the relations of `P`.
+subring `R₀` of `R` that contains the coefficients of the relations
+In this case there exists a model of `S` over `R₀`, i.e., there exists an `R₀`-algebra `S₀`
+such that `S` is isomorphic to `R ⊗[R₀] S₀`.
+
+If the presentation is finite, `R₀` may be chosen as a Noetherian ring. In this case,
+this API can be used to remove Noetherian hypothesis in certain cases.
+
+-/
+
+open TensorProduct
+
+variable {R S ι σ : Type*} [CommRing R] [CommRing S] [Algebra R S]
+
+variable {P : Algebra.Presentation R S ι σ}
+
+namespace Algebra.Presentation
+
+variable (P) in
+/-- The coefficients of a presentation are the coefficients of the relations. -/
+def coeffs : Set R := ⋃ (i : σ), (P.relation i).coeffs
+
+lemma coeffs_relation_subset_coeffs (x : σ) :
+    ((P.relation x).coeffs : Set R) ⊆ P.coeffs :=
+  Set.subset_iUnion_of_subset x (by simp)
+
+lemma finite_coeffs [Finite σ] : P.coeffs.Finite :=
+  Set.finite_iUnion fun _ ↦ Finset.finite_toSet _
+
+variable (P) in
+/-- The core of a presentation is the subalgebra generated by the coefficients of the relations. -/
+def core : Subalgebra ℤ R := Algebra.adjoin _ P.coeffs
+
+variable (P) in
+lemma coeffs_subset_core : P.coeffs ⊆ P.core := Algebra.subset_adjoin
+
+lemma coeffs_relation_subset_core (x : σ) :
+    ((P.relation x).coeffs : Set R) ⊆ P.core :=
+  subset_trans (P.coeffs_relation_subset_coeffs x) P.coeffs_subset_core
+
+variable (P) in
+/-- The core coerced to a type for performance reasons. -/
+def Core : Type _ := P.core
+
+instance : CommRing P.Core := fast_instance% (inferInstanceAs <| CommRing P.core)
+instance : Algebra P.Core R := fast_instance% (inferInstanceAs <| Algebra P.core R)
+instance : FaithfulSMul P.Core R := inferInstanceAs <| FaithfulSMul P.core R
+instance : Algebra P.Core S := fast_instance% (inferInstanceAs <| Algebra P.core S)
+instance : IsScalarTower P.Core R S := inferInstanceAs <| IsScalarTower P.core R S
+
+instance [Finite σ] : FiniteType ℤ P.Core := .adjoin_of_finite P.finite_coeffs
+
+variable (P) in
+/--
+A ring `R₀` has the coefficients of the presentation `P` if the coefficients of the relations of `P`
+lie in the image of `R₀` in `R`.
+The smallest subring of `R` satisfying this is given by `Algebra.Presentation.Core P`.
+-/
+class HasCoeffs (R₀ : Type*) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S]
+    [IsScalarTower R₀ R S] where
+  coeffs_subset_range : P.coeffs ⊆ Set.range (algebraMap R₀ R)
+
+instance : P.HasCoeffs P.Core where
+  coeffs_subset_range := by
+    refine subset_trans P.coeffs_subset_core ?_
+    simp [Core, Subalgebra.algebraMap_eq]
+
+variable (R₀ : Type*) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S]
+  [P.HasCoeffs R₀]
+
+lemma coeffs_subset_range : (P.coeffs : Set R) ⊆ Set.range (algebraMap R₀ R) :=
+  HasCoeffs.coeffs_subset_range
+
+lemma HasCoeffs.of_isScalarTower {R₁ : Type*} [CommRing R₁] [Algebra R₀ R₁] [Algebra R₁ R]
+    [IsScalarTower R₀ R₁ R] [Algebra R₁ S] [IsScalarTower R₁ R S] :
+    P.HasCoeffs R₁ := by
+  refine ⟨subset_trans (P.coeffs_subset_range R₀) ?_⟩
+  simp [IsScalarTower.algebraMap_eq R₀ R₁ R, RingHom.coe_comp, Set.range_comp]
+
+instance (s : Set R) : P.HasCoeffs (Algebra.adjoin R₀ s) := HasCoeffs.of_isScalarTower R₀
+
+lemma HasCoeffs.coeffs_relation_mem_range (x : σ) :
+    ↑(P.relation x).coeffs ⊆ Set.range (algebraMap R₀ R) :=
+  subset_trans (P.coeffs_relation_subset_coeffs x) HasCoeffs.coeffs_subset_range
+
+lemma HasCoeffs.relation_mem_range_map (x : σ) :
+    P.relation x ∈ Set.range (MvPolynomial.map (algebraMap R₀ R)) := by
+  rw [MvPolynomial.mem_range_map_iff_coeffs_subset]
+  exact HasCoeffs.coeffs_relation_mem_range R₀ x
+
+/-- The `r`-th relation of `P` as a polynomial in `R₀`. This is the (arbitrary) choice of a
+pre-image under the map `R₀[X] → R[X]`. -/
+noncomputable def relationOfHasCoeffs (r : σ) : MvPolynomial ι R₀ :=
+  (HasCoeffs.relation_mem_range_map (P := P) R₀ r).choose
+
+lemma map_relationOfHasCoeffs (r : σ) :
+    MvPolynomial.map (algebraMap R₀ R) (P.relationOfHasCoeffs R₀ r) = P.relation r :=
+  (HasCoeffs.relation_mem_range_map R₀ r).choose_spec
+
+@[simp]
+lemma aeval_val_relationOfHasCoeffs (r : σ) :
+    MvPolynomial.aeval P.val (P.relationOfHasCoeffs R₀ r) = 0 := by
+  rw [← MvPolynomial.aeval_map_algebraMap R, map_relationOfHasCoeffs, aeval_val_relation]
+
+@[simp]
+lemma algebraTensorAlgEquiv_symm_relation (r : σ) :
+    (MvPolynomial.algebraTensorAlgEquiv R₀ R).symm (P.relation r) =
+      1 ⊗ₜ P.relationOfHasCoeffs R₀ r := by
+  rw [← map_relationOfHasCoeffs R₀, MvPolynomial.algebraTensorAlgEquiv_symm_map]
+
+/-- The model of `S` over a `R₀` that contains the coefficients of `P` is `R₀[X]` quotiented by the
+same relations. -/
+abbrev ModelOfHasCoeffs : Type _ :=
+  MvPolynomial ι R₀ ⧸ (Ideal.span <| Set.range (P.relationOfHasCoeffs R₀))
+
+instance [Finite ι] [Finite σ] : Algebra.FinitePresentation R₀ (P.ModelOfHasCoeffs R₀) := by
+  classical
+  cases nonempty_fintype σ
+  exact .quotient ⟨Finset.image (P.relationOfHasCoeffs R₀) .univ, by simp⟩
+
+variable (P) in
+/-- (Implementation detail): The underlying `AlgHom` of `tensorModelOfHasCoeffsEquiv`. -/
+noncomputable def tensorModelOfHasCoeffsHom : R ⊗[R₀] P.ModelOfHasCoeffs R₀ →ₐ[R] S :=
+  Algebra.TensorProduct.lift (Algebra.ofId R S)
+    (Ideal.Quotient.liftₐ _ (MvPolynomial.aeval P.val) <| by
+      simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le]
+      rintro a ⟨i, rfl⟩
+      simp)
+    fun _ _ ↦ Commute.all _ _
+
+@[simp]
+lemma tensorModelOfHasCoeffsHom_tmul (x : R) (y : MvPolynomial ι R₀) :
+    P.tensorModelOfHasCoeffsHom R₀ (x ⊗ₜ y) = algebraMap R S x * MvPolynomial.aeval P.val y :=
+  rfl
+
+variable (P) in
+/-- (Implementation detail): The inverse of `tensorModelOfHasCoeffsHom`. -/
+noncomputable def tensorModelOfHasCoeffsInv : S →ₐ[R] R ⊗[R₀] P.ModelOfHasCoeffs R₀ :=
+  (Ideal.Quotient.liftₐ _
+    ((Algebra.TensorProduct.map (.id R R) (Ideal.Quotient.mkₐ _ _)).comp
+      (MvPolynomial.algebraTensorAlgEquiv R₀ R).symm.toAlgHom) <| by
+    simp_rw [← RingHom.mem_ker, ← SetLike.le_def]
+    rw [← P.span_range_relation_eq_ker, Ideal.span_le]
+    rintro a ⟨i, rfl⟩
+    simp only [AlgEquiv.toAlgHom_eq_coe, SetLike.mem_coe, RingHom.mem_ker, AlgHom.coe_comp,
+      AlgHom.coe_coe, Function.comp_apply, algebraTensorAlgEquiv_symm_relation]
+    simp only [TensorProduct.map_tmul, AlgHom.coe_id, id_eq, Ideal.Quotient.mkₐ_eq_mk,
+      Ideal.Quotient.mk_span_range, tmul_zero]).comp
+    (P.quotientEquiv.restrictScalars R).symm.toAlgHom
+
+@[simp]
+lemma tensorModelOfHasCoeffsInv_aeval_val (x : MvPolynomial ι R₀) :
+    P.tensorModelOfHasCoeffsInv R₀ (MvPolynomial.aeval P.val x) =
+      1 ⊗ₜ[R₀] (Ideal.Quotient.mk _ x) := by
+  rw [← MvPolynomial.aeval_map_algebraMap R, ← Generators.algebraMap_apply, ← quotientEquiv_mk]
+  simp [tensorModelOfHasCoeffsInv, -quotientEquiv_symm, -quotientEquiv_mk]
+
+private lemma hom_comp_inv :
+    (P.tensorModelOfHasCoeffsHom R₀).comp (P.tensorModelOfHasCoeffsInv R₀) = AlgHom.id R S := by
+  have h : Function.Surjective
+      ((P.quotientEquiv.restrictScalars R).toAlgHom.comp (Ideal.Quotient.mkₐ _ _)) :=
+    (P.quotientEquiv.restrictScalars R).surjective.comp Ideal.Quotient.mk_surjective
+  simp only [← AlgHom.cancel_right h, tensorModelOfHasCoeffsInv, AlgEquiv.toAlgHom_eq_coe,
+    AlgHom.id_comp]
+  rw [AlgHom.comp_assoc, AlgHom.comp_assoc, ← AlgHom.comp_assoc _ _ (Ideal.Quotient.mkₐ R P.ker),
+    AlgEquiv.symm_comp, AlgHom.id_comp]
+  ext x
+  simp
+
+private lemma inv_comp_hom :
+    (P.tensorModelOfHasCoeffsInv R₀).comp (P.tensorModelOfHasCoeffsHom R₀) = AlgHom.id R _ := by
+  ext x
+  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
+  simp
+
+/-- The natural isomorphism `R ⊗[R₀] S₀ ≃ₐ[R] S`. -/
+noncomputable def tensorModelOfHasCoeffsEquiv : R ⊗[R₀] P.ModelOfHasCoeffs R₀ ≃ₐ[R] S :=
+  AlgEquiv.ofAlgHom (P.tensorModelOfHasCoeffsHom R₀) (P.tensorModelOfHasCoeffsInv R₀)
+    (P.hom_comp_inv R₀) (P.inv_comp_hom R₀)
+
+@[simp]
+lemma tensorModelOfHasCoeffsEquiv_tmul (x : R) (y : MvPolynomial ι R₀) :
+    P.tensorModelOfHasCoeffsEquiv R₀ (x ⊗ₜ y) = algebraMap R S x * MvPolynomial.aeval P.val y :=
+  rfl
+
+@[simp]
+lemma tensorModelOfHasCoeffsEquiv_symm_tmul (x : MvPolynomial ι R₀) :
+    (P.tensorModelOfHasCoeffsEquiv R₀).symm (MvPolynomial.aeval P.val x) =
+      1 ⊗ₜ[R₀] (Ideal.Quotient.mk _ x) :=
+  tensorModelOfHasCoeffsInv_aeval_val _ x
+
+end Algebra.Presentation

Mathlib/RingTheory/FiniteType.lean

@@ -209,6 +209,11 @@ theorem isNoetherianRing (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
 theorem _root_.Subalgebra.fg_iff_finiteType (S : Subalgebra R A) : S.FG ↔ Algebra.FiniteType R S :=
   S.fg_top.symm.trans ⟨fun h => ⟨h⟩, fun h => h.out⟩
 
+lemma adjoin_of_finite {A : Type*} [CommSemiring A] [Algebra R A] {t : Set A} (h : Set.Finite t) :
+    FiniteType R (Algebra.adjoin R t) := by
+  rw [← Subalgebra.fg_iff_finiteType]
+  exact ⟨h.toFinset, by simp⟩
+
 end FiniteType
 
 end Algebra

Mathlib/RingTheory/Ideal/Quotient/Basic.lean

@@ -36,6 +36,12 @@ variable {S : Type v}
 
 namespace Quotient
 
+@[simp]
+lemma mk_span_range {ι : Type*} (f : ι → R) [(span (range f)).IsTwoSided] (i : ι) :
+    mk (span (.range f)) (f i) = 0 := by
+  rw [Ideal.Quotient.eq_zero_iff_mem]
+  exact Ideal.subset_span ⟨i, rfl⟩
+
 variable {I} {x y : R}
 
 theorem zero_eq_one_iff : (0 : R ⧸ I) = 1 ↔ I = ⊤ :=

Mathlib/RingTheory/LinearDisjoint.lean

@@ -270,7 +270,7 @@ noncomputable def basisOfBasisRight (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis
 @[simp]
 theorem algebraMap_basisOfBasisRight_apply (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis ι R B) (i : ι) :
     H.basisOfBasisRight H' b i = algebraMap B S (b i) := by
-  simp [basisOfBasisRight, Subalgebra.algebraMap_def]
+  simp [basisOfBasisRight]
 
 @[simp]
 theorem mulMapLeftOfSupEqTop_symm_apply (H' : A ⊔ B = ⊤) (x : B) :
@@ -287,8 +287,7 @@ theorem leftMulMatrix_basisOfBasisRight_algebraMap (H' : A ⊔ B = ⊤) {ι : Ty
     Algebra.leftMulMatrix (H.basisOfBasisRight H' b) (algebraMap B S x) =
       RingHom.mapMatrix (algebraMap R A) (Algebra.leftMulMatrix b x) := by
   ext
-  simp [Algebra.leftMulMatrix_eq_repr_mul, ← H.algebraMap_basisOfBasisRight_repr_apply H',
-    Subalgebra.algebraMap_def]
+  simp [Algebra.leftMulMatrix_eq_repr_mul, ← H.algebraMap_basisOfBasisRight_repr_apply H']
 
 /--
 If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are

Mathlib/RingTheory/TensorProduct/MvPolynomial.lean

@@ -237,6 +237,20 @@ lemma algebraTensorAlgEquiv_symm_monomial (m : σ →₀ ℕ) (a : A) :
     nth_rw 2 [← mul_one a]
     rw [Algebra.TensorProduct.tmul_mul_tmul]
 
+@[simp]
+lemma algebraTensorAlgEquiv_symm_comp_aeval :
+    (((algebraTensorAlgEquiv (σ := σ) R A).symm.restrictScalars R) :
+        MvPolynomial σ A →ₐ[R] A ⊗[R] MvPolynomial σ R).comp
+      (MvPolynomial.mapAlgHom (R := R) (S₁ := R) (S₂ := A) (Algebra.ofId R A)) =
+      Algebra.TensorProduct.includeRight := by
+  ext
+  simp
+
+@[simp]
+lemma algebraTensorAlgEquiv_symm_map (x : MvPolynomial σ R) :
+    (algebraTensorAlgEquiv R A).symm (map (algebraMap R A) x) = 1 ⊗ₜ x :=
+  DFunLike.congr_fun (algebraTensorAlgEquiv_symm_comp_aeval R A) x
+
 lemma aeval_one_tmul (f : σ → S) (p : MvPolynomial σ R) :
     (aeval fun x ↦ (1 ⊗ₜ[R] f x : N ⊗[R] S)) p = 1 ⊗ₜ[R] (aeval f) p := by
   induction p using MvPolynomial.induction_on with