WithAbs for fields

This extends the WithAbs mechanism to fields, providing a type synonym for a field which depends on an absolute value. This is useful when dealing with several absolute values on the same field.

In particular this allows us to define the completion of a field at a given absolute value.

instance WithAbs.instField {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] (v : AbsoluteValue R S) : Field (WithAbs v)

Equations

• WithAbs.instField v = inst✝

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

Equations

• WithAbs.normedField v = v.toNormedField

instance WithAbs.instFiniteDimensional {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] {R' : Type u_3} [Field R] [Field R'] [Module R R'] [FiniteDimensional R R'] (v : AbsoluteValue R S) : FiniteDimensional (WithAbs v) R'

instance WithAbs.instIsSeparable {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] {R' : Type u_3} [Field R] [Field R'] [Algebra R R'] [Algebra.IsSeparable R R'] (v : AbsoluteValue R S) : Algebra.IsSeparable (WithAbs v) R'

The completion of a field at an absolute value.

theorem WithAbs.isometry_of_comp {K : Type u_3} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_4} [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_3} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_4} [NormedField L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : PseudoMetricSpace.induced (⇑f) inferInstance = (normedField v).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_3} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_4} [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.isUniformInducing_of_comp {K : Type u_3} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_4} [NormedField L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : IsUniformInducing ⇑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_3} [Field K] (v : AbsoluteValue K ℝ) : Type u_3

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

Equations

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

instance AbsoluteValue.Completion.instCoe {K : Type u_3} [Field K] (v : AbsoluteValue K ℝ) : Coe K v.Completion

Equations

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

@[reducible, inline]

abbrev AbsoluteValue.Completion.extensionEmbedding_of_comp {K : Type u_3} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_4} [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_3} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_4} [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) (x : K) : (extensionEmbedding_of_comp h) ↑x = f x

theorem AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp {K : Type u_3} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_4} [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) (x y : v.Completion) : dist ((extensionEmbedding_of_comp h) x) ((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_3} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_4} [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : Isometry ⇑(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.isClosedEmbedding_extensionEmbedding_of_comp {K : Type u_3} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_4} [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L} (h : ∀ (x : WithAbs v), ‖f x‖ = v x) : Topology.IsClosedEmbedding ⇑(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_3} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_4} [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.