Zulip Chat Archive

Stream: LftCM22

Topic: quadratic fields


Kevin Buzzard (Jul 11 2022 at 18:58):

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

Kevin Buzzard (Jul 11 2022 at 19:00):

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 Q(d)\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 (Jul 11 2022 at 19:01):

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 Q\mathbb{Q}".

Kevin Buzzard (Jul 11 2022 at 19:02):

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 dd such that the quadratic field is isomorphic to the splitting field of x2dx^2-d.

Kevin Buzzard (Jul 11 2022 at 19:03):

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

Kevin Buzzard (Jul 11 2022 at 19:03):

Let me knock something up.

Kevin Buzzard (Jul 11 2022 at 19:03):

I could live stream somewhere

Jackie Lang (Jul 11 2022 at 19:04):

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

Kevin Buzzard (Jul 11 2022 at 19:04):

I'll send you a Zoom link

Kevin Buzzard (Jul 11 2022 at 19:05):

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

Riccardo Brasca (Jul 11 2022 at 19:21):

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

Daniel Hast (Jul 11 2022 at 19:34):

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 (Jul 11 2022 at 20:05):

@Daniel Hast : how is it going?

Daniel Hast (Jul 11 2022 at 20:13):

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

Filippo A. E. Nuccio (Jul 11 2022 at 20:13):

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

Chris Birkbeck (Jul 12 2022 at 08:06):

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

Daniel Hast (Jul 12 2022 at 15:50):

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 (Jul 12 2022 at 15:55):

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

Junyan Xu (Jul 12 2022 at 15:56):

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

Junyan Xu (Jul 12 2022 at 16:02):

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 (Jul 12 2022 at 16:08):

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 (Jul 12 2022 at 16:09):

This is not in mathlib I think

Riccardo Brasca (Jul 12 2022 at 16:10):

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

Riccardo Brasca (Jul 12 2022 at 16:11):

For cyclotomic fields I essentially avoided speaking of integral basis

Riccardo Brasca (Jul 12 2022 at 16:12):

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

Chris Birkbeck (Jul 12 2022 at 16:13):

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 (Jul 12 2022 at 16:14):

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 (Jul 12 2022 at 16:14):

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 (Jul 12 2022 at 16:14):

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

Riccardo Brasca (Jul 12 2022 at 16:14):

But in general there is no integral power basis

Riccardo Brasca (Jul 12 2022 at 16:22):

@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 (Jul 12 2022 at 16:24):

@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 (Jul 12 2022 at 16:25):

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

Daniel Hast (Jul 12 2022 at 16:26):

Do you know what name it has now?

Riccardo Brasca (Jul 12 2022 at 16:27):

I don't find it, strange

Riccardo Brasca (Jul 12 2022 at 16:27):

Give me 5 minutes

Riccardo Brasca (Jul 12 2022 at 16:28):

The PR is #13041

Riccardo Brasca (Jul 12 2022 at 16:28):

(deleted)

Riccardo Brasca (Jul 12 2022 at 16:30):

docs#linear_independent.localization

Riccardo Brasca (Jul 12 2022 at 16:31):

And friends below it

Chris Birkbeck (Jul 12 2022 at 16:31):

its linear_independent.iff_fraction_ring

Chris Birkbeck (Jul 12 2022 at 16:31):

oh beat me to it!

Riccardo Brasca (Jul 13 2022 at 14:48):

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

Daniel Hast (Jul 13 2022 at 14:51):

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 (Jul 13 2022 at 15:03):

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

Riccardo Brasca (Jul 13 2022 at 15:20):

That is nice! What is your strategy?

Daniel Hast (Jul 13 2022 at 15:28):

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 (Jul 13 2022 at 15:29):

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 (Jul 13 2022 at 15:50):

Already the first result is interesting

Riccardo Brasca (Jul 13 2022 at 15:50):

It allows to define the discriminant of a number field

Riccardo Brasca (Jul 13 2022 at 15:50):

As a well defined integer

Riccardo Brasca (Jul 13 2022 at 15:51):

(and a well defined ideal in the relative case)

Daniel Hast (Jul 13 2022 at 19:05):

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 (Jul 13 2022 at 19:57):

  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 (Jul 13 2022 at 19:57):

...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 (Jul 13 2022 at 20:00):

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

Riccardo Brasca (Jul 13 2022 at 20:01):

My idea is to use docs#algebra.discr_eq_discr_of_to_matrix_coeff_is_integral

Riccardo Brasca (Jul 13 2022 at 20:04):

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

Riccardo Brasca (Jul 13 2022 at 20:16):

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 (Jul 13 2022 at 20:16):

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

Riccardo Brasca (Jul 13 2022 at 20:17):

See docs#module.free_of_finite_type_torsion_free'

Kevin Buzzard (Jul 13 2022 at 20:19):

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 (Jul 13 2022 at 20:28):

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

Riccardo Brasca (Jul 13 2022 at 20:31):

Hmm, I am afraid we don't

Riccardo Brasca (Jul 13 2022 at 20:44):

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 (Jul 13 2022 at 20:47):

@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 (Jul 16 2022 at 05:39):

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 (Jul 16 2022 at 12:31):

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.)


Last updated: Dec 20 2023 at 11:08 UTC