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.

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

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

Canonical equivalence between WithAbs v and R.

Equations

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

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

Equations

• ⋯ = ⋯

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_1} [Semiring R] (v : AbsoluteValue R ℝ) [Ring 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 }

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

Equations

• WithAbs.normedRing v = v.toNormedRing

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

Equations

• WithAbs.normedField v = v.toNormedField

WithAbs.equiv preserves the ring structure.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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)