WithAbs

WithAbs v is a type synonym for a semiring R which depends on an absolute value. The point of this is to allow the type class inference system to handle multiple sources of instances that arise from absolute values. See NumberTheory.NumberField.Completion for an example of this being used to define Archimedean completions of a number field.

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. This can be used to assign and infer instances on a semiring that depend on absolute values.
• WithAbs.equiv v : the canonical (type) equivalence between WithAbs v and R.
• WithAbs.ringEquiv v : The canonical ring equivalence between WithAbs v and R.
• AbsoluteValue.Completion : the uniform space completion of a field K according to the uniform structure defined by the specified real absolute value.

def WithAbs {R : Type u_1} {S : Type u_3} [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.instNonTrivial {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) [Nontrivial R] : Nontrivial (WithAbs v)

instance WithAbs.instUnique {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) [Unique R] : Unique (WithAbs v)

Equations

• WithAbs.instUnique v = inferInstanceAs (Unique R)

instance WithAbs.instSemiring {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) : Semiring (WithAbs v)

Equations

• WithAbs.instSemiring v = inferInstanceAs (Semiring R)

instance WithAbs.instRing {R' : Type u_2} [Ring R'] (v' : AbsoluteValue R' ℝ) : Ring (WithAbs v')

Equations

• WithAbs.instRing v' = inferInstanceAs (Ring R')

instance WithAbs.instInhabited {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) : Inhabited (WithAbs v)

Equations

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

def WithAbs.equiv {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) : WithAbs v ≃+* R

The canonical (semiring) equivalence between WithAbs v and R.

Equations

• WithAbs.equiv v = RingEquiv.refl (WithAbs v)

instance WithAbs.normedRing {R' : Type u_2} [Ring R'] (v' : AbsoluteValue R' ℝ) : NormedRing (WithAbs v')

Equations

• WithAbs.normedRing v' = v'.toNormedRing

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

Equations

• WithAbs.normedField v = v.toNormedField

WithAbs.equiv preserves the ring structure.

@[simp, deprecated "Use map_zero" (since := "2025-01-13")]

theorem WithAbs.equiv_zero {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) : (WithAbs.equiv v) 0 = 0

@[simp, deprecated "Use map_zero" (since := "2025-01-13")]

theorem WithAbs.equiv_symm_zero {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) : (WithAbs.equiv v).symm 0 = 0

@[simp, deprecated "Use map_add" (since := "2025-01-13")]

theorem WithAbs.equiv_add {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (x y : WithAbs v) : (WithAbs.equiv v) (x + y) = (WithAbs.equiv v) x + (WithAbs.equiv v) y

@[simp, deprecated "Use map_add" (since := "2025-01-13")]

theorem WithAbs.equiv_symm_add {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (r s : R) : (WithAbs.equiv v).symm (r + s) = (WithAbs.equiv v).symm r + (WithAbs.equiv v).symm s

@[simp, deprecated "Use map_sub" (since := "2025-01-13")]

theorem WithAbs.equiv_sub {R' : Type u_2} [Ring R'] (v' : AbsoluteValue R' ℝ) (x' y' : WithAbs v') : (WithAbs.equiv v') (x' - y') = (WithAbs.equiv v') x' - (WithAbs.equiv v') y'

@[simp, deprecated "Use map_sub" (since := "2025-01-13")]

theorem WithAbs.equiv_symm_sub {R' : Type u_2} [Ring R'] (v' : AbsoluteValue R' ℝ) (r' s' : R') : (WithAbs.equiv v').symm (r' - s') = (WithAbs.equiv v').symm r' - (WithAbs.equiv v').symm s'

@[simp, deprecated "Use map_neg" (since := "2025-01-13")]

theorem WithAbs.equiv_neg {R' : Type u_2} [Ring R'] (v' : AbsoluteValue R' ℝ) (x' : WithAbs v') : (WithAbs.equiv v') (-x') = -(WithAbs.equiv v') x'

@[simp, deprecated "Use map_neg" (since := "2025-01-13")]

theorem WithAbs.equiv_symm_neg {R' : Type u_2} [Ring R'] (v' : AbsoluteValue R' ℝ) (r' : R') : (WithAbs.equiv v').symm (-r') = -(WithAbs.equiv v').symm r'

@[simp, deprecated "Use map_mul" (since := "2025-01-13")]

theorem WithAbs.equiv_mul {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (x y : WithAbs v) : (WithAbs.equiv v) (x * y) = (WithAbs.equiv v) x * (WithAbs.equiv v) y

@[simp, deprecated "Use map_mul" (since := "2025-01-13")]

theorem WithAbs.equiv_symm_mul {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (x y : WithAbs v) : (WithAbs.equiv v).symm (x * y) = (WithAbs.equiv v).symm x * (WithAbs.equiv v).symm y

@[deprecated WithAbs.equiv (since := "2025-01-13")]

def WithAbs.ringEquiv {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) : WithAbs v ≃+* R

WithAbs.equiv as a ring equivalence.

Equations

• WithAbs.ringEquiv v = RingEquiv.refl (WithAbs v)

The completion of a field at an absolute value.

theorem WithAbs.isometry_of_comp {K : Type u_5} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_6} [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_5} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_6} [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_5} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_6} [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_5} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_6} [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_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)

@[deprecated AbsoluteValue.Completion (since := "2024-12-01")]

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

Alias of AbsoluteValue.Completion.

---

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

Equations

• @AbsoluteValue.completion = @AbsoluteValue.Completion

instance AbsoluteValue.Completion.instCoe {K : Type u_1} [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_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) ↑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 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.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) : Topology.IsClosedEmbedding ⇑(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.