Ring of definition

Stream: Is there code for X?

[Christian Merten]

Is there something like the following: Given a finitely presented R-algebra A, there exists a finite type ℤ-algebra R₀ and a finitely presented A₀-algebra such that R ⊗[R₀] A₀ is R-isomorphic to A. Note that I need an explicit construction, i.e. something like

import Mathlib

universe u v w

open TensorProduct

variable {R : Type u} [CommRing R] {ι : Type v} (I : Ideal (MvPolynomial ι R))
variable (S : Set (MvPolynomial ι R)) (hgenS : Ideal.span S = I) (hf : Set.Finite S)

def MvPolynomial.Set.coefficients (S : Set (MvPolynomial ι R)) : Set R :=
  Set.iUnion (ι := S) (fun (p : S) ↦ p.val.coeff '' p.val.support)

def RingOfDefinition : Subring R :=
  Subalgebra.toSubring (Algebra.adjoin ℤ (MvPolynomial.Set.coefficients S))

local notation "R₀" => RingOfDefinition S
local notation "A" => MvPolynomial ι R ⧸ I

def RingOfDefinition.Set : Set (MvPolynomial ι R₀) :=
  MvPolynomial.map (SubringClass.subtype R₀) ⁻¹' S

local notation "S₀" => RingOfDefinition.Set S
local notation "I₀" => Ideal.span S₀
local notation "A₀" => MvPolynomial ι R₀ ⧸ I₀

noncomputable local instance : Module R₀ A₀ := Algebra.toModule

def baseChange : R ⊗[R₀] A₀ ≃ₐ[R] A := sorry

[Adam Topaz]

I highly doubt that we have anything like this

[Kevin Buzzard]

We definitely should have it though! It's the first key idea in all that reduction to the noetherian case in EGA4 sections 8 to 11

[Christian Merten]

Working on it, would put this in something like RingTheory.RingOfDefinition?

[Christian Merten]

I have played around with this for a while now: Showing the above mentioned result is quite straightforward, but I tried to come up with a usable API if more is needed than merely the existence of such a subring, but also some control over which equalities should remain true. The suggestion can be found at draft PR #12743.

A quick summary of #12743: The interesting part is https://github.com/leanprover-community/mathlib4/blob/6091ad276d920fe835213a1a82392c7063529b45/Mathlib/RingTheory/RingOfDefinition/Basic.lean.

• introduce a typeclass HasCoefficients expressing that the coefficients of a polynomial are contained in a subring.
• automatically infer HasCoefficients under basic adjoinCoefficients operations, to reduce overhead when various sets of coefficients need to be adjoined.

One example (is in above linked file):

/- Lean automatically infers that any of the adjoined polynomials has coefficients in the new
ring. -/
example (t₁ t₂ t₃ t₄ : Set (MvPolynomial ι R)) (f : ℕ → MvPolynomial ι R) (p : t₁)
  (n : ℕ) :
    let R₀ := Subring.adjoinCoefficients t₄ <|
      Subring.adjoinCoefficients t₃ <|
      Subring.adjoinCoefficients (Set.range f) <|
      Subring.adjoinCoefficients t₂ <|
      core t₁;
    HasCoefficients (f n) R₀ ∧ HasCoefficients p.val R₀ :=
  ⟨inferInstance, inferInstance⟩

Given [HasCoefficients p R₀], p.repr R₀ is the representative of p in MvPolynomial ι R₀. For more details read the module docstring of the linked file.

A use of this API can be found in draft PR #12744. Here the relevant file is https://github.com/leanprover-community/mathlib4/blob/0f581c67990efbf323fbd70c2000945cb04022d1/Mathlib/RingTheory/Smooth/Descent.lean.

If you have any comments or suggestions, I would be happy to hear them.

[Junyan Xu]

Your coefficients is basically docs#Polynomial.frange. APIs around docs#Polynomial.toSubring and docs#Polynomial.liftsRing may also be useful.

[Christian Merten]

Thanks, that seems to be only for single variable polynomials though. But I can certainly adapt the naming. Although I find Polyonmial.frange less telling than "coefficients"

[Johan Commelin]

Yeah, it might make sense to adapt the naming in the other direction.