The completion of a number field at an infinite place

This file contains the completion of a number field at an infinite place. This is ultimately achieved by applying the UniformSpace.Completion functor, however each infinite place induces its own UniformSpace instance on the number field, so the inference system cannot automatically infer these. A common approach to handle the ambiguity that arises from having multiple sources of instances is through the use of type synonyms. In this case, we use the type synonym WithAbs of a semiring. In particular this type synonym depends on an absolute value, which provides a systematic way of assigning and inferring instances of the semiring that also depend on an absolute value. The completion of a field at multiple absolute values is defined in Mathlib/Algebra/Ring/WithAbs.lean as AbsoluteValue.Completion. The completion of a number field at an infinite place is then derived in this file, as InfinitePlace is a subtype of AbsoluteValue.

Main definitions

• NumberField.InfinitePlace.Completion : the completion of a number field K at an infinite place, obtained by completing K with respect to the absolute value associated to the infinite place.
• NumberField.InfinitePlace.Completion.extensionEmbedding : the embedding v.embedding : K →+* ℂ extended to v.Completion →+* ℂ.
• NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal : if the infinite place v is real, then this extends the embedding v.embedding_of_isReal : K →+* ℝ to v.Completion →+* ℝ.
• NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal : the ring isomorphism v.Completion ≃+* ℝ when v is a real infinite place; the forward direction of this is extensionEmbeddingOfIsReal.
• NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex : the ring isomorphism v.Completion ≃+* ℂ when v is a complex infinite place; the forward direction of this is extensionEmbedding.

Main results

• NumberField.Completion.locallyCompactSpace : the completion of a number field at an infinite place is locally compact.
• NumberField.Completion.isometry_extensionEmbedding : the embedding v.Completion →+* ℂ is an isometry. See also isometry_extensionEmbedding_of_isReal for the corresponding result on v.Completion →+* ℝ when v is real.
• NumberField.Completion.bijective_extensionEmbedding_of_isComplex : the embedding v.Completion →+* ℂ is bijective when v is complex. See also bijective_extensionEmebdding_of_isReal for the corresponding result for v.Completion →+* ℝ when v is real.

Tags

number field, embeddings, infinite places, completion, absolute value

@[reducible, inline]

abbrev NumberField.InfinitePlace.Completion {K : Type u_1} [Field K] (v : InfinitePlace K) : Type u_1

The completion of a number field at an infinite place.

Equations

• v.Completion = (↑v).Completion

@[deprecated NumberField.InfinitePlace.Completion (since := "2024-12-01")]

def NumberField.InfinitePlace.completion {K : Type u_1} [Field K] (v : InfinitePlace K) : Type u_1

Alias of NumberField.InfinitePlace.Completion.

---

The completion of a number field at an infinite place.

Equations

• @NumberField.InfinitePlace.completion = @NumberField.InfinitePlace.Completion

instance NumberField.InfinitePlace.Completion.instNormedField {K : Type u_1} [Field K] (v : InfinitePlace K) : NormedField v.Completion

Equations

• NumberField.InfinitePlace.Completion.instNormedField v = UniformSpace.Completion.instNormedFieldOfCompletableTopField (WithAbs ↑v)

theorem NumberField.InfinitePlace.Completion.norm_coe {K : Type u_1} [Field K] (v : InfinitePlace K) (x : WithAbs ↑v) : ‖↑x‖ = v ((WithAbs.equiv ↑v) x)

instance NumberField.InfinitePlace.Completion.instAlgebra {K : Type u_1} [Field K] (v : InfinitePlace K) : Algebra K v.Completion

Equations

• NumberField.InfinitePlace.Completion.instAlgebra v = inferInstanceAs (Algebra (WithAbs ↑v) (↑v).Completion)

theorem NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv (v : InfinitePlace ℚ) (x : WithAbs ↑v) : ↑((WithAbs.equiv ↑v) x) = ↑x

The coercion from the rationals to its completion along an infinite place is Rat.cast.

theorem NumberField.InfinitePlace.Completion.Rat.norm_infinitePlace_completion (v : InfinitePlace ℚ) (x : ℚ) : ‖↑x‖ = ↑|x|

instance NumberField.InfinitePlace.Completion.locallyCompactSpace {K : Type u_1} [Field K] (v : InfinitePlace K) : LocallyCompactSpace v.Completion

The completion of a number field at an infinite place is locally compact.

def NumberField.InfinitePlace.Completion.extensionEmbedding {K : Type u_1} [Field K] (v : InfinitePlace K) : v.Completion →+* ℂ

The embedding associated to an infinite place extended to an embedding v.Completion →+* ℂ.

Equations

• NumberField.InfinitePlace.Completion.extensionEmbedding v = AbsoluteValue.Completion.extensionEmbedding_of_comp ⋯

def NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) : v.Completion →+* ℝ

The embedding K →+* ℝ associated to a real infinite place extended to v.Completion →+* ℝ.

Equations

• NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv = AbsoluteValue.Completion.extensionEmbedding_of_comp ⋯

@[deprecated NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal (since := "2024-12-07")]

def NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) : v.Completion →+* ℝ

Alias of NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal.

---

The embedding K →+* ℝ associated to a real infinite place extended to v.Completion →+* ℝ.

Equations

• @NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal = @NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal

@[simp]

theorem NumberField.InfinitePlace.Completion.extensionEmbedding_coe {K : Type u_1} [Field K] (v : InfinitePlace K) (x : K) : (extensionEmbedding v) ↑x = v.embedding x

@[simp]

theorem NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal_coe {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) (x : K) : (extensionEmbeddingOfIsReal hv) ↑x = (embedding_of_isReal hv) x

theorem NumberField.InfinitePlace.Completion.isometry_extensionEmbedding {K : Type u_1} [Field K] (v : InfinitePlace K) : Isometry ⇑(extensionEmbedding v)

The embedding v.Completion →+* ℂ is an isometry.

theorem NumberField.InfinitePlace.Completion.isometry_extensionEmbedding_of_isReal {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) : Isometry ⇑(extensionEmbeddingOfIsReal hv)

The embedding v.Completion →+* ℝ at a real infinite place is an isometry.

theorem NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding {K : Type u_1} [Field K] (v : InfinitePlace K) : IsClosed (Set.range ⇑(extensionEmbedding v))

The embedding v.Completion →+* ℂ has closed image inside ℂ.

theorem NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding_of_isReal {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) : IsClosed (Set.range ⇑(extensionEmbeddingOfIsReal hv))

The embedding v.Completion →+* ℝ associated to a real infinite place has closed image inside ℝ.

theorem NumberField.InfinitePlace.Completion.subfield_ne_real_of_isComplex {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsComplex) : (extensionEmbedding v).fieldRange ≠ Complex.ofRealHom.fieldRange

theorem NumberField.InfinitePlace.Completion.surjective_extensionEmbedding_of_isComplex {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsComplex) : Function.Surjective ⇑(extensionEmbedding v)

If v is a complex infinite place, then the embedding v.Completion →+* ℂ is surjective.

theorem NumberField.InfinitePlace.Completion.bijective_extensionEmbedding_of_isComplex {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsComplex) : Function.Bijective ⇑(extensionEmbedding v)

If v is a complex infinite place, then the embedding v.Completion →+* ℂ is bijective.

def NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsComplex) : v.Completion ≃+* ℂ

The ring isomorphism v.Completion ≃+* ℂ, when v is complex, given by the bijection v.Completion →+* ℂ.

Equations

• NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex hv = RingEquiv.ofBijective (NumberField.InfinitePlace.Completion.extensionEmbedding v) ⋯

@[deprecated NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex (since := "2024-12-07")]

def NumberField.InfinitePlace.Completion.ringEquiv_complex_of_isComplex {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsComplex) : v.Completion ≃+* ℂ

Alias of NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex.

---

The ring isomorphism v.Completion ≃+* ℂ, when v is complex, given by the bijection v.Completion →+* ℂ.

Equations

• @NumberField.InfinitePlace.Completion.ringEquiv_complex_of_isComplex = @NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex

def NumberField.InfinitePlace.Completion.isometryEquivComplexOfIsComplex {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsComplex) : v.Completion ≃ᵢ ℂ

If the infinite place v is complex, then v.Completion is isometric to ℂ.

Equations

• NumberField.InfinitePlace.Completion.isometryEquivComplexOfIsComplex hv = { toEquiv := ↑(NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex hv), isometry_toFun := ⋯ }

@[deprecated NumberField.InfinitePlace.Completion.isometryEquivComplexOfIsComplex (since := "2024-12-07")]

def NumberField.InfinitePlace.Completion.isometryEquiv_complex_of_isComplex {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsComplex) : v.Completion ≃ᵢ ℂ

Alias of NumberField.InfinitePlace.Completion.isometryEquivComplexOfIsComplex.

---

If the infinite place v is complex, then v.Completion is isometric to ℂ.

Equations

• @NumberField.InfinitePlace.Completion.isometryEquiv_complex_of_isComplex = @NumberField.InfinitePlace.Completion.isometryEquivComplexOfIsComplex

theorem NumberField.InfinitePlace.Completion.surjective_extensionEmbedding_of_isReal {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) : Function.Surjective ⇑(extensionEmbeddingOfIsReal hv)

If v is a real infinite place, then the embedding v.Completion →+* ℝ is surjective.

theorem NumberField.InfinitePlace.Completion.bijective_extensionEmbedding_of_isReal {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) : Function.Bijective ⇑(extensionEmbeddingOfIsReal hv)

If v is a real infinite place, then the embedding v.Completion →+* ℝ is bijective.

def NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) : v.Completion ≃+* ℝ

The ring isomorphism v.Completion ≃+* ℝ, when v is real, given by the bijection v.Completion →+* ℝ.

Equations

• NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal hv = RingEquiv.ofBijective (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv) ⋯

@[deprecated NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal (since := "2024-12-07")]

def NumberField.InfinitePlace.Completion.ringEquiv_real_of_isReal {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) : v.Completion ≃+* ℝ

Alias of NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal.

---

The ring isomorphism v.Completion ≃+* ℝ, when v is real, given by the bijection v.Completion →+* ℝ.

Equations

• @NumberField.InfinitePlace.Completion.ringEquiv_real_of_isReal = @NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal

def NumberField.InfinitePlace.Completion.isometryEquivRealOfIsReal {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) : v.Completion ≃ᵢ ℝ

If the infinite place v is real, then v.Completion is isometric to ℝ.

Equations

• NumberField.InfinitePlace.Completion.isometryEquivRealOfIsReal hv = { toEquiv := ↑(NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal hv), isometry_toFun := ⋯ }

@[deprecated NumberField.InfinitePlace.Completion.isometryEquivRealOfIsReal (since := "2024-12-07")]

def NumberField.InfinitePlace.Completion.isometryEquiv_real_of_isReal {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) : v.Completion ≃ᵢ ℝ

Alias of NumberField.InfinitePlace.Completion.isometryEquivRealOfIsReal.

---

If the infinite place v is real, then v.Completion is isometric to ℝ.

Equations

• @NumberField.InfinitePlace.Completion.isometryEquiv_real_of_isReal = @NumberField.InfinitePlace.Completion.isometryEquivRealOfIsReal