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.