# Seminorms and norms on rings #

This file defines seminorms and norms on rings. These definitions are useful when one needs to consider multiple (semi)norms on a given ring.

## Main declarations #

For a ring R:

• RingSeminorm: A seminorm on a ring R is a function f : R → ℝ that preserves zero, takes nonnegative values, is subadditive and submultiplicative and such that f (-x) = f x for all x ∈ R.
• RingNorm: A seminorm f is a norm if f x = 0 if and only if x = 0.
• MulRingSeminorm: A multiplicative seminorm on a ring R is a ring seminorm that preserves multiplication.
• MulRingNorm: A multiplicative norm on a ring R is a ring norm that preserves multiplication.

## Notes #

The corresponding hom classes are defined in Mathlib.Analysis.Order.Hom.Basic to be used by absolute values.

## References #

• [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert]

## Tags #

ring_seminorm, ring_norm

structure RingSeminorm (R : Type u_4) extends :
Type u_4

A seminorm on a ring R is a function f : R → ℝ that preserves zero, takes nonnegative values, is subadditive and submultiplicative and such that f (-x) = f x for all x ∈ R.

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

The property of a RingSeminorm that for all x and y in the ring, the norm of x * y is less than the norm of x times the norm of y.

Instances For
theorem RingSeminorm.mul_le' {R : Type u_4} (self : ) (x : R) (y : R) :
self.toFun (x * y) self.toFun x * self.toFun y

The property of a RingSeminorm that for all x and y in the ring, the norm of x * y is less than the norm of x times the norm of y.

structure RingNorm (R : Type u_4) extends :
Type u_4

A function f : R → ℝ is a norm on a (nonunital) ring if it is a seminorm and f x = 0 implies x = 0.

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

If the image under the seminorm is zero, then the argument is zero.

Instances For
structure MulRingSeminorm (R : Type u_4) [] extends :
Type u_4

A multiplicative seminorm on a ring R is a function f : R → ℝ that preserves zero and multiplication, takes nonnegative values, is subadditive and such that f (-x) = f x for all x.

• toFun : R
• map_zero' : self.toFun 0 = 0
• add_le' : ∀ (r s : R), self.toFun (r + s) self.toFun r + self.toFun s
• neg' : ∀ (r : R), self.toFun (-r) = self.toFun r
• map_one' : self.toFun 1 = 1

The proposition that the function preserves 1

• map_mul' : ∀ (x y : R), self.toFun (x * y) = self.toFun x * self.toFun y

The proposition that the function preserves multiplication

Instances For
structure MulRingNorm (R : Type u_4) [] extends :
Type u_4

A multiplicative norm on a ring R is a multiplicative ring seminorm such that f x = 0 implies x = 0.

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

If the image under the seminorm is zero, then the argument is zero.

Instances For
instance RingSeminorm.funLike {R : Type u_2} [] :
Equations
• RingSeminorm.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance RingSeminorm.ringSeminormClass {R : Type u_2} [] :
Equations
• =
@[simp]
theorem RingSeminorm.toFun_eq_coe {R : Type u_2} [] (p : ) :
theorem RingSeminorm.ext {R : Type u_2} [] {p : } {q : } :
(∀ (x : R), p x = q x)p = q
instance RingSeminorm.instZero {R : Type u_2} [] :
Zero ()
Equations
• RingSeminorm.instZero = { zero := let __src := Zero.zero; { toAddGroupSeminorm := __src, mul_le' := } }
theorem RingSeminorm.eq_zero_iff {R : Type u_2} [] {p : } :
p = 0 ∀ (x : R), p x = 0
theorem RingSeminorm.ne_zero_iff {R : Type u_2} [] {p : } :
p 0 ∃ (x : R), p x 0
instance RingSeminorm.instInhabited {R : Type u_2} [] :
Equations
• RingSeminorm.instInhabited = { default := 0 }
instance RingSeminorm.instOneOfDecidableEq {R : Type u_2} [] [] :
One ()

The trivial seminorm on a ring R is the RingSeminorm taking value 0 at 0 and 1 at every other element.

Equations
• RingSeminorm.instOneOfDecidableEq = { one := let __src := 1; { toAddGroupSeminorm := __src, mul_le' := } }
@[simp]
theorem RingSeminorm.apply_one {R : Type u_2} [] [] (x : R) :
1 x = if x = 0 then 0 else 1
theorem RingSeminorm.seminorm_one_eq_one_iff_ne_zero {R : Type u_2} [Ring R] (p : ) (hp : p 1 1) :
p 1 = 1 p 0
def normRingSeminorm (R : Type u_4) :

The norm of a NonUnitalSeminormedRing as a RingSeminorm.

Equations
• = let __src := ; { toFun := norm, map_zero' := , add_le' := , neg' := , mul_le' := }
Instances For
instance RingNorm.funLike {R : Type u_2} [] :
Equations
• RingNorm.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance RingNorm.ringNormClass {R : Type u_2} [] :
Equations
• =
theorem RingNorm.toFun_eq_coe {R : Type u_2} [] (p : ) :
p.toFun = p
theorem RingNorm.ext {R : Type u_2} [] {p : } {q : } :
(∀ (x : R), p x = q x)p = q
instance RingNorm.instOneOfDecidableEq (R : Type u_2) [] [] :
One ()

The trivial norm on a ring R is the RingNorm taking value 0 at 0 and 1 at every other element.

Equations
• = { one := let __src := 1; let __src_1 := 1; { toRingSeminorm := __src, eq_zero_of_map_eq_zero' := } }
@[simp]
theorem RingNorm.apply_one (R : Type u_2) [] [] (x : R) :
1 x = if x = 0 then 0 else 1
instance RingNorm.instInhabitedOfDecidableEq (R : Type u_2) [] [] :
Equations
• = { default := 1 }
instance MulRingSeminorm.funLike {R : Type u_2} [] :
Equations
• MulRingSeminorm.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
Equations
• =
@[simp]
theorem MulRingSeminorm.toFun_eq_coe {R : Type u_2} [] (p : ) :
theorem MulRingSeminorm.ext {R : Type u_2} [] {p : } {q : } :
(∀ (x : R), p x = q x)p = q
instance MulRingSeminorm.instOne {R : Type u_2} [] [] [] [] :

The trivial seminorm on a ring R is the MulRingSeminorm taking value 0 at 0 and 1 at every other element.

Equations
• MulRingSeminorm.instOne = { one := let __src := 1; { toAddGroupSeminorm := __src, map_one' := , map_mul' := } }
@[simp]
theorem MulRingSeminorm.apply_one {R : Type u_2} [] [] [] [] (x : R) :
1 x = if x = 0 then 0 else 1
instance MulRingSeminorm.instInhabited {R : Type u_2} [] [] [] [] :
Equations
• MulRingSeminorm.instInhabited = { default := 1 }
instance MulRingNorm.funLike {R : Type u_2} [] :
Equations
• MulRingNorm.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance MulRingNorm.mulRingNormClass {R : Type u_2} [] :
Equations
• =
theorem MulRingNorm.toFun_eq_coe {R : Type u_2} [] (p : ) :
p.toFun = p
theorem MulRingNorm.ext {R : Type u_2} [] {p : } {q : } :
(∀ (x : R), p x = q x)p = q
instance MulRingNorm.instOne (R : Type u_2) [] [] [] [] :
One ()

The trivial norm on a ring R is the MulRingNorm taking value 0 at 0 and 1 at every other element.

Equations
• = { one := let __src := 1; let __src_1 := 1; { toMulRingSeminorm := __src, eq_zero_of_map_eq_zero' := } }
@[simp]
theorem MulRingNorm.apply_one (R : Type u_2) [] [] [] [] (x : R) :
1 x = if x = 0 then 0 else 1
instance MulRingNorm.instInhabited (R : Type u_2) [] [] [] [] :
Equations
• = { default := 1 }
def MulRingNorm.equiv {R : Type u_4} [Ring R] (f : ) (g : ) :

Two multiplicative ring norms f, g on R are equivalent if there exists a positive constant c such that for all x ∈ R, (f x)^c = g x.

Equations
• f.equiv g = ∃ (c : ), 0 < c (fun (x : R) => f x ^ c) = g
Instances For
theorem MulRingNorm.equiv_refl {R : Type u_4} [Ring R] (f : ) :
f.equiv f

Equivalence of multiplicative ring norms is reflexive.

theorem MulRingNorm.equiv_symm {R : Type u_4} [Ring R] {f : } {g : } (hfg : f.equiv g) :
g.equiv f

Equivalence of multiplicative ring norms is symmetric.

theorem MulRingNorm.equiv_trans {R : Type u_4} [Ring R] {f : } {g : } {k : } (hfg : f.equiv g) (hgk : g.equiv k) :
f.equiv k

Equivalence of multiplicative ring norms is transitive.

def RingSeminorm.toRingNorm {K : Type u_4} [] (f : ) (hnt : f 0) :

A nonzero ring seminorm on a field K is a ring norm.

Equations
• f.toRingNorm hnt = { toRingSeminorm := f, eq_zero_of_map_eq_zero' := }
Instances For
@[simp]
theorem normRingNorm_toFun (R : Type u_4) :
∀ (a : R), ().toFun a = a
def normRingNorm (R : Type u_4) :

The norm of a NonUnitalNormedRing as a RingNorm.

Equations
• = let __src := ; let __src_1 := ; { toAddGroupSeminorm := __src.toAddGroupSeminorm, mul_le' := , eq_zero_of_map_eq_zero' := }
Instances For
theorem MulRingNorm_nat_le_nat {R : Type u_4} [Ring R] (n : ) (f : ) :
f n n

A multiplicative ring norm satisfies f n ≤ n for every n : ℕ.