quadratic fields

Stream: LftCM22

[Kevin Buzzard]

@Daniel Hast @Jackie Lang it would be interesting to do some quadratic field stuff. Here are some thoughts!

[Kevin Buzzard]

I think that a bad idea would be making an explicit model of quadratic fields, e.g. you could imagine a function which eats a squarefree integer d and spits out an explicit quadratic field $\mathbb{Q}(\sqrt{d})$ and then one can go on and prove theorems about that quadratic field. The problem with this is that then when people come along with their own quadratic fields constructed in different ways, they will be isomorphic to the concrete definition but not equal to it, so one would be constantly porting definitions and theorems along isomorphisms.

[Kevin Buzzard]

So perhaps one way to start would be a predicate on number fields (i.e. a function which eats a number field and outputs a true-false statement, saying "I have degree 2 over $\mathbb{Q}$".

[Kevin Buzzard]

That should be easy to do. And now one can start asking questions about this field. For example one could try and prove that there exists a unique squarefree integer $d$ such that the quadratic field is isomorphic to the splitting field of $x^2-d$.

[Kevin Buzzard]

Once one has this, one can then prove the standard facts about what the integers of $\mathbb{Q}(\sqrt{d})$ are.

[Kevin Buzzard]

Let me knock something up.

[Kevin Buzzard]

I could live stream somewhere

[Jackie Lang]

That sounds good; I don't know how to follow your livestream

[Kevin Buzzard]

I'll send you a Zoom link

[Kevin Buzzard]

This https://imperial-ac-uk.zoom.us/j/98307531484?pwd=ejQ3Z2lyaUJlYmRaS01TVlFIRGxtUT09 should work

[Riccardo Brasca]

I am a little busy today and tomorrow, but then I will be happy to join this project

[Daniel Hast]

This project seems interesting to me. I'm still learning a lot of the basics of Lean, but I'll try to contribute to this.

[Filippo A. E. Nuccio]

@Daniel Hast : how is it going?

[Daniel Hast]

Still brushing up on the basic syntax and familiarizing myself with some of the relevant library functions.

[Filippo A. E. Nuccio]

Sounds good! Do not hesitate if you have questions, I am outside the lecture room.

[Chris Birkbeck]

I'm also happy to help out with some quadratic field stuff

[Daniel Hast]

A key lemma that I can't find in mathlib is the following: Given a number field K, the rank of the ring of integers of K (as a Z-module) is equal to the dimension of K (as a Q-vector space). Anyone know if this has been implemented anywhere, either in mathlib or otherwise?

[Johan Commelin]

I'm not sure. @Riccardo Brasca and @Chris Birkbeck know that part of the library best.

[Junyan Xu]

https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Rational.20basis.20of.20a.20number.20field

[Junyan Xu]

To show the algebraic integers span the number field over Q, it would be convenient to use docs#scale_roots. (Linear independence was already done.)

[Chris Birkbeck]

Daniel Hast said:

A key lemma that I can't find in mathlib is the following: Given a number field K, the rank of the ring of integers of K (as a Z-module) is equal to the dimension of K (as a Q-vector space). Anyone know if this has been implemented anywhere, either in mathlib or otherwise?

I don't think we have this in general (or at least I don't know where it is in mathlib) but the link above is a good place to start

[Riccardo Brasca]

This is not in mathlib I think

[Riccardo Brasca]

I am on mobile now, but I am afraid this requires some work

[Riccardo Brasca]

For cyclotomic fields I essentially avoided speaking of integral basis

[Riccardo Brasca]

But we were able to compute the discriminant and the ring of integers

[Chris Birkbeck]

We also know the dimension of the power basis for the ring of integers, so we should almost have it in the cyclotomic case

[Riccardo Brasca]

Note that all the traces/norms one has to consider are relative to the fields extension , even if we apply them to integral elements

[Daniel Hast]

That linear_independent.of_fraction_ring lemma at that link does look useful here; is it also not in mathlib yet? Anyway, I wonder if it would make sense to implement more of the general theory of rings of integers like this before doing the specifics of quadratic rings of integers.

[Riccardo Brasca]

Yes, for cyclotomic fields we have it since we have the ring of integers, using #14981

[Riccardo Brasca]

But in general there is no integral power basis

[Riccardo Brasca]

@Daniel Hast which lemma are you talking t? If it is in mathlib you can write docs#name and it will create an hyperlink to the lemma

[Daniel Hast]

@Riccardo Brasca I meant the lemma at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Rational.20basis.20of.20a.20number.20field/near/271819591 that Junyan linked above. But I searched for that lemma name in mathlib and didn't find anything, so I'm guessing it hasn't made it into mathlib yet.

[Riccardo Brasca]

Ah, I see. If I remember correctly I merged it at some point so it should be there

[Daniel Hast]

Do you know what name it has now?

[Riccardo Brasca]

I don't find it, strange

[Riccardo Brasca]

Give me 5 minutes

[Riccardo Brasca]

The PR is #13041

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

docs#linear_independent.localization

[Riccardo Brasca]

And friends below it

[Chris Birkbeck]

its linear_independent.iff_fraction_ring

[Chris Birkbeck]

oh beat me to it!

[Riccardo Brasca]

@Daniel Hast are you working on quadratic/number fields?

[Daniel Hast]

Yes, I'm working on proving some lemmas for rings of integers of number fields. Currently I'm working on a proof that the rank of the ring of integers is equal to the dimension of the number field over Q.

[Chris Birkbeck]

awesome! If you have any questions or want to post any code here for feedback then don't hesitate to do so.

[Riccardo Brasca]

That is nice! What is your strategy?

[Daniel Hast]

First I'm writing up the proof that some nonzero multiple of an algebraic element is integral. Then I'm going to pretty much follow the standard proof where you show the ring of integers both contains and is contained in modules of the appropriate rank. Might need to prove some lemmas about the trace pairing along the way but I don't know of a simpler approach.

[Daniel Hast]

I might not have time to do all this, though; I'm leaving for PCMI in a few days and will be pretty busy with that for a few weeks.

[Riccardo Brasca]

Already the first result is interesting

[Riccardo Brasca]

It allows to define the discriminant of a number field

[Riccardo Brasca]

As a well defined integer

[Riccardo Brasca]

(and a well defined ideal in the relative case)

[Daniel Hast]

I'm sure I've done lots of inefficient or clunky things here, but I did complete the proof that an algebraic element has a nonzero multiple that's integral:

variables (A K C : Type*) [comm_ring A] [is_domain A] [field K] [algebra A K] [is_fraction_ring A K] [comm_ring C]

lemma algebraic_has_integral_multiple [algebra A C] [algebra K C] [is_scalar_tower A K C] {x : C} :
  is_algebraic K x → (∃ d : A, d ≠ 0 ∧ is_integral A (x * (algebra_map A C) d)) :=
begin
  intro h,
  rw ← is_algebraic_iff A K C at h,
  cases h with f hf,
  use f.leading_coeff,
  split,
  {
    apply polynomial.coeff_ne_zero_of_eq_degree,
    rw polynomial.degree_eq_iff_nat_degree_eq hf.left,
  },
  by_cases x_zero : x = 0,
  { use polynomial.X, simp [x_zero], },
  use polynomial.integral_normalization f,
  split,
  { exact polynomial.monic_integral_normalization hf.left, },
  nontriviality C,
  have inj : ∀ (a : A), (algebra_map A C) a = 0 → a = 0, begin
    intros a ha,
    apply is_fraction_ring.to_map_eq_zero_iff.mp,
    apply (algebra_map K C).map_eq_zero.mp,
    rw ← ha,
    rw eq_comm,
    exact is_scalar_tower.algebra_map_apply A K C a,
    assumption,
  end,
  exact polynomial.integral_normalization_eval₂_eq_zero (algebra_map A C) hf.right inj,
end

[Kevin Buzzard]

  split,
  { exact polynomial.monic_integral_normalization hf.left, },

could be

refine ⟨polynomial.monic_integral_normalization hf.left, _⟩,

: basically refine \<_, _\> is the same as split but you can sometimes save a line with this trick.

[Daniel Hast]

...and now I just found that this is basically already exists in mathlib at ring_theory.dedekind_domain.integral_closure.exists_integral_multiples. The statements aren't identical but the slight extra generality in the version I wrote isn't actually relevant to the application to rings of integers. Oh well!

[Riccardo Brasca]

That's super nice! It is actually not enough to define the discriminant, but we are not far.

[Riccardo Brasca]

My idea is to use docs#algebra.discr_eq_discr_of_to_matrix_coeff_is_integral

[Riccardo Brasca]

And in any case it is better to be as general as possible :D

[Riccardo Brasca]

I am thinking about the freeness of 𝓞 K. We know that torsion free implies free for PID, so this is probably the fastest way to get there.

[Riccardo Brasca]

And once we now that 𝓞 K is free it should be easy to prove that it has the right rank.

[Riccardo Brasca]

See docs#module.free_of_finite_type_torsion_free'

[Kevin Buzzard]

Daniel Hast said:

...and now I just found that this is basically already exists in mathlib at ring_theory.dedekind_domain.integral_closure.exists_integral_multiples. The statements aren't identical but the slight extra generality in the version I wrote isn't actually relevant to the application to rings of integers. Oh well!

It's good practice! Your code looked very nice to me. The library is huge and it's hard to get on top of everything that is there quickly. This comes from experience. Thanks a lot for your efforts on this -- it's about time we got number fields into a solid state.

[Riccardo Brasca]

Do we know that 𝓞 K is finite as ℤ-module?

[Riccardo Brasca]

Hmm, I am afraid we don't

[Riccardo Brasca]

OK, we probably need to follow the classical proof, but all the ingredients are there. Take x such that K = ℚ(x), with x an algebraic integer. We know that ℤ[x] is finite, and to prove that 𝓞 K is finite we can use docs#algebra.discr_mul_is_integral_mem_adjoin

[Riccardo Brasca]

@Daniel Hast if you want a precise goal that I am pretty sure it is not in mathlib, we need a docs#power_basis B of K such that B.gen is integral. We surely have a way to produce a power basis of K (over ℚ), and the rest shouldn't be too difficult.

[Junyan Xu]

Daniel Hast said:

... I did complete the proof that an algebraic element has a nonzero multiple that's integral:

variables (A K C : Type*) [comm_ring A] [is_domain A] [field K] [algebra A K] [is_fraction_ring A K] [comm_ring C]
lemma algebraic_has_integral_multiple [algebra A C] [algebra K C] [is_scalar_tower A K C] {x : C} :
  is_algebraic K x → (∃ d : A, d ≠ 0 ∧ is_integral A (x * (algebra_map A C) d)) :=

I am able to prove a possibly overly general version of the result:

variables {A B C : Type*} [comm_ring A] [comm_ring B] [comm_ring C]
  [algebra A B] [algebra A C] [algebra B C] [is_scalar_tower A B C]
lemma eq_smul_is_integral_of_is_localization (M : submonoid A) [is_localization M B] {x : C}
  (h : is_integral B x) : ∃ y : C, is_integral A y ∧ ∃ d : B, is_unit d ∧ x = d • y :=

I think it's strictly more general, because if B is a field then we have docs#algebra.is_algebraic_iff_is_integral. The full proof is at this gist and uses two lemmas, and one of them I believe is of some general interest:

lemma eq_map_of_frange_subset_srange {A B} [semiring A] [semiring B] (f : A →+* B)
  (p : B[X]) (hp : ↑p.frange ⊆ (f.srange : set B)) :
  ∃ q : A[X], p = q.map f ∧ q.nat_degree = p.nat_degree ∧ (p.monic → q.monic) :=

Its proof would be much easier if f is injective because f.srange would then be isomorphic to A and we can use docs#polynomial.map. I might PR them some time but feel free to PR them for me if you need the result soon.

[Riccardo Brasca]

Since this is strictly more general than a lemma already in the library I suggest to PR it as soon as possible. Short PRs are very welcome, and generalization is usually uncontroversial, so it can be merged quickly and then it won't be your problem to maintain the proof. (Mathlib changes very quickly, so a proof working today can be broken tomorrow.)