Zulip Chat Archive
Stream: general
Topic: Embeddings of a number field
Xavier Roblot (Jun 19 2022 at 12:53):
I am currently working on defining and proving basic results on the embeddings of a number field K
into an algebraic closed field A
of char. 0. There are two natural choices to define those: we can see them as plain ring homomorphisms K →+* A
or as $\mathbb{Q}$algebra homomorphisms K →ₐ[ℚ] A
. Of course, these are equivalent thanks to docs#ring_hom.equiv_rat_alg_hom.
The goal of this thread is to discuss between these two choices and come up (hopefully) with a decision.
Kevin Buzzard (Jun 19 2022 at 12:57):
I would go with plain ring homomorphisms. There are diamonds lurking here IIRC. Why not keep things as simple as possible? I would love to see a proof of the formula for the rank of the unit group of a number field btw!
Xavier Roblot (Jun 19 2022 at 12:57):
/poll Embeddings of a number field
Ring hom. K →+* A
Alg. hom. K →ₐ[ℚ] A
Riccardo Brasca (Jun 19 2022 at 12:59):
I agree with Kevin. The algebra_rat
diamond is really annoying.
Reid Barton (Jun 19 2022 at 12:59):
I would also guess that many of the basic things you can prove about these will work in any characteristic.
Reid Barton (Jun 19 2022 at 14:38):
Oh but then you would also want to work over the base field, which might not be a prime field.
Anne Baanen (Jun 20 2022 at 08:24):
Riccardo Brasca said:
I agree with Kevin. The
algebra_rat
diamond is really annoying.
@Alex J. Best did you get around to dealing with this diamond in the last days? Otherwise I'd like to take a shot at it this afternoon.
Alex J. Best (Jun 20 2022 at 13:22):
No I didn't look at this one got too distracted by eta for structures type diamonds.
Junyan Xu (Jun 20 2022 at 14:25):
Anyone assessed difficulty of backporting structure eta defeq?
Xavier Roblot (Nov 14 2022 at 10:18):
I am reviving this old thread to discuss the next step after embeddings of a number field that is places of a number field.
For K
a number field and φ : K →+* A
an embedding into a normed_division_ring A
, I define the place associated to φ
by place K φ := norm ∘ φ
. (I guess at some point I should prove that all the places of K
 in the usual sense of equivalent classes of absolute values , are obtained that way. I am not sure if Ostrowski theorem is in Lean yet.) I am interested to know if people agree with this definition or have some better ideas on how to proceed.
For the moment, I am working on infinite places of K
, that is the case A = ℂ
. I have proved (with some difficulties) that two embeddings into ℂ
define the same infinite place iff they are equal or complex conjugate (#17285, still WIP). My next step is to prove that the number of places defined by real embeddings is the number of real embeddings and the number of places defined by complex embeddings is half the number of complex embeddings. Well, in fact, I have an almost complete proof of these facts but it is pretty ugly and not satisfactory in many ways...
I would like to get some advice / suggestions concerning the following points:

I need to work with the set of embeddings into
ℂ
and the set of infinite places and their cardinalities. Is it better to defined those asfintype
,finset
orset.finite
? So far, I have worked withfintype
. 
I think it would be useful for applications to be able to work with the set of embeddings into
ℂ
modulo the equivalence relation "define the same place" or a set of representatives of the embeddings modulo this relation. What is the best way to do that? Should I usesetoid
? Is there another / better way to do that? 
What would be the lemmas /methods I could use to prove that the number of places defined by complex embeddings is half the number of complex embeddings? I have been using docs#fintype.sum_fiberwise, but I find myself having to deal with quite a lot of technical difficulties so I am suspecting there is a better way to proceed.
Yaël Dillies (Nov 14 2022 at 10:21):
Ostrowski's theorem is one of the projects people worked on during this september's Xena workshop. Students are still on it.
Eric Rodriguez (Nov 14 2022 at 10:23):
There's Ostrowski for Q somewhere, but not the function/number field Version AFAIK
Riccardo Brasca (Nov 14 2022 at 10:49):
Concerning your first question, we have to think if it is better to have the embeddings as a new type or a (fin)set of type K →+* ℂ
. Do you think usually one has a ring hom and at some point they want to consider is as an embedding or rather one starts with an embedding in the first place?
Riccardo Brasca (Nov 14 2022 at 10:51):
The second question is similar, we have to figure out if it's more common to say that two embedding are equivalent or to speak about the equivalence class. In my opinion the actual equivalence class will be less useful, since one cannot apply it to elements, but I am not sure. In any case we surely want the setoid
.
Riccardo Brasca (Nov 14 2022 at 10:53):
Isn't proving that all the equivalence classes have cardinality 2
enough? Or maybe this is the difficult part?
Yaël Dillies (Nov 14 2022 at 11:07):
The Xena Ostrowski is the general one.
Xavier Roblot (Nov 14 2022 at 12:01):
Riccardo Brasca said:
Concerning your first question, we have to think if it is better to have the embeddings as a new type or a (fin)set of type
K →+* ℂ
. Do you think usually one has a ring hom and at some point they want to consider is as an embedding or rather one starts with an embedding in the first place?
Embeddings are fine since they are exactly (K→+* ℂ)
so they are naturally a type. For places, I am inclined to use type for the time being since I am more confortable with those.
The second question is similar, we have to figure out if it's more common to say that two embedding are equivalent or to speak about the equivalence class. In my opinion the actual equivalence class will be less useful, since one cannot apply it to elements, but I am not sure. In any case we surely want the
setoid
.
I agree that the equivalence class would be less useful. I'll define the setoid
Isn't proving that all the equivalence classes have cardinality
2
enough? Or maybe this is the difficult part?
It is not that it is difficult but more that it is painful. I'll see if I can do it in a better way.
Riccardo Brasca (Nov 14 2022 at 12:17):
Ah I see, you question is about places. Then I think having the finset
would be nice.
Riccardo Brasca (Nov 14 2022 at 12:27):
Sorry, I already changed my mind. The type of (the elements of) this finset
is less clear, so maybe let's just go with a fintype
.
Kevin Buzzard (Nov 14 2022 at 12:56):
What did Maria Ines do in her work on adeles?
María Inés de Frutos Fernández (Nov 14 2022 at 17:28):
Yaël Dillies said:
The Xena Ostrowski is the general one.
I think so far the students have been working on the rational case and the K(X) case, but they haven't yet thought about the general number/function field case.
María Inés de Frutos Fernández (Nov 14 2022 at 17:30):
Kevin Buzzard said:
What did Maria Ines do in her work on adeles?
I didn't write a definition of infinite place for my work on adèles (I got the infinite part of the adèle ring as ℝ ⊗[ℚ] K).
Yaël Dillies (Nov 14 2022 at 17:40):
Ah sorry! I thought so
Last updated: Aug 03 2023 at 10:10 UTC