Valuation rings that are not domains

Stream: maths

[Yakov Pechersky]

I am working on formalizing Kaplansky's theorem, which states that

For commutative Noetherian R, R is a PIR iff every maximal ideal is principal.

In fact, his theorem is a classification of noetherian commutative rings -- every such ring can be decomposed as a finite direct sum of integral domains and valuation rings (with DCC).
image.png

[Yakov Pechersky]

However, this classification is not possible to state in this manner in mathlib, since ValuationRing assumes IsDomain.

[Yakov Pechersky]

There are rings that satisfy the axioms of ValuationRing that cannot satisfy IsDomain, and Mathlib knows about one such example: K[X] / X^2 where K is a field. Formalized as the dual numbers over K:

import Mathlib.RingTheory.DualNumber
import Mathlib.RingTheory.Valuation.ValuationRing

open DualNumber

variable {K : Type*} [Field K]

#synth IsPrincipalIdealRing K[ε]
#synth LocalRing K[ε]
#synth IsBezout K[ε]
#check maximalIdeal_eq_span_singleton_eps -- maximal ideal is not bot; requirement for DVR
#check exists_mul_left_or_mul_right -- ∀ (a b : K[ε]), ∃ c, a * c = b ∨ b * c = a
#check ValuationRing.cond' -- ∀ (a b : A), ∃ (c : A), a * c = b ∨ b * c = a
-- but we can't have IsDomain K[ε], since ε is nilpotent
#check isNilpotent_eps

[Yakov Pechersky]

Can the _definition_ of ValuationRing (and possibly DVR) be loosened to not require IsDomain? A small number of theorems would also no longer require it. And it would allow me to state the classification. Otherwise, I'll have to express the classification as a direct sum of integral domains and rings-that-have-the-valuation-ring-condition-but-not-as-a-class.

[Johan Commelin]

Weakening valuation ring sounds fine to me. I'm less sure about DVR. Is there literature on DVRs that are not domains? Would mathlib need a DVD concept?

[Yakov Pechersky]

I guess for DVR, my only current argument is consistency with the VR definition

[Adam Topaz]

Deligne has paper(s?) on "truncated DVRs"

[Ruben Van de Velde]

This one? https://github.com/riccardobrasca/kaplanski4/tree/master

Cc @Riccardo Brasca

[Kevin Buzzard]

I think that we shouldn't deviate from the terminology used in the literature...

[Damiano Testa]

I agree that we should not deviate from established names: I'd rather have preDVR and DVR, rather than using DVD for what everyone else calls a DVR.

[Johan Commelin]

Right, but what about valuation ring?

[Damiano Testa]

Maybe there should be a typeclass that only assumes Mul, since this seems to be all that ValuationRing actually uses? And then we can reserve the ValuationRing name for the more restricted one?

[Riccardo Brasca]

Ruben Van de Velde said:

This one? https://github.com/riccardobrasca/kaplanski4/tree/master

Cc Riccardo Brasca

I am not sure what "this one" refers to, but that repo contains a proof of the fact that an integral domain is a UFD if and only if every nonzero prime ideal contains a prime element. It is not directly related to DVRs.

[Yakov Pechersky]

Kevin Buzzard said:

I think that we shouldn't deviate from the terminology used in the literature...

Ah, but the Kaplansky reference is part of the literature :upside_down:

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib4/pull/17634