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 , Seminorm , RingSeminorm , AddGroupNorm , AddGroupSeminorm : Type u_2

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

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 , SeminormClass , RingSeminormClass , AddGroupNormClass , AddGroupSeminormClass , SubmultiplicativeHomClass , SubadditiveHomClass : 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.

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 {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 , Seminorm , MulRingSeminorm , AddGroupNorm , AddGroupSeminorm , MonoidWithZeroHom , ZeroHom , MonoidHom , OneHom , MulHom : 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.

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 , SeminormClass , MulRingSeminormClass , AddGroupNormClass , AddGroupSeminormClass , MonoidWithZeroHomClass , SubadditiveHomClass , MonoidHomClass , ZeroHomClass , MulHomClass , OneHomClass : 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.

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 {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.