Embeddings of a number field

Stream: general

[Xavier Roblot]

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]

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]

/poll Embeddings of a number field
Ring hom. K →+* A
Alg. hom. K →ₐ[ℚ] A

[Riccardo Brasca]

I agree with Kevin. The algebra_rat diamond is really annoying.

[Reid Barton]

I would also guess that many of the basic things you can prove about these will work in any characteristic.

[Reid Barton]

Oh but then you would also want to work over the base field, which might not be a prime field.

[Anne Baanen]

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]

No I didn't look at this one got too distracted by eta for structures type diamonds.

[Junyan Xu]

Anyone assessed difficulty of backporting structure eta defeq?

[Xavier Roblot]

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 as fintype, finset or set.finite? So far, I have worked with fintype.

• 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 use setoid? 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]

Ostrowski's theorem is one of the projects people worked on during this september's Xena workshop. Students are still on it.

[Eric Rodriguez]

There's Ostrowski for Q somewhere, but not the function/number field Version AFAIK

[Riccardo Brasca]

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]

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]

Isn't proving that all the equivalence classes have cardinality 2 enough? Or maybe this is the difficult part?

[Yaël Dillies]

The Xena Ostrowski is the general one.

[Xavier Roblot]

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]

Ah I see, you question is about places. Then I think having the finset would be nice.

[Riccardo Brasca]

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]

What did Maria Ines do in her work on adeles?

[María Inés de Frutos Fernández]

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]

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]

Ah sorry! I thought so