[Merged by Bors] - refactor(NumberTheory.NumberField.CanonicalEmbedding): make the canonical embedding canonical#5518
[Merged by Bors] - refactor(NumberTheory.NumberField.CanonicalEmbedding): make the canonical embedding canonical#5518
Conversation
|
Please remember to add the label |
|
This PR/issue depends on: |
|
sorry, can you briefly explain what is the issue with the original one and how this fixes this? |
Thanks for the suggestion. I have expanded the PR description with more details on the refactor. |
There was a problem hiding this comment.
I haven't reviewed most of the later proofs, but I do think that this is the way to do it. The "canonical" R-vector space is the Galois-invariant subset of the C-vector-space. I have expressed my distaste for is-R-or-C before -- PRs like this are somehow doing things in a slightly more invariant way -- you get more theorems about complex conjugation for free if you consider it as an action of Z/2 on the RBarification rather than choosing an orientation (i.e. choosing I as a basis vector) and then having to start fussing about "CM types" or whatever they're called in the CM theory of abelian varieties.
…ical embedding canonical (#5518) It was observed by @kbuzzard, and rightly so, that in the first version of this file the `canonical_embedding` was not so canonical. This refactor fixes that by replacing it with a truly canonical embedding. More precisely, in the old version, the canonical embedding was defined as the ring homomorphism `K →+* ℝ^r₁ × ℂ^r₂` that sends `x ∈ K` to `(φ_₁(x),...,φ_r₁(x)) × (ψ_₁(x),..., ψ_r₂(x))` where `φ_₁,...,φ_r₁` are its real embeddings and `ψ_₁,..., ψ_r₂` are its complex embeddings (up to complex conjugation). This is not canonical since it depends upon the choice of the `ψ`'s. In the new version, the canonical embedding is defined as the ring homomorphism `K →+* ℂ^n` that sends `x ∈ K` to `(φ_₁(x),...,φ_n(x))` where the `φ_i`'s are the complex embeddings of `K`. The new version is easier to compute with since one does not have to distinguish between real and complex embeddings as in the first version. It also enables to prove the following result: the image of the ring of integers by `canonicalEmbedding` is a full ℤ-lattice (see `latticeBasis`) that will be useful in #5650. Note that the original version of the canonical embedding will reappear in #5650 (as `mixedEmbedding`) since it allows for easier volume computation.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
It was observed by @kbuzzard, and rightly so, that in the first version of this file the
canonical_embeddingwas not so canonical. This refactor fixes that by replacing it with a truly canonical embedding.More precisely, in the old version, the canonical embedding was defined as the ring homomorphism
K →+* ℝ^r₁ × ℂ^r₂that sendsx ∈ Kto(φ_₁(x),...,φ_r₁(x)) × (ψ_₁(x),..., ψ_r₂(x))whereφ_₁,...,φ_r₁are its real embeddings andψ_₁,..., ψ_r₂are its complex embeddings (up tocomplex conjugation). This is not canonical since it depends upon the choice of the
ψ's.In the new version, the canonical embedding is defined as the ring homomorphism
K →+* ℂ^nthat sendsx ∈ Kto(φ_₁(x),...,φ_n(x))where theφ_i's are the complex embeddings ofK.The new version is easier to compute with since one does not have to distinguish between real and complex embeddings as in the first version. It also enables to prove the following result: the image of the ring of integers by
canonicalEmbeddingis a full ℤ-lattice (seelatticeBasis) that will be useful in #5650.Note that the original version of the canonical embedding will reappear in #5650 (as
mixedEmbedding) since it allows for easier volume computation.