The ring-of-integers lattice in the Euclidean mixed embedding. The real and imaginary coordinates are unweighted; the covolume is 2^(-r₂) √|D|. All norm comparisons below have constants depending only on the degree.

noncomputable def CCDN.euclideanNumberFieldEmbedding (K : Type u_1) [Field K] [NumberField K] : K →+* NumberField.mixedEmbedding.euclidean.mixedSpace K

The mixed embedding with its Euclidean, rather than supremum, norm.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CCDN.toMixed_euclideanNumberFieldEmbedding (K : Type u_1) [Field K] [NumberField K] (x : K) : (NumberField.mixedEmbedding.euclidean.toMixed K) ((euclideanNumberFieldEmbedding K) x) = (NumberField.mixedEmbedding K) x

Transporting the Euclidean embedding of x back to the mixed space gives the mixed embedding of x.

theorem CCDN.euclideanNumberFieldEmbedding_injective (K : Type u_1) [Field K] [NumberField K] : Function.Injective ⇑(euclideanNumberFieldEmbedding K)

The Euclidean mixed embedding of a number field is injective.

noncomputable def CCDN.euclideanNumberFieldLinearMap (K : Type u_1) [Field K] [NumberField K] : K →ₗ[ℚ] NumberField.mixedEmbedding.euclidean.mixedSpace K

The Euclidean mixed embedding of K, as a ℚ-linear map.

Equations

• CCDN.euclideanNumberFieldLinearMap K = ↑ℚ ↑↑(NumberField.mixedEmbedding.euclidean.toMixed K).symm ∘ₗ (NumberField.mixedEmbedding K).toRatAlgHom.toLinearMap

@[simp]

theorem CCDN.euclideanNumberFieldLinearMap_apply (K : Type u_1) [Field K] [NumberField K] (x : K) : (euclideanNumberFieldLinearMap K) x = (euclideanNumberFieldEmbedding K) x

The ℚ-linear Euclidean embedding agrees with euclideanNumberFieldEmbedding.

theorem CCDN.euclideanNumberFieldEmbedding_mem_integerLattice (K : Type u_1) [Field K] [NumberField K] (x : NumberField.RingOfIntegers K) : (euclideanNumberFieldEmbedding K) ↑x ∈ NumberField.mixedEmbedding.euclidean.integerLattice K

The Euclidean embedding of an algebraic integer lies in the Euclidean integer lattice.

theorem CCDN.mem_euclidean_integerLattice_iff (K : Type u_1) [Field K] [NumberField K] (x : NumberField.mixedEmbedding.euclidean.mixedSpace K) : x ∈ NumberField.mixedEmbedding.euclidean.integerLattice K ↔ ∃ (z : NumberField.RingOfIntegers K), (euclideanNumberFieldEmbedding K) ↑z = x

A vector lies in the Euclidean integer lattice if and only if it is the Euclidean embedding of an algebraic integer.

theorem CCDN.one_le_euclidean_norm_integer (K : Type u_1) [Field K] [NumberField K] {x : NumberField.RingOfIntegers K} (hx : x ≠ 0) : 1 ≤ ‖(euclideanNumberFieldEmbedding K) ↑x‖

The Euclidean embedding of a nonzero algebraic integer has norm at least 1.

theorem CCDN.one_le_euclidean_integerLattice_norm (K : Type u_1) [Field K] [NumberField K] {x : NumberField.mixedEmbedding.euclidean.mixedSpace K} (hx : x ∈ NumberField.mixedEmbedding.euclidean.integerLattice K) (hne : x ≠ 0) : 1 ≤ ‖x‖

Every nonzero vector of the Euclidean integer lattice has norm at least 1.

theorem CCDN.euclideanNumberFieldEmbedding_norm_le (K : Type u_1) [Field K] [NumberField K] {B : ℝ} (hB : 0 ≤ B) (x : K) (hx : ∀ (w : NumberField.InfinitePlace K), w x ≤ B) : ‖(euclideanNumberFieldEmbedding K) x‖ ≤ √↑(Module.finrank ℚ K) * B

If w x ≤ B at every infinite place w, then the Euclidean embedding of x has norm at most √[K : ℚ] * B.

theorem CCDN.euclideanNumberFieldEmbedding_one_norm_le (K : Type u_1) [Field K] [NumberField K] : ‖(euclideanNumberFieldEmbedding K) 1‖ ≤ √↑(Module.finrank ℚ K)

The Euclidean embedding of 1 has norm at most √[K : ℚ].

theorem CCDN.euclideanNumberFieldEmbedding_norm_mul_le (K : Type u_1) [Field K] [NumberField K] (x y : K) : ‖(euclideanNumberFieldEmbedding K) (x * y)‖ ≤ ‖(euclideanNumberFieldEmbedding K) x‖ * ‖(euclideanNumberFieldEmbedding K) y‖

The Euclidean norm is submultiplicative on embedded field elements: the norm of the embedding of x * y is at most the product of the norms of the embeddings of x and y.

theorem CCDN.euclidean_integerLattice_covolume (K : Type u_1) [Field K] [NumberField K] : ZLattice.covolume (NumberField.mixedEmbedding.euclidean.integerLattice K) MeasureTheory.volume = 2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * √|↑(NumberField.discr K)|

The Euclidean integer lattice has covolume 2 ^ (-r₂) * √|discr K|, where r₂ is the number of complex places of K.