Rings with finite quotients

Stream: maths

[Xavier Roblot]

While working on decomposition fields and inertia fields, I need to consider rings S such that S ⧸ I is finite for a nonzero ideal I. In the case where S is a finite ℤ-module, we have docs#Ideal.finiteQuotientOfFreeOfNeBot, but there are certainly more cases when this is true. What is the right generality for that? Maybe we need something like Ring.hasFiniteQuotient

[Kevin Buzzard]

You presumably also don't allow $I=S$? But you do allow $\Z/4\Z$? Why can't this just be a condition on the prime ideal you're making the decomposition and inertia field for? It's not just the existence of I you need, presumably?

[Aaron Liu]

Do you want every quotient by a nonzero ideal to be finite? (That's the conclusion of the theorem you linked)

[Xavier Roblot]

Sorry, I meant S ⧸ I is finite for all nonzero ideals I

[Kevin Buzzard]

So probably 1-dimensional, maybe finite rings and S-integers in local and global fields are going to be the main examples

[Riccardo Brasca]

@Antoine Chambert-Loir I think we discussed if there was a reasonable typeclass for this, but I don't remember our conclusion.

[Kevin Buzzard]

class ClassFieldTheoryWorksForMe

[Kevin Buzzard]

Oh and of course all fields ;-)

[Riccardo Brasca]

Anyway if this is the literal condition you need I don't see any problem in making it a class.

[Xavier Roblot]

To be more precise, here is the situation that I have: let R ⊆ S be a extension of rings (in most cases that I consider, they are actually Dedekind domains) such that Module.Finite R S and let P be a maximal ideal of S above the maximal ideal p of R, then I need to know that IsGalois (R ⧸ p) (S ⧸ P).

If R ⧸ p and S ⧸ P are finite, this follows directly by docs#GaloisField.instIsGaloisOfFinite (and docs#Ideal.Quotient.field).

[Xavier Roblot]

@Kevin Buzzard said:

So probably 1-dimensional, maybe finite rings and S-integers in local and global fields are going to be the main examples

Wait, are you sure 1-dimensional rings have finite quotients? If so, then HasFiniteQuotient is equivalent to DimensionLEOne since the other direction is easily proved.

[Aaron Liu]

I think polynomials over an infinite field definitely fail this condition, but

import Mathlib

variable {K : Type*} [Field K]

#synth Ring.DimensionLEOne (Polynomial K)

[Riccardo Brasca]

I think that what Kevin means is that an infinite ring has this property then it is 1-dimensional (not sure if this is true without any other assumption, but it looks reasonable).

[Xavier Roblot]

Riccardo Brasca said:

I think that what Kevin means is that an infinite ring has this property then is 1-dimensional (not sure if this is true without any other assumption, but it looks reasonable).

Yes, I proved that. Well, actually I proved that HasFiniteQuotient implies DimensionLEOne

[Kevin Buzzard]

Yeah, the difference between "a 1-d Dedekind domain" and "a 1-d Dedekind domain for which class field theory applies to its field of fractions" is precisely some kind of finiteness hypothesis which implies, but might not be equivalent to, finiteness of all residue fields.

[Kevin Buzzard]

This is why I think of Dedekind domains as algebra but integers of local and global fields as arithmetic.

[Kevin Buzzard]

I was once hoping it was as simple as "finite residue fields" but then someone pointed me to some paper which gave some much more subtle conditions. Here's a question I don't know the answer to: if a 1-d integral domain has finite residue fields, is its class group finite? Maybe a careful reading of the proof will prove this but I'm not sure, I think you might need a bit more.

[Kevin Buzzard]

Oh I guess orders in global fields also satisfy this finiteness hypothesis, i.e. the curve doesn't have to be smooth.

[Riccardo Brasca]

I've asked chatGPT about the finiteness of the class group and it answered "What I’m less confident about off the top of my head is whether Claborn-style realizations can always be arranged while also forcing all residue fields to be finite; many can, but I don’t want to assert “always” without checking". I think it's the first time I see an LLM saying "I don't know" without trying to cheat. Maybe it's a good sign.

[Xavier Roblot]

What are Claborn-style realizations?

[Antoine Chambert-Loir]

But nonconnected Dedekind rings with co-finite maximal ideals won't satisfy the property.

[Riccardo Brasca]

Xavier Roblot said:

What are Claborn-style realizations?

The fact that any abelian group is the class group of a Dedekind domain.

[Riccardo Brasca]

On the other hand I found this mathoverflow question that is relevant.

[Riccardo Brasca]

In particular is seems there are Dedekind domains with infinite class group and finite residue fields.

[Xavier Roblot]

#35530