Documentation

Mathlib.Analysis.Normed.Ring.WithAbs

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 #

def WithAbs {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] :
AbsoluteValue R SType 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
Instances For
    instance WithAbs.instInhabited {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) :
    Equations
    def WithAbs.equiv {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) :

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

    Equations
    Instances For
      def WithAbs.equivWithAbs {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v w : AbsoluteValue R S) :

      The canonical (semiring) equivalence between WithAbs v and WithAbs w, for any two absolute values v and w on R.

      Equations
      Instances For
        theorem WithAbs.equivWithAbs_symm {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v w : AbsoluteValue R S) :
        @[simp]
        theorem WithAbs.equiv_equivWithAbs_symm_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] {v w : AbsoluteValue R S} {x : WithAbs w} :
        (equiv v) ((equivWithAbs v w).symm x) = (equiv w) x
        @[simp]
        theorem WithAbs.equivWithAbs_equiv_symm_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] {v w : AbsoluteValue R S} {x : R} :
        (equivWithAbs v w) ((equiv v).symm x) = (equiv w).symm x
        @[simp]
        theorem WithAbs.equivWithAbs_symm_equiv_symm_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] {v w : AbsoluteValue R S} {x : R} :
        (equivWithAbs v w).symm ((equiv w).symm x) = (equiv v).symm x
        instance WithAbs.instRing {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Ring R] (v : AbsoluteValue R S) :
        Equations
        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} [Semiring S] [PartialOrder S] {R' : Type u_3} [Semiring R] [AddCommGroup R'] [Module R R'] (v : AbsoluteValue R S) :
        Equations
        instance WithAbs.instModule_right {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] {R' : Type u_3} [Semiring R] [Semiring R'] [Module R R'] (v : AbsoluteValue R' S) :
        Equations
        instance WithAbs.instAlgebra_left {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] {R' : Type u_3} [CommSemiring R] [Semiring R'] [Algebra R R'] (v : AbsoluteValue R S) :
        Equations
        theorem WithAbs.algebraMap_left_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] {R' : Type u_3} [CommSemiring R] [Semiring R'] [Algebra R R'] (v : AbsoluteValue R S) (x : WithAbs v) :
        (algebraMap (WithAbs v) R') x = (algebraMap R R') ((equiv v) x)
        instance WithAbs.instAlgebra_right {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] {R' : Type u_3} [CommSemiring R] [Semiring R'] [Algebra R R'] (v : AbsoluteValue R' S) :
        Equations
        theorem WithAbs.algebraMap_right_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] {R' : Type u_3} [CommSemiring R] [Semiring R'] [Algebra R R'] (v : AbsoluteValue R' S) (x : R) :
        (algebraMap R (WithAbs v)) x = (equiv v) ((algebraMap R R') x)
        theorem WithAbs.equiv_algebraMap_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] {R' : Type u_3} [CommSemiring R] [Semiring R'] [Algebra R R'] (v : AbsoluteValue R S) (w : AbsoluteValue R' S) (x : WithAbs v) :
        (equiv w) ((algebraMap (WithAbs v) (WithAbs w)) x) = (algebraMap R R') ((equiv v) x)
        def WithAbs.algEquiv {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] {R' : Type u_3} [CommSemiring R] [Semiring R'] [Algebra R R'] (v : AbsoluteValue R' S) :

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

        Equations
        Instances For