The completion of a number field at an infinite place

This file contains the completion of a number field at its infinite places.

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 define a type synonym WithAbs for a semiring. In particular this type synonym depends on an absolute value. This provides a systematic way of assigning and inferring instances of the semiring that also depend on an absolute value. In our application, relevant instances and the completion of a number field K are first defined at the level of AbsoluteValue by using the type synonym WithAbs of K, and then derived downstream for InfinitePlace (which is a subtype of AbsoluteValue). Namely, if v is an infinite place of K, then v.completion defines the completion of K at v.

The embedding v.embedding : K →+* ℂ associated to an v enjoys useful properties within the uniform structure defined by v; namely, it is a uniform embedding and an isometry. This is because the absolute value associated to v factors through v.embedding. This allows us to show that the completion of K at an infinite place is locally compact. Moreover, we can extend v.embedding to a embedding v.completion →+* ℂ. We show that if v is real (i.e., v.embedding (K) ⊆ ℝ) then the extended embedding gives an isomorphism v.completion ≃+* ℝ, else the extended embedding gives an isomorphism v.completion ≃+* ℂ.

Main definitions

• WithAbs : type synonym for a semiring which depends on an absolute value. This is a function that takes an absolute value on a semiring and returns the semiring. We use this to assign and infer instances on a semiring that depend on absolute values.
• AbsoluteValue.completion : the uniform space completion of a field K equipped with real absolute value.
• 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.ringEquiv_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.ringEquiv_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

def WithAbs {R : Type u_1} {S : Type u_2} [Semiring R] [OrderedSemiring S] : AbsoluteValue R S → Type u_1

Type synonym for a semiring which depends on an absolute value. This is a function that takes an absolute value on a semiring and returns the semiring. We use this to assign and infer instances on a semiring that depend on absolute values.

Equations

• WithAbs x = R

instance WithAbs.instNormedRingReal {R : Type u_1} [Ring R] (v : AbsoluteValue R ℝ) : NormedRing (WithAbs v)

Equations

• WithAbs.instNormedRingReal v = NormedRing.mk ⋯ ⋯

instance WithAbs.normedField {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : NormedField (WithAbs v)

Equations

• WithAbs.normedField v = let __spread.0 := inferInstanceAs (NormedRing (WithAbs v)); NormedField.mk ⋯ ⋯

instance WithAbs.instInhabitedReal {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : Inhabited (WithAbs v)

Equations

• WithAbs.instInhabitedReal v = { default := 0 }

theorem WithAbs.isometry_of_comp {K : Type u_2} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_1} [NormedField L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : Isometry ⇑f

If the absolute value v factors through an embedding f into a normed field, then f is an isometry.

theorem WithAbs.pseudoMetricSpace_induced_of_comp {K : Type u_2} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_1} [NormedField L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : PseudoMetricSpace.induced (⇑f) inferInstance = MetricSpace.toPseudoMetricSpace

If the absolute value v factors through an embedding f into a normed field, then the pseudo metric space associated to the absolute value is the same as the pseudo metric space induced by f.

theorem WithAbs.uniformSpace_comap_eq_of_comp {K : Type u_2} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_1} [NormedField L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : UniformSpace.comap (⇑f) inferInstance = PseudoMetricSpace.toUniformSpace

If the absolute value v factors through an embedding f into a normed field, then the uniform structure associated to the absolute value is the same as the uniform structure induced by f.

theorem WithAbs.uniformInducing_of_comp {K : Type u_2} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_1} [NormedField L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : UniformInducing ⇑f

If the absolute value v factors through an embedding f into a normed field, then f is uniform inducing.

@[reducible, inline]

abbrev AbsoluteValue.completion {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : Type u_1

The completion of a field with respect to a real absolute value.

Equations

• v.completion = UniformSpace.Completion (WithAbs v)

instance AbsoluteValue.Completion.instCoeCompletion {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : Coe K v.completion

Equations

• AbsoluteValue.Completion.instCoeCompletion v = inferInstanceAs (Coe (WithAbs v) (UniformSpace.Completion (WithAbs v)))

@[reducible, inline]

abbrev AbsoluteValue.Completion.extensionEmbedding_of_comp {K : Type u_1} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_2} [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : v.completion →+* L

If the absolute value of a normed field factors through an embedding into another normed field L, then we can extend that embedding to an embedding on the completion v.completion →+* L.

Equations

• AbsoluteValue.Completion.extensionEmbedding_of_comp h = UniformSpace.Completion.extensionHom f ⋯

theorem AbsoluteValue.Completion.extensionEmbedding_of_comp_coe {K : Type u_1} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_2} [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) (x : K) : (AbsoluteValue.Completion.extensionEmbedding_of_comp h) (↑(WithAbs v) x) = f x

theorem AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp {K : Type u_1} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_2} [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) (x : v.completion) (y : v.completion) : dist ((AbsoluteValue.Completion.extensionEmbedding_of_comp h) x) ((AbsoluteValue.Completion.extensionEmbedding_of_comp h) y) = dist x y

If the absolute value of a normed field factors through an embedding into another normed field, then the extended embedding v.completion →+* L preserves distances.

theorem AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp {K : Type u_1} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_2} [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : Isometry ⇑(AbsoluteValue.Completion.extensionEmbedding_of_comp h)

If the absolute value of a normed field factors through an embedding into another normed field, then the extended embedding v.completion →+* L is an isometry.

theorem AbsoluteValue.Completion.closedEmbedding_extensionEmbedding_of_comp {K : Type u_1} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_2} [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : ClosedEmbedding ⇑(AbsoluteValue.Completion.extensionEmbedding_of_comp h)

If the absolute value of a normed field factors through an embedding into another normed field, then the extended embedding v.completion →+* L is a closed embedding.

theorem AbsoluteValue.Completion.locallyCompactSpace {K : Type u_1} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_2} [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L} [LocallyCompactSpace L] (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : LocallyCompactSpace v.completion

If the absolute value of a normed field factors through an embedding into another normed field that is locally compact, then the completion of the first normed field is also locally compact.

@[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.ofReal.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 := ⋯ }