Finiteness of residue fields for number fields

Stream: Is there code for X?

[Kevin Buzzard]

We have finiteness of the class group of a number field but I can't find finiteness of the residue fields, which is much easier! Furthermore I am not entirely sure whether I should be just proving it for the ring of integers (approach 2) or more generally (approach 1). Do we have any of these?

import Mathlib

-- approach 1

open IsDedekindDomain

variable (A : Type*) [CommRing A] [IsDedekindDomain A] (K : Type*) [Field K] [NumberField K] [Algebra A K]
    [IsFractionRing A K]

example (I : Ideal A) (hI : I ≠ 0) : Finite (A ⧸ I) := by sorry

-- weaker statement which is all I need
variable (v : HeightOneSpectrum A) in
example : Finite (A ⧸ v.asIdeal) := sorry

-- approach 2

open NumberField

variable (L : Type*) [Field L] [NumberField L] (w : HeightOneSpectrum (𝓞 L))

example (I : Ideal (𝓞 L)) (hI : I ≠ 0) : Finite ((𝓞 L) ⧸ I) := by sorry

-- weaker statement which is all I need
example : Finite ((𝓞 L) ⧸ w.asIdeal) := sorry

[Kevin Buzzard]

The first approach looks like more of a kerfuffle but it applies more generally (e.g. for S-integers) and also means that for $\mathbb{Q}$ you're able to use $\mathbb{Z}$. However I don't need either of these for my current work.

[Yakov Pechersky]

The bottom is usually done via docs#IsLocalRing.ResidueField

[Yakov Pechersky]

So you have to show that w.asIdeal is equal to IsLocalRing.maximalIdeal

[Kevin Buzzard]

But this is global not local; 𝓞 L is far from local (an example would be the integers).

[Yakov Pechersky]

Ah, apologies.

[Kevin Buzzard]

In fact I also want to relate the residue field to the residue field of the completion, that's the next question. I'd like to prove that the residue field of v.adicCompletionIntegers is finite in the number field case, and I figured I'd do it by identifying it with the global residue field and then using the results above.

[Matthew Jasper]

Ideal.absNorm (and some of the following results) are probably what you want

[Kevin Buzzard]

Interestingly that doesn't look general enough for the first approach; it asks that the ring is free as a Z-module, which is not true for e.g. Z[1/p].

[Matthew Jasper]

The first approach is missing an assumption on A or K though

[Kevin Buzzard]

Oh sorry! You're absolutely right! I've edited to add the missing NumberField assumption. You're exactly right that it's nonsense without that assumption.

[Andrew Yang]

docs#Ideal.fintypeQuotientOfFreeOfNeBot

[Kevin Buzzard]

That also assumes that A is Z-free so doesn't apply to S-integers, but it will apply to the second approach.

[Andrew Yang]

I thought finite char 0 domain over Z is free because of PID things?

[Kevin Buzzard]

For the first approach, note that A is not remotely uniquely determined by K; indeed even if K is the rationals there are uncountably many choices for A up to isomorphism! For any set of primes you can let A be the rationals whose denominators only have prime factors in this set. So you can't reduce to the second approach. But I personally don't care about the generality of the first approach; the only advantage of it is that I might have to deal with \MCO \Q, but I've had to deal with this before and it's not too bad (it's known to be isomorphic to \Z in mathlib and this is usually enough)

[Andrew Yang]

Oh you are taking the localization so its not finite I see.

[Kevin Buzzard]

I mean, in practice I'm not, it's just that I am slightly wary of tying myself down to the ring of integers because of this Z vs O_Q thing, and it's true for any localization which is why I asked.

[Kevin Buzzard]

Our definition of finite adeles was refactored to allow a general A whose field of fractions was K so everything works in this generality, although I've never needed it because the one time I wanted to do calculations with the adeles of Q and was so scared of its integer ring that I made the refactor, I then discovered that working with the integers of Q was fine.

[Kevin Buzzard]

Maybe I'll just stick to approach 2 for now, especially given that we have everything already to deal with that situation.

[Kevin Buzzard]

Related: I guess we may then not have finiteness of class groups for S-integers?

[Jz Pan]

Kevin Buzzard said:

Related: I guess we may then not have finiteness of class groups for S-integers?

Prove that it's a quotient of the usual class group so it's also finite?

[Jz Pan]

I think your approach 2 should imply approach 1. To prove approach 1 you only need to prove it for all maximal ideal thanks to unique factorization of ideals. Then any such A is automatically a localization of 𝓞 K. So if suffices to prove the result for 𝓞 K.

[Antoine Chambert-Loir]

The ring of integers $R$ of a number field is a free $$\mathbf Z$$$-module of finite rank, and if an ideal $I$ is nonzero, then it contains a nonzero integer $n$ (the norm of any nonzero element) , which implies that the quotient $R/I$ is a quotient of $R/nR$, which is finite.

[Kevin Buzzard]

This is no good for approach 1 though which allows S-integers

[Jz Pan]

Kevin Buzzard said:

This is no good for approach 1 though which allows S-integers

Is it possible to prove that any Dedeking domains whose fraction ring is a number field is a localization of the ring of integers of that field?

[Junyan Xu]

It was discussed in #maths > ✔ S-integers and S-units @ 💬 and the conclusion was that this is true whenever the class group is finite torsion (in particular for number fields).

[Antoine Chambert-Loir]

Do we have the Nullstellensatz in its Zariski version (a finitely generated $k$-algebra which is a field is finite over $k$)? Then residue fields (for any maximal ideal of a finitely generated $\mathbf Z$-algebra) could be proved to be finite. Also, dimension theory would prove that nonzero ideals have finite co-height.

[Antoine Chambert-Loir]

By the way, the above approach seems to work for $S$-integers, because $\mathbf Z_S/n$ is finite, it is a quotient (!) of $\mathbf Z/n\mathbf Z$.

[Andrew Yang]

nullstellensatz is docs#finite_of_finite_type_of_isJacobsonRing

[Antoine Chambert-Loir]

If one wishes for a proof standing on very general principles, I'd combine these two:

• If $R$ is a noetherian integral domain of dimension 1 and $I$ is a nonzero ideal of $R$, then $R/I$ has finite length.

• If $R$ is a finitely generated $\mathbf Z$-algebra, then all residue fields of $R$ are finite fields.

[Jz Pan]

Antoine Chambert-Loir said:

• If $R$ is a noetherian integral domain of dimension 1 and $I$ is a nonzero ideal of $R$, then $R/I$ has finite length.

... which means that $R/I$ is Artinian ring.

[Junyan Xu]

import Mathlib.RingTheory.DedekindDomain.Basic
import Mathlib.RingTheory.HopkinsLevitzki

variable {R : Type*} [CommRing R] [Ring.DimensionLEOne R] (I : Ideal R) (hI : I ≠ ⊥)
include hI

lemma Ideal.ringKrullDimLE_zero_quotient : Ring.KrullDimLE 0 (R ⧸ I) :=
  Ring.krullDimLE_zero_iff.mpr fun J prime ↦
    isMaximal_of_isIntegral_of_isMaximal_comap _ <| (prime.comap (Quotient.mk I)).isMaximal
      (hI.bot_lt.trans_le <| mk_ker.ge.trans <| J.ker_le_comap _).ne'

lemma isArtinianRing_quotient [IsNoetherianRing R] : IsArtinianRing (R ⧸ I) :=
  have := I.ringKrullDimLE_zero_quotient hI
  IsNoetherianRing.isArtinianRing_of_krullDimLE_zero

[IsDomain R] is not needed because it's implicit in the definition of Ring.DimensionLEOne.

[Jz Pan]

Junyan Xu said:

it's implicit in the definition of Ring.DimensionLEOne

Oops. Why are there duplicate APIs (Ring.KrullDimLE)?

[Junyan Xu]

Ring.KrullDimLE is new. Ring.DimensionLEOne should be replaced by it IMO.

[Andrew Yang]

Because Ring.DimensionLEOne is very wrong. See #mathlib4 > Dedekind ring @ 💬

[Jz Pan]

Andrew Yang said:

is very wrong

... same as docs#IsDedekindDomain.HeightOneSpectrum which is in fact non-zero prime ideals, hence wrong for non-Dedekind rings

[Yongle Hu]

Kevin Buzzard 发言道：

We have finiteness of the class group of a number field but I can't find finiteness of the residue fields, which is much easier! Furthermore I am not entirely sure whether I should be just proving it for the ring of integers (approach 2) or more generally (approach 1). Do we have any of these?

I think we proved

example (I : Ideal (𝓞 L)) (hI : I ≠ 0) : Finite ((𝓞 L) ⧸ I) := by sorry

in a previous project.

[Yongle Hu]

Oh, I think this is the same as the proof using docs#Ideal.finiteQuotientOfFreeOfNeBot that @Andrew Yang pointed out earlier.