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. MulRingNorm R is essentially the same as AbsoluteValue R ℝ, and it is recommended to use the latter instead to avoid duplicating results.

Notes

The corresponding hom classes are defined in Mathlib/Analysis/Order/Hom/Basic.lean 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_2) [NonUnitalNonAssocRing R] extends AddGroupSeminorm R : Type u_2

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.

structure RingNorm (R : Type u_2) [NonUnitalNonAssocRing R] extends RingSeminorm R, AddGroupNorm R : Type u_2

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

structure MulRingSeminorm (R : Type u_2) [NonAssocRing R] extends AddGroupSeminorm R, R →*₀ ℝ : Type u_2

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
• map_mul' (x y : R) : self.toFun (x * y) = self.toFun x * self.toFun y

structure MulRingNorm (R : Type u_2) [NonAssocRing R] extends MulRingSeminorm R, AddGroupNorm R : Type u_2

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

It is recommended to use AbsoluteValue R ℝ instead (which works for Semiring R and is equivalent to MulRingNorm R for a nontrivial Ring 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
• 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 = 0 → x = 0

instance RingSeminorm.funLike {R : Type u_1} [NonUnitalRing R] : FunLike (RingSeminorm R) R ℝ

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

@[simp]

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

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

theorem RingSeminorm.ext_iff {R : Type u_1} [NonUnitalRing R] {p q : RingSeminorm R} : p = q ↔ ∀ (x : R), p x = q x

instance RingSeminorm.instZero {R : Type u_1} [NonUnitalRing R] : Zero (RingSeminorm R)

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

theorem RingSeminorm.ne_zero_iff {R : Type u_1} [NonUnitalRing R] {p : RingSeminorm R} : p ≠ 0 ↔ ∃ (x : R), p x ≠ 0

instance RingSeminorm.instInhabited {R : Type u_1} [NonUnitalRing R] : Inhabited (RingSeminorm R)

instance RingSeminorm.instOneOfDecidableEq {R : Type u_1} [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_1} [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_1} [Ring R] (p : RingSeminorm R) (hp : p 1 ≤ 1) : p 1 = 1 ↔ p ≠ 0

theorem RingSeminorm.exists_index_pow_le {R : Type u_1} [CommRing R] (p : RingSeminorm R) (hna : IsNonarchimedean ⇑p) (x y : R) (n : ℕ) : ∃ m < n + 1, p ((x + y) ^ n) ^ (1 / ↑n) ≤ (p (x ^ m) * p (y ^ (n - m))) ^ (1 / ↑n)

theorem map_pow_le_pow {F : Type u_2} {α : Type u_3} [Ring α] [FunLike F α ℝ] [RingSeminormClass F α ℝ] (f : F) (a : α) {n : ℕ} : n ≠ 0 → f (a ^ n) ≤ f a ^ n

If f is a ring seminorm on a, then ∀ {n : ℕ}, n ≠ 0 → f (a ^ n) ≤ f a ^ n.

theorem map_pow_le_pow' {F : Type u_2} {α : Type u_3} [Ring α] [FunLike F α ℝ] [RingSeminormClass F α ℝ] {f : F} (hf1 : f 1 ≤ 1) (a : α) (n : ℕ) : f (a ^ n) ≤ f a ^ n

If f is a ring seminorm on a with f 1 ≤ 1, then ∀ (n : ℕ), f (a ^ n) ≤ f a ^ n.

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

The norm of a NonUnitalSeminormedRing as a RingSeminorm.

theorem RingSeminorm.isBoundedUnder {R : Type u_1} [Ring R] (p : RingSeminorm R) (hp : p 1 ≤ 1) {s : ℕ → ℕ} (hs_le : ∀ (n : ℕ), s n ≤ n) {x : R} (ψ : ℕ → ℕ) : Filter.IsBoundedUnder LE.le Filter.atTop fun (n : ℕ) => p (x ^ s (ψ n)) ^ (1 / ↑(ψ n))

If f is a ring seminorm on R with f 1 ≤ 1 and s : ℕ → ℕ is bounded by n, then f (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ)) is eventually bounded.

instance RingNorm.funLike {R : Type u_1} [NonUnitalRing R] : FunLike (RingNorm R) R ℝ

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

theorem RingNorm.toFun_eq_coe {R : Type u_1} [NonUnitalRing R] (p : RingNorm R) : p.toFun = ⇑p

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

theorem RingNorm.ext_iff {R : Type u_1} [NonUnitalRing R] {p q : RingNorm R} : p = q ↔ ∀ (x : R), p x = q x

instance RingNorm.instOneOfDecidableEq (R : Type u_1) [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_1) [NonUnitalRing R] [DecidableEq R] (x : R) : 1 x = if x = 0 then 0 else 1

instance RingNorm.instInhabitedOfDecidableEq (R : Type u_1) [NonUnitalRing R] [DecidableEq R] : Inhabited (RingNorm R)

@[reducible, inline]

abbrev RingNorm.toNormedRing {R : Type u_1} [Ring R] (f : RingNorm R) : NormedRing R

The NormedRing structure on a ring R determined by a RingNorm

instance MulRingSeminorm.funLike {R : Type u_1} [NonAssocRing R] : FunLike (MulRingSeminorm R) R ℝ

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

@[simp]

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

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

theorem MulRingSeminorm.ext_iff {R : Type u_1} [NonAssocRing R] {p q : MulRingSeminorm R} : p = q ↔ ∀ (x : R), p x = q x

instance MulRingSeminorm.instOne {R : Type u_1} [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_1} [NonAssocRing R] [DecidableEq R] [NoZeroDivisors R] [Nontrivial R] (x : R) : 1 x = if x = 0 then 0 else 1

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

instance MulRingNorm.funLike {R : Type u_1} [NonAssocRing R] : FunLike (MulRingNorm R) R ℝ

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

theorem MulRingNorm.toFun_eq_coe {R : Type u_1} [NonAssocRing R] (p : MulRingNorm R) : p.toFun = ⇑p

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

theorem MulRingNorm.ext_iff {R : Type u_1} [NonAssocRing R] {p q : MulRingNorm R} : p = q ↔ ∀ (x : R), p x = q x

instance MulRingNorm.instOne (R : Type u_1) [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_1) [NonAssocRing R] [DecidableEq R] [NoZeroDivisors R] [Nontrivial R] (x : R) : 1 x = if x = 0 then 0 else 1

instance MulRingNorm.instInhabited (R : Type u_1) [NonAssocRing R] [DecidableEq R] [NoZeroDivisors R] [Nontrivial R] : Inhabited (MulRingNorm R)

def MulRingNorm.mulRingNormEquivAbsoluteValue {R : Type u_2} [Ring R] [Nontrivial R] : MulRingNorm R ≃ AbsoluteValue R ℝ

The equivalence of MulRingNorm R and AbsoluteValue R ℝ when R is a nontrivial ring.

theorem MulRingNorm.mulRingNormEquivAbsoluteValue_apply {R : Type u_2} [Ring R] [Nontrivial R] (N : MulRingNorm R) (x : R) : (mulRingNormEquivAbsoluteValue N) x = N x

theorem MulRingNorm.mulRingNormEquivAbsoluteValue_symm_apply {R : Type u_2} [Ring R] [Nontrivial R] (v : AbsoluteValue R ℝ) (x : R) : (mulRingNormEquivAbsoluteValue.symm v) x = v x

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

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

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

The norm of a NonUnitalNormedRing as a RingNorm.

@[simp]

theorem normRingNorm_toFun (R : Type u_2) [NonUnitalNormedRing R] (a✝ : R) : (normRingNorm R).toFun a✝ = ‖a✝‖

def SeminormedRing.toRingSeminorm (R : Type u_2) [SeminormedRing R] : RingSeminorm R

The seminorm on a SeminormedRing, as a RingSeminorm.

def NormedRing.toRingNorm (R : Type u_2) [NormedRing R] : RingNorm R

The norm on a NormedRing, as a RingNorm.

@[simp]

theorem NormedRing.toRingNorm_toFun (R : Type u_2) [NormedRing R] (a✝ : R) : (toRingNorm R).toFun a✝ = ‖a✝‖

@[simp]

theorem NormedRing.toRingNorm_apply (R : Type u_2) [NormedRing R] (x : R) : (toRingNorm R) x = ‖x‖

def NormedField.toMulRingNorm (R : Type u_2) [NormedField R] : MulRingNorm R

The norm on a NormedField, as a MulRingNorm.

def NormedField.toAbsoluteValue (R : Type u_2) [NormedField R] : AbsoluteValue R ℝ

The norm on a NormedField, as an AbsoluteValue.