Documentation

Mathlib.Analysis.Normed.Field.WithAbs

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.

source
@[implicit_reducible]
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
source
@[implicit_reducible]
noncomputable instance WithAbs.normedField {R : Type u_1} [Field R] (v : AbsoluteValue R ℝ) :
NormedField (WithAbs v)
Equations
source
instance WithAbs.instFiniteDimensional {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] {T : Type u_3} [Field T] (v : AbsoluteValue R S) [Module R T] [FiniteDimensional R T] :
FiniteDimensional (WithAbs v) T
source
instance WithAbs.instFiniteDimensional_1 {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] {T : Type u_3} [Field T] (v : AbsoluteValue R S) [Module T R] [FiniteDimensional T R] :
FiniteDimensional T (WithAbs v)
source
instance WithAbs.instIsSeparable {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] {T : Type u_3} [Field T] (v : AbsoluteValue R S) [Algebra R T] [Algebra.IsSeparable R T] :
Algebra.IsSeparable (WithAbs v) T
source
instance WithAbs.instIsSeparable_1 {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] {T : Type u_3} [Field T] (v : AbsoluteValue R S) [Algebra T R] [Algebra.IsSeparable T R] :
Algebra.IsSeparable T (WithAbs v)
source
@[simp]
theorem WithAbs.toAbs_div {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] (v : AbsoluteValue R S) (x y : R) :
toAbs v (x / y) = toAbs v x / toAbs v y
source
@[simp]
theorem WithAbs.ofAbs_div {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] (v : AbsoluteValue R S) (x y : WithAbs v) :
(x / y).ofAbs = x.ofAbs / y.ofAbs
source
@[simp]
theorem WithAbs.toAbs_inv {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] (v : AbsoluteValue R S) (x : R) :
toAbs v x⁻¹ = (toAbs v x)⁻¹
source
@[simp]
theorem WithAbs.ofAbs_inv {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] (v : AbsoluteValue R S) (x : WithAbs v) :
x⁻¹.ofAbs = x.ofAbs⁻¹
source
theorem WithAbs.tendsto_one_div_one_add_pow_nhds_one {R : Type u_1} [Field R] {v : AbsoluteValue R ℝ} {a : R} (ha : v a < 1) :
Filter.Tendsto (fun (n : ℕ) => (equiv v).symm (1 / (1 + a ^ n))) Filter.atTop (nhds 1)
source
instance WithAbs.instUniformContinuousConstSMulReal {R : Type u_1} [CommRing R] {T : Type u_3} [Field T] [Algebra R T] (w : AbsoluteValue T ℝ) :
UniformContinuousConstSMul R (WithAbs w)

The completion of a field at an absolute value. #

source
@[deprecated AddMonoidHomClass.isometry_of_norm (since := "2025-11-28")]
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.ofAbs) :
Isometry ⇑f

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

source
@[deprecated "Use `Isometry.dist_eq` in combination with `AddMonoidHomClass.isometry_of_norm`" (since := "2025-11-28")]
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.ofAbs) :
PseudoMetricSpace.induced (⇑f) inferInstance = (normedField v).toPseudoMetricSpace

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

source
@[deprecated "Use `IsUniformInducing.comap_uniformSpace in combination` with AddMonoidHomClass.isometry_of_norm" (since := "2025-11-28")]
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.ofAbs) :
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.

source
@[deprecated "Use `Isometry.isUniformInducing` in combination with AddMonoidHomClass.isometry_of_norm" (since := "2025-11-28")]
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.ofAbs) :
IsUniformInducing ⇑f

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

source
@[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
Instances For
    source
    @[implicit_reducible]
    noncomputable instance AbsoluteValue.Completion.instCoe {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) :
    Coe K v.Completion
    Equations
    source
    @[reducible, inline, deprecated "Use `Isometry.extensionHom` in combination with `AddMonoidHomClass.isometry_of_norm`" (since := "2025-11-28")]
    noncomputable 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.ofAbs) :
    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
    Instances For
      source
      @[deprecated "Use `Isometry.extensionHom_coe` in combination with `AddMonoidHomClass.isometry_of_norm`" (since := "2025-11-28")]
      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.ofAbs) (x : K) :
      ⋯.extensionHom ↑(WithAbs.toAbs v x) = f ((WithAbs.equiv v).symm x)
      source
      @[deprecated "Use `Isometry.dist_eq` in combination with `AddMonoidHomClass.isometry_of_norm`" (since := "2025-11-28")]
      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.ofAbs) (x y : v.Completion) :
      have f := ⋯.extensionHom; dist (f x) (f 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.

      source
      @[deprecated "Use `Isometry.completion_extension` in combination with `AddMonoidHomClass.isometry_of_norm`" (since := "2025-11-28")]
      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.ofAbs) :
      Isometry ⇑⋯.extensionHom

      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.

      source
      @[deprecated "Use `Isometry.isClosedEmbedding` in combination with `Isometry.completion_extension` and `AddMonoidHomClass.isometry_of_norm`" (since := "2025-11-28")]
      theorem AbsoluteValue.Completion.isClosedEmbedding_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.ofAbs) :
      Topology.IsClosedEmbedding ⇑⋯.extensionHom

      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.

      source
      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 : Isometry ⇑f) :
      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.