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.

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} [OrderedSemiring S] [Semiring R] : 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.

This is also helpful when dealing with several absolute values on the same semiring.

Equations

• WithAbs x✝ = R

instance WithAbs.instNontrivial {R : Type u_1} {S : Type u_2} [OrderedSemiring S] [Semiring R] (v : AbsoluteValue R S) [Nontrivial R] : Nontrivial (WithAbs v)

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

Equations

• WithAbs.instUnique v = inferInstanceAs (Unique R)

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

Equations

• WithAbs.instSemiring v = inferInstanceAs (Semiring R)

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

Equations

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

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

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

Equations

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

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

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

WithAbs.equiv as a ring equivalence.

Equations

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

instance WithAbs.instCommSemiring {R : Type u_1} {S : Type u_2} [OrderedSemiring S] [CommSemiring R] (v : AbsoluteValue R S) : CommSemiring (WithAbs v)

Equations

• WithAbs.instCommSemiring v = inferInstanceAs (CommSemiring R)

instance WithAbs.instRing {R : Type u_1} {S : Type u_2} [OrderedSemiring S] [Ring R] (v : AbsoluteValue R S) : Ring (WithAbs v)

Equations

• WithAbs.instRing v = inferInstanceAs (Ring R)

instance WithAbs.instCommRing {R : Type u_1} {S : Type u_2} [OrderedSemiring S] [CommRing R] (v : AbsoluteValue R S) : CommRing (WithAbs v)

Equations

• WithAbs.instCommRing v = inferInstanceAs (CommRing R)

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

Equations

• WithAbs.normedRing v = v.toNormedRing

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

instance WithAbs.instModule_left {R : Type u_1} {S : Type u_2} [OrderedSemiring S] {R' : Type u_3} [Semiring R] [AddCommGroup R'] [Module R R'] (v : AbsoluteValue R S) : Module (WithAbs v) R'

Equations

• WithAbs.instModule_left v = inferInstanceAs (Module R R')

instance WithAbs.instModule_right {R : Type u_1} {S : Type u_2} [OrderedSemiring S] {R' : Type u_3} [Semiring R] [Semiring R'] [Module R R'] (v : AbsoluteValue R' S) : Module R (WithAbs v)

Equations

• WithAbs.instModule_right v = inferInstanceAs (Module R R')

instance WithAbs.instAlgebra_left {R : Type u_1} {S : Type u_2} [OrderedSemiring S] {R' : Type u_3} [CommSemiring R] [Semiring R'] [Algebra R R'] (v : AbsoluteValue R S) : Algebra (WithAbs v) R'

Equations

• WithAbs.instAlgebra_left v = inferInstanceAs (Algebra R R')

instance WithAbs.instAlgebra_right {R : Type u_1} {S : Type u_2} [OrderedSemiring S] {R' : Type u_3} [CommSemiring R] [Semiring R'] [Algebra R R'] (v : AbsoluteValue R' S) : Algebra R (WithAbs v)

Equations

• WithAbs.instAlgebra_right v = inferInstanceAs (Algebra R R')

def WithAbs.algEquiv {R : Type u_1} {S : Type u_2} [OrderedSemiring S] {R' : Type u_3} [CommSemiring R] [Semiring R'] [Algebra R R'] (v : AbsoluteValue R' S) : WithAbs v ≃ₐ[R] R'

The canonical algebra isomorphism from an R-algebra R' with an absolute value v to R'.

Equations

• WithAbs.algEquiv v = AlgEquiv.refl

WithAbs.equiv preserves the ring structure.

These are deprecated as they are special cases of the generic map_zero etc. lemmas after WithAbs.equiv is defined to be a ring equivalence.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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