finite extension of DVR

Stream: Is there code for X?

[Kenny Lau]

Is every finite extension of DVR a PID?

import Mathlib

example (A B : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
    [Algebra A B] [Module.Finite A B] :
    IsPrincipalIdealRing B :=
  sorry

For more context, I thought I would show a complicated proof to see if there's a simpler proof, so that I could simplify IsDedekindDomain.isPrincipalIdealRing_localization_over_prime, but I couldn't come up with a proof in the first place.

For even more context, this came up while thinking about #31061, which is a PR in response to #Is there code for X? > For a Dedekind domain, UFD implies PID

[Andrew Yang]

It is a dedekind domain with finite maximal ideals.

[Kenny Lau]

I tried to do that, but I found out that installing the Dedekind domain instance requires talking about the fraction fields (and actually in this setup Frac(A) doesn't have to map to Frac(B))

[Kenny Lau]

this is definitely deviating from the usual "AKLB" setup

[Andrew Yang]

By extension I assumed that A->B is injective? If not then I guess it is a boring case because B is then just a field extension of the residue field.

[Kenny Lau]

feel free to add that assumption to my code

[Andrew Yang]

Then Frac(A) should map to Frac(B)?

[Kenny Lau]

should we have this step separately in mathlib?

[Andrew Yang]

Do you mean docs#FractionRing.liftAlgebra ?

[Kenny Lau]

i mean the whole step of A is dedekind + B/A is finite => B is dedekind, which cases on whether it factors through a maximal ideal

[Riccardo Brasca]

Andrew Yang said:

It is a dedekind domain with finite maximal ideals.

This is a PID, right?

[Kenny Lau]

yes

[Antoine Chambert-Loir]

A proof is in the book by Auslander and Buchsbaum, Groups, rings, modules, corollary 1.4 of chapter 13 (p. 447).
image.png

[Kenny Lau]

hi, sorry, I should have clarified, we already have the theorem "semilocal + DD -> PID" in mathlib, what i'm asking above is that specific application to fin ext of DVR

[Kenny Lau]

in other words, the proof goes fin ext of DVR -> semilocal + DD -> PID, and we have the second ->, but I'm asking about the first ->

[Kenny Lau]

semilocal should be slightly non-trivial but should be easy, it's the DD that is the problem

[Andrew Yang]

Arbitrary finite extensions of DVRs are not necessarily dedekind domains.
Integral extensions preserves dimension and finite type extensions preserves noetherianity but neither preserves normality.

[Kenny Lau]

import Mathlib.RingTheory.DedekindDomain.PID
import Mathlib.RingTheory.RingHom.Finite

local notation:max "𝓂["R"]" => IsLocalRing.maximalIdeal R

-- (fin ext / DVR) + DD => PID
theorem pid_of_finExtDVR_of_DD (R S : Type*)
    [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [CommRing S] [IsDedekindDomain S]
    [Algebra R S] [Module.Finite R S] [FaithfulSMul R S] :
    IsPrincipalIdealRing S := by
  letI := Classical.decEq (Ideal S)
  letI := Classical.decPred fun P : Ideal S => P.IsPrime
  refine .of_finite_maximals ?_
  convert primesOver_finite 𝓂[R] S using 1
  ext I
  simp_rw [Ideal.primesOver, Set.mem_setOf_eq]
  refine ⟨fun h ↦ ⟨h.isPrime, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
  · rw [Ideal.liesOver_iff]
    exact (IsLocalRing.eq_maximalIdeal inferInstance).symm
  · exact Ideal.IsMaximal.of_liesOver_isMaximal I 𝓂[R]

section
variable {R : Type*} [CommRing R]
variable [IsDedekindDomain R]
variable (S : Type*) [CommRing S]
variable [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S]
variable (p : Ideal R) (hp0 : p ≠ ⊥) [p.IsPrime]
variable {Sₚ : Type*} [CommRing Sₚ] [Algebra S Sₚ]
variable [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
variable [Algebra R Sₚ] [IsScalarTower R S Sₚ]
variable [IsDedekindDomain Sₚ]
include hp0

#check IsDedekindDomain.isPrincipalIdealRing_localization_over_prime

theorem IsDedekindDomain.isPrincipalIdealRing_localization_over_prime' [IsDomain S] :
    IsPrincipalIdealRing Sₚ :=
  have : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ := ‹_›
  let : IsDiscreteValuationRing (Localization.AtPrime p) :=
    IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain _ hp0 _
  let : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra _ S
  have : IsScalarTower R (Localization.AtPrime p) Sₚ := .of_algebraMap_eq fun x ↦ by
    change _ = IsLocalization.map Sₚ (algebraMap R S) p.primeCompl.le_comap_map
      (algebraMap _ _ x : Localization.AtPrime p)
    rw [IsLocalization.map_eq, ← IsScalarTower.algebraMap_apply]
  have : Module.Finite (Localization.AtPrime p) Sₚ :=
    Module.Finite.of_isLocalization R S p.primeCompl
  have : NoZeroSMulDivisors (Localization.AtPrime p) Sₚ :=
    NoZeroSMulDivisors_of_isLocalization R S _ _ p.primeCompl_le_nonZeroDivisors
  pid_of_finExtDVR_of_DD (Localization.AtPrime p) _

[Kenny Lau]

thanks, with this input I've realised that IsDedekindDomain.isPrincipalIdealRing_localization_over_prime actually assumes IsDedekindDomain Sₚ to begin with, and I've now factorised this lemma into the two lemmas in my code above

[Kenny Lau]

it's a bit messy here but everything is just setting up the correct algebra structures, and then the final line just uses pid_of_finExtDVR_of_DD

[Kenny Lau]

I would say that in a "real" use case, one would already have the commuting square, so I think we should remove the existing lemma in mathlib and replace it with pid_of_finExtDVR_of_DD from my code above

[Antoine Chambert-Loir]

But it seems that the request assumed that the extension was normal.

[Junyan Xu]

A full proof of the statement in the OP:

import Mathlib.RingTheory.Artinian.Module
import Mathlib.RingTheory.DedekindDomain.PID
import Mathlib.RingTheory.LocalRing.ResidueField.Fiber
import Mathlib.RingTheory.TensorProduct.Finite

variable (A B : Type*) [CommRing A] [CommRing B] [Algebra A B] [Module.Finite A B]

open TensorProduct in
/-- A finite ring hom induces a finite-to-one map on the prime spectra. -/
theorem PrimeSpectrum.finite_preimage_specComap_singleton (p : PrimeSpectrum A) :
    ((algebraMap A B).specComap ⁻¹' {p}).Finite :=
  (preimageOrderIsoTensorResidueField A B p).finite_iff.mpr <|
    have := IsArtinianRing.of_finite p.1.ResidueField (p.1.ResidueField ⊗[A] B)
    inferInstance

theorem Finite.comap {α β} [Finite β] (f : α → β) (h : ∀ b, (f ⁻¹' {b}).Finite) :
    Finite α := by
  contrapose! h
  simp only [Set.Finite, not_finite_iff_infinite]
  exact Finite.exists_infinite_fiber f
-- see also Set.Finite.of_finite_fibers

theorem PrimeSpectrum.map_finite [Finite (PrimeSpectrum A)] :
    Finite (PrimeSpectrum B) :=
  .comap _ (PrimeSpectrum.finite_preimage_specComap_singleton A B)

variable [IsDomain A] [IsDiscreteValuationRing A] [IsDomain B] [IsIntegrallyClosed B]

instance : Finite (PrimeSpectrum A) :=
  have ⟨p, _, h⟩ := ((IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime A).mp ‹_›).2
  (PrimeSpectrum.equivSubtype A).finite_iff.mpr <| Set.Finite.subset (s := {⊥, p})
    (by simp) fun q hq1 ↦ or_iff_not_imp_left.mpr fun hq2 ↦ h q ⟨hq2, hq1⟩

include A in
theorem isDedekindDomain : IsDedekindDomain B where
  __ := IsNoetherianRing.of_finite A B
  __ := Ring.DimensionLEOne.isIntegralClosure A (FractionRing B) B
-- Mathlib doesn't know that integral extension doesn't increase Krull dimension

example : IsPrincipalIdealRing B :=
  have := isDedekindDomain A B
  .of_finite_primes <| (PrimeSpectrum.equivSubtype _).finite_iff.mp <|
    PrimeSpectrum.map_finite A B

[Kenny Lau]

nice!

[Junyan Xu]

Antoine Chambert-Loir said:

A proof is in the book by Auslander and Buchsbaum, Groups, rings, modules, corollary 1.4 of chapter 13 (p. 447).

I'm currently proving a version Proposition 1.3 with R not assumed to be an integral domain, aka stacks#02M9. Apparently "projective" can be replaced by "flat" as well.

[Junyan Xu]

#31241