Ramification iff divides discriminant

Stream: Is there code for X?

[Gareth Ma]

Does the following theorem exist?

image.png - Milne AlgNT

For non-infinite primes of number fields, it seems that there is no direct notion for "a prime ramifies". Should it exist or is Mathlib happy with 0 < ramificationIdx something?

[Andrew Yang]

It’s essentially docs#pow_sub_one_dvd_differentIdeal

[Riccardo Brasca]

In flt-regular we have a notion of being unramified at a prime. We didn't need connection with the discriminant, but all the prerequisites are there.

[Andrew Yang]

Andrew Yang said:

It’s essentially docs#pow_sub_one_dvd_differentIdeal

(at least one direction of it)

[Thomas Browning]

Andrew Yang said:

It’s essentially docs#pow_sub_one_dvd_differentIdeal

Does that tell you that ramify implies divides discriminant, but not divides discriminant implies ramifies?

[Thomas Browning]

For something I'm working on, I'll need to know that every number field has at least one ramified prime, which requires the opposite direction.

[Riccardo Brasca]

I think it's time to have the discriminant ideal!

[Riccardo Brasca]

Thomas Browning said:

For something I'm working on, I'll need to know that every number field has at least one ramified prime, which requires the opposite direction.

Note that the hard part of this result, Minkowski bound, is in mathlib.

[Gareth Ma]

In fact there's

Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
18:* `NumberField.abs_discr_gt_two`: **Hermite-Minkowski Theorem**. A nontrivial number field has
192:theorem abs_discr_gt_two (h : 1 < finrank ℚ K) : 2 < |discr K| := by

[Gareth Ma]

(I saw this but nothing like "Q has no unramified extensions", hence this question.) I think the IsUnramified{At} notion from flt-regular should be brought to Mathlib, seems natural at least to me

[Riccardo Brasca]

Yes, I mean we know all we need about the discriminant, we are missing the connection between the discriminant and remification.

[Riccardo Brasca]

If you want to PR those results please feel free to do so

[Riccardo Brasca]

I am in the process of moving stuff from flt-regular to mathlib, but currently working on other results

[Gareth Ma]

Oh yeah I just meant even the Minkowski bound => discr > 1 part is done :D

[Gareth Ma]

I'm probably not free to do it myself, sorry :(

[Riccardo Brasca]

But I don't think we should spend too much time with the discriminant as an integer, we need the ideal

[Riccardo Brasca]

And this does not exist I think

[Riccardo Brasca]

@Andrew Yang you mentionned that someone else was working on improving the status of primeOver or something similar. Is this done?

[Andrew Yang]

I belieive the mathlib counter part for primeOver is docs#Ideal.LiesOver. And I think @Thomas Browning's frobenius element work will give a better framework for the remaining parts of galoisPrime.lean too.

[Kevin Buzzard]

PS the hypothesis that B is free as an A-module is not necessary. I'm guessing that Milne (incorrectly) only defines the discriminant in this situation?

[Riccardo Brasca]

We have a lot of places where we can remove freeness :(

[David Loeffler]

Kevin Buzzard said:

PS the hypothesis that B is free as an A-module is not necessary. I'm guessing that Milne (incorrectly) only defines the discriminant in this situation?

"Incorrectly" is a bit harsh; maybe his results are not maximally general, but that doesn't mean they aren't correct, and clearly the most important case is A = ZZ.

[Gareth Ma]

Kevin Buzzard said:

PS the hypothesis that B is free as an A-module is not necessary. I'm guessing that Milne (incorrectly) only defines the discriminant in this situation?

Correct!

[Gareth Ma]

image.png

But as David said $A = \mathbb{Z}$ is important and PID most of the time

[Gareth Ma]

Ahh but I guess a subsequent question I should ask first is does anyone have an introductory reference that also removes the hypothesis?

[Riccardo Brasca]

In general you take all integral bases of L as K-vector space, and the discriminant lies in 𝓞 K. You don't need 𝓞 L to be free as 𝓞 K-module.

[Riccardo Brasca]

It's called the "relative discriminant". Neukirch surely explains it

[Riccardo Brasca]

You can also look at "Local Fields", chapter II for a more abstract approach

[Gareth Ma]

:man_facepalming: how did I forget about Neukirch. (p.201)

[Gareth Ma]

Random side note, but Wikipedia has a section on it as well, but their field extension is somehow $K / L$ and adjacent things written a bit weirdly :/

[Gareth Ma]

I guess this is a Lean/Mathlib question rather than a math question, but are there better ways to write relDiscr? And is the discr ℤ (integralBasis K) part correct?

import Mathlib

open NumberField Algebra

-- Relative discriminant (ideal) of field extension L/K
set_option linter.unusedVariables false
def relDiscr (L K : Type*) [Field K] [Field L] [Algebra K L] : Ideal (𝓞 K) :=
  Ideal.span { d |
    ∃ (ι : Type*) (inst₁ : DecidableEq ι) (inst₂ : Fintype ι) (b : Basis ι K L),
    ∀ i, IsIntegral K (b i) ∧ discr K b = d }

-- Relative discriminant of K/ℚ is just principal ideal of absolute discriminant disc(K)
example (K : Type*) [Field K] [NumberField K] :
    (relDiscr K ℚ).map Rat.ringOfIntegersEquiv = Ideal.span { discr ℤ (integralBasis K) } := by
  sorry

[Riccardo Brasca]

Note that we also have NumberField.discr

[Riccardo Brasca]

For the absolute discriminant you should definitely use that

[Gareth Ma]

Yes, sorry I didn't know that haha

[Riccardo Brasca]

For the relative one I am not sure. Maybe we can go via the different

[Riccardo Brasca]

cc @Xavier Roblot

[Xavier Roblot]

I would use a definition similar to the one you give for the relative discriminant but for all families, not just bases.

import Mathlib

open NumberField Algebra

open Classical in
def relDiscr (L K : Type*) [Field K] [Field L] [Algebra K L] : Ideal (𝓞 K) :=
  Ideal.span { d | ∃ (ι : Type*) (_ : Fintype ι) (v : ι → 𝓞 L),
    Algebra.discr K (fun i ↦ (v i : L)) = d }

[Kevin Buzzard]

I think differents exist in some huge generality. Aren't they used in the theory of finite flat group schemes?

[Andrew Yang]

What's the definition in that case? The annihilator of the sheaf of differentials?

[Kevin Buzzard]

I have some old notes of Conrad where he goes through all this and my instinct is to refer you to these, but they appear to be no longer on his website. When I get home later I'll see if I can dig them out.

[Kevin Buzzard]

Sorry for the delay -- home now. This is from Conrad--Lieblich "Galois Representations Arising from p-Divisible Groups", a mythical text which Brian seems to have removed from his website. I have no idea whether it got published.

Screenshot from 2024-11-16 17-27-41.png

[Kevin Buzzard]

I don't know of any published reference which works in this generality, I'm just saying I trust Brian.

[Andrew Yang]

I managed to find the same text at Lieblich’s website here.

[Riccardo Brasca]

Riccardo Brasca said:

We have a lot of places where we can remove freeness :(

See for example #19244 for a generalization of the relative norm

[Antoine Chambert-Loir]

The reference I would have looked at for these questions is the old paper by Mazur and Roberts (1970), “Local Euler Characteristics” , Invent. Math. 9, p. 201–234. doi:10.1007/BF01404325 The appendix should be something like that.

[Andrew Yang]

@Thomas Browning said:

For something I'm working on, I'll need to know that every number field has at least one ramified prime, which requires the opposite direction.

Are there any updates on this? Both divides discriminant => ramified and Q has no nontrivial unramified extensions.

[Riccardo Brasca]

I didn't see anything related to this recently.

[Riccardo Brasca]

Waiting for the PR :stuck_out_tongue:

[Thomas Browning]

No, I'm not aware of any progress on this. But there is progress on inertia groups with #20899 and #21770.

[Andrew Yang]

I’ll try to think about this then.