Algebra norms

We define algebra norms and multiplicative algebra norms.

Main Definitions

• AlgebraNorm : an algebra norm on an R-algebra S is a ring norm on S compatible with the action of R.
• MulAlgebraNorm : a multiplicative algebra norm on an R-algebra S is a multiplicative ring norm on S compatible with the action of R.

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 = 0 → x = 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.

instance instInhabitedAlgebraNorm (K : Type u_1) [NormedField K] : Inhabited (AlgebraNorm K K)

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 : Prop

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 = 0 → a = 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.

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

The ring seminorm underlying an algebra norm.

Equations

• f.toRingSeminorm' = f.toRingSeminorm

instance AlgebraNorm.instFunLikeReal {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [Ring S] [Algebra R S] : FunLike (AlgebraNorm R S) S ℝ

Equations

• AlgebraNorm.instFunLikeReal = { coe := fun (f : AlgebraNorm R S) => f.toFun, coe_injective' := ⋯ }

instance AlgebraNorm.algebraNormClass {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [Ring S] [Algebra R S] : AlgebraNormClass (AlgebraNorm R S) R S

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) : AlgebraNorm R ↥A

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' := ⋯ }

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) : AlgebraNorm R A

The restriction of an algebra norm in a scalar tower.

Equations

• One or more equations did not get rendered due to their size.

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 = 0 → x = 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.

instance instInhabitedMulAlgebraNorm (K : Type u_1) [NormedField K] : Inhabited (MulAlgebraNorm K K)

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 : Prop

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 = 0 → a = 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.

instance MulAlgebraNorm.instFunLikeReal {R : outParam (Type u_1)} {S : outParam (Type u_2)} [SeminormedCommRing R] [Ring S] [Algebra R S] : FunLike (MulAlgebraNorm R S) S ℝ

Equations

• MulAlgebraNorm.instFunLikeReal = { coe := fun (f : MulAlgebraNorm R S) => f.toFun, coe_injective' := ⋯ }

instance MulAlgebraNorm.mulAlgebraNormClass {R : outParam (Type u_1)} {S : outParam (Type u_2)} [SeminormedCommRing R] [Ring S] [Algebra R S] : MulAlgebraNormClass (MulAlgebraNorm R S) R S

Equations

• ⋯ = ⋯

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.

def MulRingNorm.toRingNorm {R : Type u_1} [NonAssocRing R] (f : MulRingNorm R) : RingNorm 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' := ⋯ }

theorem MulRingNorm.isPowMul {A : Type u_2} [Ring A] (f : MulRingNorm A) : IsPowMul ⇑f

A multiplicative ring norm is power-multiplicative.