Selmer groups of number fields

Stream: maths

[David Ang]

I've been working on a proof of the Mordell-Weil theorem for elliptic curves over number fields, and somewhere in the proof I need the finiteness of an "S-Selmer group", defined to be the (multiplicative) subgroup K(S, n) = {x(Kˣ)ⁿ ∈ Kˣ/(Kˣ)ⁿ | ∀ v ∉ S, ord_v(x) ≡ 0 mod n} of the units Kˣ modulo n-th powers (pow_monoid_hom n).range of a number field K. The main idea is that there's an exact sequence linking this group with the S-class group and the S-unit group, and the finiteness of the S-Selmer group is a consequence of the finiteness of these groups.

I have a fully-working definition (*) of the maps in this exact sequence, as well as sorry-free proofs for their exactness, and its consequent finiteness assuming the finite generation part of Dirichlet's unit theorem, all found in the branch mordell_weil . The definitions are probably generalisable to a Dedekind domain (so that height_one_spectrum makes sense), and the proofs are generalisable to a Dedekind domain whose class group has finite n-torsion, but for now I just need the number field case. I'm at an early stage of trying to PR this into mathlib, but I'm trying to seek some advice before proceeding.

The current definition of height_one_spectrum.valuation takes values in with_zero (multiplicative ℤ) (because 0 is sent to 0), but for the purposes of Selmer groups I'm only looking at Kˣ (so multiplicative ℤ is enough), and in fact I need things like Kˣ/(Kˣ)ⁿ →* multiplicative (zmod n) (so having with_zero is actually bad). How should I define a valuation val_of_ne_zero that takes values in multiplicative ℤ? I thought of several options:

1. Currently I'm composing the existing height_one_spectrum.valuation with an isomorphism (with_zero G)ˣ ≃* G I wrote, but this means I have to unfold this isomorphism whenever I want to use the definition, and I thought it's a bit excessive.
2. I have a separate file that copies the definition for height_one_spectrum.valuation but without the ite, then a separate lemma to prove they're equal whenever an element is non-zero, so I don't have to copy over all the existing API.
3. Perhaps it's worth refactoring all the lemmas for the existing height_one_spectrum.valuation that hold for non-zero elements, including the definition itself?
   Any other suggestions are very welcome.

(*) There is a single sorry at line 92, which surfaced when trying to merge newer versions of mathlib. I used the old definition of height_one_spectrum.valuation from the fractional_ideal.lean file in a separate repository by @María Inés de Frutos Fernández that used is_localization.mk'_surjective, but was later defined in mathlib using is_localization.sec and extend_to_localization, so there is a disconnect that isn't immediately resolvable. I wanted to ask for advice on what I should do before trying to fix this.

[David Ang]

Aside from this, I was also wondering if anyone is working on more facts about unit groups of number fields (especially Dirichlet's unit theorem or even the S-unit theorem), or if anyone is interested in working together for this?

[Eric Rodriguez]

docs#is_dedekind_domain.height_one_spectrum.valuation

[Eric Rodriguez]

I wonder if 1) is the "correct" API approach for a valuation, considering that docs#valuation.unit_map_eq is defined quite early.

[Eric Rodriguez]

and if you have enough simp lemmas then stuff should hopefully work out.

[Eric Rodriguez]

Oh also option 4, not sure how mich people will like it but maybe a docs#units.map' that turns into a K -> with_zero G into a K* -> G

[David Ang]

Eric Rodriguez said:

Oh also option 4, not sure how mich people will like it but maybe a docs#units.map' that turns into a K -> with_zero G into a K* -> G

Yeah, this is ideal as long as we know only 0 is sent to 0, but I'm not sure how to write this without directly/indirectly using the isomorphism in 1.

[Eric Rodriguez]

I mean, what does it matter if you use said isomorphism if you have a zillion simp lemmas sprinkled everywhere?

[David Ang]

Eric Rodriguez said:

I mean, what does it matter if you use said isomorphism if you have a zillion simp lemmas sprinkled everywhere?

Yeah, I was just looking for some other ideas that might be more elegant. @Yaël Dillies has the isomorphism written somewhere else too but just not PR'ed

[David Ang]

I've put 2) in a work-in-progress PR #15405. I thought it might be a bit cleaner than 1), but might just be a bad idea --- can someone have a look?