Commit 2023-08-19 09:44 0c89b795

refactor(NumberTheory.NumberField.CanonicalEmbedding): make the canonical 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.