Algebraic number theory

Stream: maths

[Riccardo Brasca]

I am going to upstream what we have in flt-regular about the different ideal, unramified extensions of number fields and stuff about ideal norm in non free extensions (all the credits to @Andrew Yang ). Just posting here in case anyone needs/is interested in working about those subjects.

[Andrew Yang]

IIRC someone (maybe in the FLT project) is redoing galoisPrime.lean using a better approach (e.g. docs#Ideal.LiesOver) which might block the porting of the results on unramified extensions.

[Andrew Yang]

I think its @Yongle Hu ?

[Riccardo Brasca]

@Andrew Yang I saw your comment in flt-regular. I promise I will PR everything to mathlib, even if I erased something from the repo (it's like 5 results).

[Andrew Yang]

The other things are indeed useless though; they are completely subsumed by other results.
I was trying to get away from developing the whole different ideal thing by proving a weaker statement but turns out they weren't enough.

[Yongle Hu]

Andrew Yang said:

IIRC someone (maybe in the FLT project) is redoing galoisPrime.lean using a better approach (e.g. docs#Ideal.LiesOver) which might block the porting of the results on unramified extensions.

I have written the ramification theory of Galois extensions of number fields using docs#Ideal.LiesOver (see here). I will try to translate them into the form of extensions of Dedekind domains later (following what has already been done in flt-regular).

[Riccardo Brasca]

Nice! We are not in a hurry, I just wanted to avoid work duplication.

[Yongle Hu]

And I have a question. Although the A K L B setup is more general, it might be more convenient to prove and use results without involving K L and only assuming IsGalois (FractionRing A) (FractionRing B) alone (for example, Algebra.algebraMap_intNorm_of_isGalois is also proven only under this assumption). Which setting would be better to use?

[Riccardo Brasca]

I think it is better to use the A K L B setup, at least in the final results. The reason is that maybe at some point someone will be in the situation of having "a fraction field", rather then FractionRing A.

[Riccardo Brasca]

but one strategy is to prove everything for FractionRing A, and then deduce the interesting stuff for any K.

[Andrew Yang]

If we redefine IsGalois A B to be an integral extension such that A is the fixed subring of B by $\operatorname{Aut}(B/A)$ then IsGalois A B <-> IsGalois (FractionRing A) (FractionRing B) (at least for finite extensions) and we won't even have to mention FractionRing in that statement.

[Andrew Yang]

Riccardo Brasca said:

but one strategy is to prove everything for FractionRing A, and then deduce the interesting stuff for any K.

This is kind of painful though which is why we switched to A K L B in fltregular instead.

[Andrew Yang]

Yongle Hu said:

Which setting would be better to use?

My rule of thumb when doing fltregular was to use FractionRing for typeclass arguments only when FractionRing does not appear anywhere else in the statement.

[Antoine Chambert-Loir]

The definition suggested by @Andrew Yang looks nice at first sight but is not consistent with the practice in algebraic geometry (hence would not resist the transfer to schemes) where Galois has an “étale” character — and is stable under base change. I'd also guess that the notion is not so well behaved when the rings are not domains (it seems it is stable under localization, though).

[Andrew Yang]

That's true but the original definition (normal + separable) isn't the right one in that setting too I think?

[Adam Topaz]

Maybe IsBranchedGalois is a more appropriate name for this definition?