Canonical embedding of a number field #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The canonical embedding of a number field K of signature (r₁, r₂) is 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).
Main definitions and results #
number_field.canonical_embedding.ring_of_integers.inter_ball_finite: the intersection of the image of the ring of integers by the canonical embedding and any ball centered at0of finite radius is finite.
Tags #
number field, infinite places
theorem
number_field.canonical_embedding.non_trivial_space
(K : Type u_1)
[field K]
[number_field K] :
nontrivial (({w // w.is_real} → ℝ) × ({w // w.is_complex} → ℂ))
The canonical embedding of a number field K of signature (r₁, r₂) into ℝ^r₁ × ℂ^r₂.
Equations
- number_field.canonical_embedding K = (pi.ring_hom (λ (w : {w // w.is_real}), number_field.infinite_place.is_real.embedding _)).prod (pi.ring_hom (λ (w : {w // w.is_complex}), w.val.embedding))
@[simp]
theorem
number_field.canonical_embedding.apply_at_real_infinite_place
{K : Type u_1}
[field K]
(w : {w // w.is_real})
(x : K) :
@[simp]
theorem
number_field.canonical_embedding.apply_at_complex_infinite_place
{K : Type u_1}
[field K]
(w : {w // w.is_complex})
(x : K) :
theorem
number_field.canonical_embedding.nnnorm_eq
{K : Type u_1}
[field K]
[number_field K]
(x : K) :
‖⇑(number_field.canonical_embedding K) x‖₊ = finset.univ.sup (λ (w : number_field.infinite_place K), ⟨⇑w x, _⟩)
theorem
number_field.canonical_embedding.norm_le_iff
{K : Type u_1}
[field K]
[number_field K]
(x : K)
(r : ℝ) :
‖⇑(number_field.canonical_embedding K) x‖ ≤ r ↔ ∀ (w : number_field.infinite_place K), ⇑w x ≤ r
The image of 𝓞 K as a subring of ℝ^r₁ × ℂ^r₂.
Equations
Instances for ↥number_field.canonical_embedding.integer_lattice
noncomputable
def
number_field.canonical_embedding.equiv_integer_lattice
(K : Type u_1)
[field K]
[number_field K] :
The linear equiv between 𝓞 K and the integer lattice.
Equations
- number_field.canonical_embedding.equiv_integer_lattice K = linear_equiv.of_bijective {to_fun := λ (x : ↥(number_field.ring_of_integers K)), ⟨⇑(number_field.canonical_embedding K) (⇑(algebra_map ↥(number_field.ring_of_integers K) K) x), _⟩, map_add' := _, map_smul' := _} _
theorem
number_field.canonical_embedding.integer_lattice.inter_ball_finite
(K : Type u_1)
[field K]
[number_field K]
(r : ℝ) :
@[protected, instance]