Documentation

Mathlib.Analysis.Normed.Algebra.Norm

Algebra norms #

We define algebra norms and multiplicative algebra norms.

Main Definitions #

Tags #

norm, algebra norm

structure AlgebraNorm (R : Type u_1) [SeminormedCommRing R] (S : Type u_2) [Ring S] [Algebra R S] extends RingNorm :
Type u_2

An algebra norm on an R-algebra S is a ring norm on S compatible with the action of R.

  • toFun : S
  • map_zero' : self.toFun 0 = 0
  • add_le' : ∀ (r s : S), self.toFun (r + s) self.toFun r + self.toFun s
  • neg' : ∀ (r : S), self.toFun (-r) = self.toFun r
  • mul_le' : ∀ (x y : S), self.toFun (x * y) self.toFun x * self.toFun y
  • eq_zero_of_map_eq_zero' : ∀ (x : S), self.toFun x = 0x = 0
  • smul' : ∀ (a : R) (x : S), self.toFun (a x) = a * self.toFun x

    The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm.

Instances For
    Equations
    • instInhabitedAlgebraNorm K = { default := { toFun := norm, map_zero' := , add_le' := , neg' := , mul_le' := , eq_zero_of_map_eq_zero' := , smul' := } }
    class AlgebraNormClass (F : Type u_1) (R : outParam (Type u_2)) [SeminormedCommRing R] (S : outParam (Type u_3)) [Ring S] [Algebra R S] [FunLike F S ] extends RingNormClass :

    AlgebraNormClass F R S states that F is a type of R-algebra norms on the ring S. You should extend this class when you extend AlgebraNorm.

    • map_add_le_add : ∀ (f : F) (a b : S), f (a + b) f a + f b
    • map_zero : ∀ (f : F), f 0 = 0
    • map_neg_eq_map : ∀ (f : F) (a : S), f (-a) = f a
    • map_mul_le_mul : ∀ (f : F) (a b : S), f (a * b) f a * f b
    • eq_zero_of_map_eq_zero : ∀ (f : F) {a : S}, f a = 0a = 0
    • map_smul_eq_mul : ∀ (f : F) (a : R) (x : S), f (a x) = a * f x

      The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm.

    Instances
      def AlgebraNorm.toRingSeminorm' {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [Ring S] [Algebra R S] (f : AlgebraNorm R S) :

      The ring seminorm underlying an algebra norm.

      Equations
      • f.toRingSeminorm' = f.toRingSeminorm
      Instances For
        instance AlgebraNorm.instFunLikeReal {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [Ring S] [Algebra R S] :
        Equations
        • AlgebraNorm.instFunLikeReal = { coe := fun (f : AlgebraNorm R S) => f.toFun, coe_injective' := }
        Equations
        • =
        theorem AlgebraNorm.toFun_eq_coe {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [Ring S] [Algebra R S] (p : AlgebraNorm R S) :
        p.toFun = p
        theorem AlgebraNorm.ext_iff {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [Ring S] [Algebra R S] {p : AlgebraNorm R S} {q : AlgebraNorm R S} :
        p = q ∀ (x : S), p x = q x
        theorem AlgebraNorm.ext {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [Ring S] [Algebra R S] {p : AlgebraNorm R S} {q : AlgebraNorm R S} :
        (∀ (x : S), p x = q x)p = q
        theorem AlgebraNorm.extends_norm' {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [Ring S] [Algebra R S] {f : AlgebraNorm R S} (hf1 : f 1 = 1) (a : R) :
        f (a 1) = a

        An R-algebra norm such that f 1 = 1 extends the norm on R.

        theorem AlgebraNorm.extends_norm {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [Ring S] [Algebra R S] {f : AlgebraNorm R S} (hf1 : f 1 = 1) (a : R) :
        f ((algebraMap R S) a) = a

        An R-algebra norm such that f 1 = 1 extends the norm on R.

        def AlgebraNorm.restriction {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [Ring S] [Algebra R S] (A : Subalgebra R S) (f : AlgebraNorm R S) :

        The restriction of an algebra norm to a subalgebra.

        Equations
        • AlgebraNorm.restriction A f = { toFun := fun (x : A) => f x, map_zero' := , add_le' := , neg' := , mul_le' := , eq_zero_of_map_eq_zero' := , smul' := }
        Instances For
          def AlgebraNorm.isScalarTower_restriction {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [Ring S] [Algebra R S] {A : Type u_3} [CommRing A] [Algebra R A] [Algebra A S] [IsScalarTower R A S] (hinj : Function.Injective (algebraMap A S)) (f : AlgebraNorm R S) :

          The restriction of an algebra norm in a scalar tower.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            structure MulAlgebraNorm (R : Type u_1) [SeminormedCommRing R] (S : Type u_2) [Ring S] [Algebra R S] extends MulRingNorm :
            Type u_2

            A multiplicative algebra norm on an R-algebra norm S is a multiplicative ring norm on S compatible with the action of R.

            • toFun : S
            • map_zero' : self.toFun 0 = 0
            • add_le' : ∀ (r s : S), self.toFun (r + s) self.toFun r + self.toFun s
            • neg' : ∀ (r : S), self.toFun (-r) = self.toFun r
            • map_one' : self.toFun 1 = 1
            • map_mul' : ∀ (x y : S), self.toFun (x * y) = self.toFun x * self.toFun y
            • eq_zero_of_map_eq_zero' : ∀ (x : S), self.toFun x = 0x = 0
            • smul' : ∀ (a : R) (x : S), self.toFun (a x) = a * self.toFun x

              The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm.

            Instances For
              Equations
              • instInhabitedMulAlgebraNorm K = { default := { toFun := norm, map_zero' := , add_le' := , neg' := , map_one' := , map_mul' := , eq_zero_of_map_eq_zero' := , smul' := } }
              class MulAlgebraNormClass (F : Type u_1) (R : outParam (Type u_2)) [SeminormedCommRing R] (S : outParam (Type u_3)) [Ring S] [Algebra R S] [FunLike F S ] extends MulRingNormClass :

              MulAlgebraNormClass F R S states that F is a type of multiplicative R-algebra norms on the ring S. You should extend this class when you extend MulAlgebraNorm.

              • map_add_le_add : ∀ (f : F) (a b : S), f (a + b) f a + f b
              • map_zero : ∀ (f : F), f 0 = 0
              • map_neg_eq_map : ∀ (f : F) (a : S), f (-a) = f a
              • map_mul : ∀ (f : F) (x y : S), f (x * y) = f x * f y
              • map_one : ∀ (f : F), f 1 = 1
              • eq_zero_of_map_eq_zero : ∀ (f : F) {a : S}, f a = 0a = 0
              • map_smul_eq_mul : ∀ (f : F) (a : R) (x : S), f (a x) = a * f x

                The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm.

              Instances
                Equations
                • MulAlgebraNorm.instFunLikeReal = { coe := fun (f : MulAlgebraNorm R S) => f.toFun, coe_injective' := }
                theorem MulAlgebraNorm.toFun_eq_coe {R : outParam (Type u_1)} {S : outParam (Type u_2)} [SeminormedCommRing R] [Ring S] [Algebra R S] (p : MulAlgebraNorm R S) :
                p.toFun = p
                theorem MulAlgebraNorm.ext_iff {R : outParam (Type u_1)} {S : outParam (Type u_2)} [SeminormedCommRing R] [Ring S] [Algebra R S] {p : MulAlgebraNorm R S} {q : MulAlgebraNorm R S} :
                p = q ∀ (x : S), p x = q x
                theorem MulAlgebraNorm.ext {R : outParam (Type u_1)} {S : outParam (Type u_2)} [SeminormedCommRing R] [Ring S] [Algebra R S] {p : MulAlgebraNorm R S} {q : MulAlgebraNorm R S} :
                (∀ (x : S), p x = q x)p = q
                theorem MulAlgebraNorm.extends_norm' {R : outParam (Type u_1)} {S : outParam (Type u_2)} [SeminormedCommRing R] [Ring S] [Algebra R S] (f : MulAlgebraNorm R S) (a : R) :
                f (a 1) = a

                A multiplicative R-algebra norm extends the norm on R.

                theorem MulAlgebraNorm.extends_norm {R : outParam (Type u_1)} {S : outParam (Type u_2)} [SeminormedCommRing R] [Ring S] [Algebra R S] (f : MulAlgebraNorm R S) (a : R) :
                f ((algebraMap R S) a) = a

                A multiplicative R-algebra norm extends the norm on R.

                The ring norm underlying a multiplicative ring norm.

                Equations
                • f.toRingNorm = { toFun := f, map_zero' := , add_le' := , neg' := , mul_le' := , eq_zero_of_map_eq_zero' := }
                Instances For
                  theorem MulRingNorm.isPowMul {A : Type u_2} [Ring A] (f : MulRingNorm A) :

                  A multiplicative ring norm is power-multiplicative.