Documentation

Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

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/Analysis/Normed/Field/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_extensionEmbeddingOfIsReal 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_extensionEmbeddingOfIsReal for the corresponding result for v.Completion →+* ℝ when v is real.

Tags #

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

theorem NumberField.InfinitePlace.isometry_embedding {K : Type u_1} [Field K] (v : InfinitePlace K) :

Isometry ⇑(v.embedding.comp (WithAbs.equiv ↑v).toRingHom)

theorem NumberField.InfinitePlace.isometry_embedding_of_isReal {K : Type u_1} [Field K] (v : InfinitePlace K) (hv : v.IsReal) :

Isometry ⇑((embedding_of_isReal hv).comp (WithAbs.equiv ↑v).toRingHom)

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

CompletableTopField (WithAbs ↑v)

structure 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, as a one-field structure wrapping the completion v.1.Completion of K at the underlying absolute value.

ofCompletion :: (

toCompletion : (↑v).Completion
The underlying element of v.1.Completion.

)

Instances For

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

v.Completion ≃ (↑v).Completion

Completion.toCompletion and Completion.ofCompletion as an equivalence.

Equations

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

Instances For

@[simp]

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

(equivCompletion v) self = self.toCompletion

@[simp]

theorem NumberField.InfinitePlace.Completion.equivCompletion_symm_apply_toCompletion {K : Type u_1} [Field K] (v : InfinitePlace K) (toCompletion : (↑v).Completion) :

((equivCompletion v).symm toCompletion).toCompletion = toCompletion

@[instance_reducible]

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

NormedField v.Completion

Equations

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

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

v.Completion ≃+* (↑v).Completion

Completion.toCompletion as a ring isomorphism onto the underlying completion.

Equations

NumberField.InfinitePlace.Completion.equiv v = { toEquiv := NumberField.InfinitePlace.Completion.equivCompletion v, map_mul' := ⋯, map_add' := ⋯ }

Instances For

@[simp]

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

(equiv v) self = self.toCompletion

@[simp]

theorem NumberField.InfinitePlace.Completion.toCompletion_ofCompletion {K : Type u_1} [Field K] (v : InfinitePlace K) (x : (↑v).Completion) :

{ toCompletion := x }.toCompletion = x

@[simp]

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

{ toCompletion := x.toCompletion } = x

@[simp]

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

toCompletion 0 = 0

@[simp]

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

toCompletion 1 = 1

@[simp]

theorem NumberField.InfinitePlace.Completion.toCompletion_add {K : Type u_1} [Field K] (v : InfinitePlace K) (x y : v.Completion) :

(x + y).toCompletion = x.toCompletion + y.toCompletion

@[simp]

theorem NumberField.InfinitePlace.Completion.toCompletion_mul {K : Type u_1} [Field K] (v : InfinitePlace K) (x y : v.Completion) :

(x * y).toCompletion = x.toCompletion * y.toCompletion

theorem NumberField.InfinitePlace.Completion.ext {K : Type u_1} [Field K] {v : InfinitePlace K} {x y : v.Completion} (h : x.toCompletion = y.toCompletion) :

x = y

theorem NumberField.InfinitePlace.Completion.ext_iff {K : Type u_1} [Field K] {v : InfinitePlace K} {x y : v.Completion} :

x = y ↔ x.toCompletion = y.toCompletion

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

Function.Surjective toCompletion

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

Function.Surjective ofCompletion

@[simp]

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

‖x.toCompletion‖ = ‖x‖

@[simp]

theorem NumberField.InfinitePlace.Completion.norm_ofCompletion {K : Type u_1} [Field K] (v : InfinitePlace K) (x : (↑v).Completion) :

‖{ toCompletion := x }‖ = ‖x‖

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

Isometry toCompletion

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

v.Completion ≃ᵢ (↑v).Completion

Completion.toCompletion as an isometry equivalence onto the underlying completion.

Equations

NumberField.InfinitePlace.Completion.isometryEquivCompletion v = { toEquiv := NumberField.InfinitePlace.Completion.equivCompletion v, isometry_toFun := ⋯ }

Instances For

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

Continuous toCompletion

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

Continuous ofCompletion

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

CompleteSpace v.Completion

@[instance_reducible]

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

Inhabited v.Completion

Equations

NumberField.InfinitePlace.Completion.instInhabited v = { default := 0 }

@[instance_reducible]

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

Coe (WithAbs ↑v) v.Completion

Coercion of an element of WithAbs v.1 into the completion.

Equations

NumberField.InfinitePlace.Completion.instCoeWithAbsRealValAbsoluteValueExistsRingHomComplexEqPlace v = { coe := fun (x : WithAbs ↑v) => { toCompletion := ↑x } }

@[instance_reducible]

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

Coe K v.Completion

Coercion of an element of K into the completion.

Equations

NumberField.InfinitePlace.Completion.instCoe v = { coe := fun (k : K) => { toCompletion := ↑(WithAbs.toAbs (↑v) k) } }

@[simp]

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

{ toCompletion := ↑x }.toCompletion = ↑x

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

{ toCompletion := ↑(WithAbs.toAbs (↑v) 0) } = 0

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

{ toCompletion := ↑(WithAbs.toAbs (↑v) 1) } = 1

theorem NumberField.InfinitePlace.Completion.coe_add {K : Type u_1} [Field K] (v : InfinitePlace K) (x y : K) :

{ toCompletion := ↑(WithAbs.toAbs (↑v) (x + y)) } = { toCompletion := ↑(WithAbs.toAbs (↑v) x) } + { toCompletion := ↑(WithAbs.toAbs (↑v) y) }

theorem NumberField.InfinitePlace.Completion.coe_mul {K : Type u_1} [Field K] (v : InfinitePlace K) (x y : K) :

{ toCompletion := ↑(WithAbs.toAbs (↑v) (x * y)) } = { toCompletion := ↑(WithAbs.toAbs (↑v) x) } * { toCompletion := ↑(WithAbs.toAbs (↑v) y) }

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

Continuous fun (x : WithAbs ↑v) => { toCompletion := ↑x }

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

DenseRange fun (x : WithAbs ↑v) => { toCompletion := ↑x }

theorem NumberField.InfinitePlace.Completion.induction_on {K : Type u_1} [Field K] (v : InfinitePlace K) {p : v.Completion → Prop} (x : v.Completion) (hp : IsClosed {x : v.Completion | p x}) (ih : ∀ (a : WithAbs ↑v), p { toCompletion := ↑a }) :

p x

Induction on the completion of a number field at an infinite place: a closed property that holds on the image of K holds everywhere.

@[instance_reducible]

noncomputable instance NumberField.InfinitePlace.Completion.instAlgebra {K : Type u_1} [Field K] (v : InfinitePlace K) (R : Type u_2) [CommSemiring R] [Algebra R (WithAbs ↑v)] [UniformContinuousConstSMul R (WithAbs ↑v)] :

Algebra R v.Completion

Equations

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

theorem NumberField.InfinitePlace.Completion.algebraMap_toCompletion {K : Type u_1} [Field K] (v : InfinitePlace K) (R : Type u_2) [CommSemiring R] [Algebra R (WithAbs ↑v)] [UniformContinuousConstSMul R (WithAbs ↑v)] (r : R) :

((algebraMap R v.Completion) r).toCompletion = (algebraMap R (↑v).Completion) r

@[simp]

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

(algebraMap K v.Completion) k = { toCompletion := ↑(WithAbs.toAbs (↑v) k) }

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

‖{ toCompletion := ↑x }‖ = v ((WithAbs.equiv ↑v) x)

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

↑((WithAbs.equiv ↑v) x) = { toCompletion := ↑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.

noncomputable 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 = ⋯.extensionHom.comp (NumberField.InfinitePlace.Completion.equiv v).toRingHom

Instances For

noncomputable 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 = ⋯.extensionHom.comp (NumberField.InfinitePlace.Completion.equiv v).toRingHom

Instances For

@[simp]

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

(extensionEmbedding v) { toCompletion := ↑x } = v.embedding ((WithAbs.equiv ↑v) x)

@[simp]

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

(extensionEmbeddingOfIsReal hv) { toCompletion := ↑x } = (embedding_of_isReal hv) ((WithAbs.equiv ↑v) 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_extensionEmbeddingOfIsReal {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.

@[simp]

theorem NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_apply {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) (x : v.Completion) :

↑((extensionEmbeddingOfIsReal hv) x) = (extensionEmbedding v) x

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_extensionEmbeddingOfIsReal {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.

noncomputable 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) ⋯

Instances For

@[simp]

theorem NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex_apply {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsComplex) (x : v.Completion) :

(ringEquivComplexOfIsComplex hv) x = (extensionEmbedding v) x

noncomputable 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 := ⋯ }

Instances For

theorem NumberField.InfinitePlace.Completion.surjective_extensionEmbeddingOfIsReal {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_extensionEmbeddingOfIsReal {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.

noncomputable 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) ⋯

Instances For

@[simp]

theorem NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal_apply {K : Type u_1} [Field K] {v : InfinitePlace K} (hv : v.IsReal) (x : v.Completion) :

(ringEquivRealOfIsReal hv) x = (extensionEmbeddingOfIsReal hv) x

noncomputable 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 := ⋯ }

Instances For

theorem NumberField.InfinitePlace.Completion.algebraMap_eq_coe {K : Type u_1} [Field K] {v : InfinitePlace K} {L : Type u_2} [Field L] [Algebra K L] (w : InfinitePlace L) (x : WithAbs ↑v) :

(algebraMap (WithAbs ↑v) w.Completion) x = { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) x) }

@[simp]

theorem NumberField.InfinitePlace.Completion.algebraMap_coe {K : Type u_1} [Field K] {v : InfinitePlace K} {L : Type u_2} [Field L] [Algebra K L] (w : InfinitePlace L) [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] (x : WithAbs ↑v) :

(algebraMap v.Completion w.Completion) { toCompletion := ↑x } = { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) x) }

theorem NumberField.InfinitePlace.Completion.liesOver_extensionEmbedding {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (w : InfinitePlace L) (v : InfinitePlace K) [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] [ComplexEmbedding.LiesOver w.embedding v.embedding] :

ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)

Assume that w.Completion forms an algebra over v.Completion with continuous scalar action, such that IsScalarTower K v.Completion w.Completion. If w.embedding : L →+* ℂ extends v.embedding : K →+* ℂ, then the corresponding embeddings to completions are also extensions.

theorem NumberField.InfinitePlace.Completion.liesOver_conjugate_extensionEmbedding {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (w : InfinitePlace L) (v : InfinitePlace K) [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] [ComplexEmbedding.LiesOver (ComplexEmbedding.conjugate w.embedding) v.embedding] :

ComplexEmbedding.LiesOver (ComplexEmbedding.conjugate (extensionEmbedding w)) (extensionEmbedding v)

@[simp]

theorem NumberField.InfinitePlace.Completion.liesOver_extensionEmbedding_apply {K : Type u_1} [Field K] {L : Type u_2} [Field L] (w : InfinitePlace L) (v : InfinitePlace K) [Algebra v.Completion w.Completion] {φ : w.Completion →+* ℂ} [ComplexEmbedding.LiesOver φ (extensionEmbedding v)] {x : v.Completion} :

φ ((algebraMap v.Completion w.Completion) x) = (extensionEmbedding v) x

theorem NumberField.InfinitePlace.LiesOver.isometry_algebraMap {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (w : InfinitePlace L) (v : InfinitePlace K) [w.LiesOver v] :

Isometry ⇑(algebraMap (WithAbs ↑v) (WithAbs ↑w))

theorem NumberField.InfinitePlace.LiesOver.embedding_liesOver_of_isReal {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (w : InfinitePlace L) {v : InfinitePlace K} [w.LiesOver v] (h : v.IsReal) :

ComplexEmbedding.LiesOver w.embedding v.embedding

theorem NumberField.InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (w : InfinitePlace L) {v : InfinitePlace K} [w.LiesOver v] [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] (h : v.IsReal) :

ComplexEmbedding.LiesOver (Completion.extensionEmbedding w) (Completion.extensionEmbedding v)