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) [NonUnitalNonAssocRing R] extends AddGroupSeminorm : Type u_4

• toFun : R → ℝ
• map_zero' : AddGroupSeminorm.toFun s.toAddGroupSeminorm 0 = 0
• add_le' : ∀ (r s_1 : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (r + s_1) ≤ AddGroupSeminorm.toFun s.toAddGroupSeminorm r + AddGroupSeminorm.toFun s.toAddGroupSeminorm s_1
• neg' : ∀ (r : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (-r) = AddGroupSeminorm.toFun s.toAddGroupSeminorm r
• mul_le' : ∀ (x y : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (x * y) ≤ AddGroupSeminorm.toFun s.toAddGroupSeminorm x * AddGroupSeminorm.toFun s.toAddGroupSeminorm 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.

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.

structure RingNorm (R : Type u_4) [NonUnitalNonAssocRing R] extends RingSeminorm : Type u_4

• toFun : R → ℝ
• map_zero' : AddGroupSeminorm.toFun s.toAddGroupSeminorm 0 = 0
• add_le' : ∀ (r s_1 : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (r + s_1) ≤ AddGroupSeminorm.toFun s.toAddGroupSeminorm r + AddGroupSeminorm.toFun s.toAddGroupSeminorm s_1
• neg' : ∀ (r : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (-r) = AddGroupSeminorm.toFun s.toAddGroupSeminorm r
• mul_le' : ∀ (x y : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (x * y) ≤ AddGroupSeminorm.toFun s.toAddGroupSeminorm x * AddGroupSeminorm.toFun s.toAddGroupSeminorm y
• eq_zero_of_map_eq_zero' : ∀ (x : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm x = 0 → x = 0

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

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

structure MulRingSeminorm (R : Type u_4) [NonAssocRing R] extends AddGroupSeminorm : Type u_4

• toFun : R → ℝ
• map_zero' : AddGroupSeminorm.toFun s.toAddGroupSeminorm 0 = 0
• add_le' : ∀ (r s_1 : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (r + s_1) ≤ AddGroupSeminorm.toFun s.toAddGroupSeminorm r + AddGroupSeminorm.toFun s.toAddGroupSeminorm s_1
• neg' : ∀ (r : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (-r) = AddGroupSeminorm.toFun s.toAddGroupSeminorm r
• map_one' : AddGroupSeminorm.toFun s.toAddGroupSeminorm 1 = 1

  The proposition that the function preserves 1

• map_mul' : ∀ (x y : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (x * y) = AddGroupSeminorm.toFun s.toAddGroupSeminorm x * AddGroupSeminorm.toFun s.toAddGroupSeminorm y

  The proposition that the function preserves multiplication

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.

structure MulRingNorm (R : Type u_4) [NonAssocRing R] extends MulRingSeminorm : Type u_4

• toFun : R → ℝ
• map_zero' : AddGroupSeminorm.toFun s.toAddGroupSeminorm 0 = 0
• add_le' : ∀ (r s_1 : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (r + s_1) ≤ AddGroupSeminorm.toFun s.toAddGroupSeminorm r + AddGroupSeminorm.toFun s.toAddGroupSeminorm s_1
• neg' : ∀ (r : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (-r) = AddGroupSeminorm.toFun s.toAddGroupSeminorm r
• map_one' : AddGroupSeminorm.toFun s.toAddGroupSeminorm 1 = 1
• map_mul' : ∀ (x y : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm (x * y) = AddGroupSeminorm.toFun s.toAddGroupSeminorm x * AddGroupSeminorm.toFun s.toAddGroupSeminorm y
• eq_zero_of_map_eq_zero' : ∀ (x : R), AddGroupSeminorm.toFun s.toAddGroupSeminorm x = 0 → x = 0

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

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

instance RingSeminorm.ringSeminormClass {R : Type u_2} [NonUnitalRing R] : RingSeminormClass (RingSeminorm R) R ℝ

instance RingSeminorm.instCoeFunRingSeminormToNonUnitalNonAssocRingForAllReal {R : Type u_2} [NonUnitalRing R] : CoeFun (RingSeminorm R) fun x => R → ℝ

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun.

@[simp]

theorem RingSeminorm.toFun_eq_coe {R : Type u_2} [NonUnitalRing R] (p : RingSeminorm R) : ↑p.toAddGroupSeminorm = ↑p

theorem RingSeminorm.ext {R : Type u_2} [NonUnitalRing R] {p : RingSeminorm R} {q : RingSeminorm R} : (∀ (x : R), ↑p x = ↑q x) → p = q

instance RingSeminorm.instZeroRingSeminormToNonUnitalNonAssocRing {R : Type u_2} [NonUnitalRing R] : Zero (RingSeminorm R)

theorem RingSeminorm.eq_zero_iff {R : Type u_2} [NonUnitalRing R] {p : RingSeminorm R} : p = 0 ↔ ∀ (x : R), ↑p x = 0

theorem RingSeminorm.ne_zero_iff {R : Type u_2} [NonUnitalRing R] {p : RingSeminorm R} : p ≠ 0 ↔ ∃ x, ↑p x ≠ 0

instance RingSeminorm.instInhabitedRingSeminormToNonUnitalNonAssocRing {R : Type u_2} [NonUnitalRing R] : Inhabited (RingSeminorm R)

instance RingSeminorm.instOneRingSeminormToNonUnitalNonAssocRing {R : Type u_2} [NonUnitalRing R] [DecidableEq R] : One (RingSeminorm R)

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

@[simp]

theorem RingSeminorm.apply_one {R : Type u_2} [NonUnitalRing R] [DecidableEq R] (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 : RingSeminorm R) (hp : ↑p 1 ≤ 1) : ↑p 1 = 1 ↔ p ≠ 0

def normRingSeminorm (R : Type u_4) [NonUnitalSeminormedRing R] : RingSeminorm R

The norm of a NonUnitalSeminormedRing as a RingSeminorm.

instance RingNorm.ringNormClass {R : Type u_2} [NonUnitalRing R] : RingNormClass (RingNorm R) R ℝ

instance RingNorm.instCoeFunRingNormToNonUnitalNonAssocRingForAllReal {R : Type u_2} [NonUnitalRing R] : CoeFun (RingNorm R) fun x => R → ℝ

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun.

theorem RingNorm.ext {R : Type u_2} [NonUnitalRing R] {p : RingNorm R} {q : RingNorm R} : (∀ (x : R), AddGroupSeminorm.toFun p.toAddGroupSeminorm x = AddGroupSeminorm.toFun q.toAddGroupSeminorm x) → p = q

instance RingNorm.instOneRingNormToNonUnitalNonAssocRing (R : Type u_2) [NonUnitalRing R] [DecidableEq R] : One (RingNorm R)

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

@[simp]

theorem RingNorm.apply_one (R : Type u_2) [NonUnitalRing R] [DecidableEq R] (x : R) : AddGroupSeminorm.toFun 1.toAddGroupSeminorm x = if x = 0 then 0 else 1

instance RingNorm.instInhabitedRingNormToNonUnitalNonAssocRing (R : Type u_2) [NonUnitalRing R] [DecidableEq R] : Inhabited (RingNorm R)

instance MulRingSeminorm.mulRingSeminormClass {R : Type u_2} [NonAssocRing R] : MulRingSeminormClass (MulRingSeminorm R) R ℝ

instance MulRingSeminorm.instCoeFunMulRingSeminormForAllReal {R : Type u_2} [NonAssocRing R] : CoeFun (MulRingSeminorm R) fun x => R → ℝ

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun.

@[simp]

theorem MulRingSeminorm.toFun_eq_coe {R : Type u_2} [NonAssocRing R] (p : MulRingSeminorm R) : ↑p.toAddGroupSeminorm = ↑p

theorem MulRingSeminorm.ext {R : Type u_2} [NonAssocRing R] {p : MulRingSeminorm R} {q : MulRingSeminorm R} : (∀ (x : R), ↑p x = ↑q x) → p = q

instance MulRingSeminorm.instOneMulRingSeminorm {R : Type u_2} [NonAssocRing R] [DecidableEq R] [NoZeroDivisors R] [Nontrivial R] : One (MulRingSeminorm R)

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

@[simp]

theorem MulRingSeminorm.apply_one {R : Type u_2} [NonAssocRing R] [DecidableEq R] [NoZeroDivisors R] [Nontrivial R] (x : R) : ↑1 x = if x = 0 then 0 else 1

instance MulRingSeminorm.instInhabitedMulRingSeminorm {R : Type u_2} [NonAssocRing R] [DecidableEq R] [NoZeroDivisors R] [Nontrivial R] : Inhabited (MulRingSeminorm R)

instance MulRingNorm.mulRingNormClass {R : Type u_2} [NonAssocRing R] : MulRingNormClass (MulRingNorm R) R ℝ

instance MulRingNorm.instCoeFunMulRingNormForAllReal {R : Type u_2} [NonAssocRing R] : CoeFun (MulRingNorm R) fun x => R → ℝ

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun.

theorem MulRingNorm.ext {R : Type u_2} [NonAssocRing R] {p : MulRingNorm R} {q : MulRingNorm R} : (∀ (x : R), AddGroupSeminorm.toFun p.toAddGroupSeminorm x = AddGroupSeminorm.toFun q.toAddGroupSeminorm x) → p = q

instance MulRingNorm.instOneMulRingNorm (R : Type u_2) [NonAssocRing R] [DecidableEq R] [NoZeroDivisors R] [Nontrivial R] : One (MulRingNorm R)

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

@[simp]

theorem MulRingNorm.apply_one (R : Type u_2) [NonAssocRing R] [DecidableEq R] [NoZeroDivisors R] [Nontrivial R] (x : R) : AddGroupSeminorm.toFun 1.toAddGroupSeminorm x = if x = 0 then 0 else 1

instance MulRingNorm.instInhabitedMulRingNorm (R : Type u_2) [NonAssocRing R] [DecidableEq R] [NoZeroDivisors R] [Nontrivial R] : Inhabited (MulRingNorm R)

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

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

@[simp]

theorem normRingNorm_toFun (R : Type u_4) [NonUnitalNormedRing R] : ∀ (a : R), AddGroupSeminorm.toFun (normRingNorm R).toRingSeminorm.toAddGroupSeminorm a = ‖a‖

def normRingNorm (R : Type u_4) [NonUnitalNormedRing R] : RingNorm R

The norm of a NonUnitalNormedRing as a RingNorm.