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 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.extensionEmbedding_of_isReal : if the infinite place v is real, then this extends the embedding v.embedding_of_isReal : K →+* ℝ to v.completion →+* ℝ.
• NumberField.InfinitePlace.Completion.equiv_real_of_isReal : the ring isomorphism v.completion ≃+* ℝ when v is a real infinite place; the forward direction of this is extensionEmbedding_of_isReal.
• NumberField.InfinitePlace.Completion.equiv_complex_of_isComplex : 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 : NumberField.InfinitePlace K) : Type u_1

The completion of a number field at an infinite place.

Equations

• v.completion = (↑v).completion

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

Equations

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

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

Equations

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

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

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

Equations

• ⋯ = ⋯

def NumberField.InfinitePlace.Completion.extensionEmbedding {K : Type u_1} [Field K] (v : NumberField.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.extensionEmbedding_of_isReal {K : Type u_1} [Field K] {v : NumberField.InfinitePlace K} (hv : v.IsReal) : v.completion →+* ℝ

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

The embedding v.completion →+* ℝ at a real infinite palce is an isometry.

theorem NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding {K : Type u_1} [Field K] (v : NumberField.InfinitePlace K) : IsClosed (Set.range ⇑(NumberField.InfinitePlace.Completion.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 : NumberField.InfinitePlace K} (hv : v.IsReal) : IsClosed (Set.range ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal 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 : NumberField.InfinitePlace K} (hv : v.IsComplex) : (NumberField.InfinitePlace.Completion.extensionEmbedding v).fieldRange ≠ Complex.ofRealHom.fieldRange

theorem NumberField.InfinitePlace.Completion.surjective_extensionEmbedding_of_isComplex {K : Type u_1} [Field K] {v : NumberField.InfinitePlace K} (hv : v.IsComplex) : Function.Surjective ⇑(NumberField.InfinitePlace.Completion.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 : NumberField.InfinitePlace K} (hv : v.IsComplex) : Function.Bijective ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding v)

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

def NumberField.InfinitePlace.Completion.ringEquiv_complex_of_isComplex {K : Type u_1} [Field K] {v : NumberField.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.ringEquiv_complex_of_isComplex hv = RingEquiv.ofBijective (NumberField.InfinitePlace.Completion.extensionEmbedding v) ⋯

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

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

Equations

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

theorem NumberField.InfinitePlace.Completion.surjective_extensionEmbedding_of_isReal {K : Type u_1} [Field K] {v : NumberField.InfinitePlace K} (hv : v.IsReal) : Function.Surjective ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal 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 : NumberField.InfinitePlace K} (hv : v.IsReal) : Function.Bijective ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal hv)

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

def NumberField.InfinitePlace.Completion.ringEquiv_real_of_isReal {K : Type u_1} [Field K] {v : NumberField.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.ringEquiv_real_of_isReal hv = RingEquiv.ofBijective (NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal hv) ⋯

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

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

Equations

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