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 ringR
is a functionf : R → ℝ
that preserves zero, takes nonnegative values, is subadditive and submultiplicative and such thatf (-x) = f x
for allx ∈ R
.RingNorm
: A seminormf
is a norm iff x = 0
if and only ifx = 0
.MulRingSeminorm
: A multiplicative seminorm on a ringR
is a ring seminorm that preserves multiplication.MulRingNorm
: A multiplicative norm on a ringR
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 #
Tags #
ring_seminorm, ring_norm
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
The property of a
RingSeminorm
that for allx
andy
in the ring, the norm ofx * y
is less than the norm ofx
times the norm ofy
.
Instances For
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 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
- map_one' : self.toFun 1 = 1
The proposition that the function preserves 1
The proposition that the function preserves multiplication
Instances For
Equations
- RingSeminorm.funLike = { coe := fun (f : RingSeminorm R) => f.toFun, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Equations
- RingSeminorm.instZero = { zero := let __src := Zero.zero; { toAddGroupSeminorm := __src, mul_le' := ⋯ } }
Equations
- RingSeminorm.instInhabited = { default := 0 }
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' := ⋯ } }
The norm of a NonUnitalSeminormedRing
as a RingSeminorm
.
Equations
- normRingSeminorm R = { toFun := norm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
The trivial norm on a ring R
is the RingNorm
taking value 0
at 0
and 1
at every
other element.
Equations
- RingNorm.instOneOfDecidableEq R = { one := let __src := 1; let __src_1 := 1; { toRingSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }
Equations
- RingNorm.instInhabitedOfDecidableEq R = { default := 1 }
Equations
- MulRingSeminorm.funLike = { coe := fun (f : MulRingSeminorm R) => f.toFun, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
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' := ⋯ } }
Equations
- MulRingSeminorm.instInhabited = { default := 1 }
Equations
- MulRingNorm.funLike = { coe := fun (f : MulRingNorm R) => f.toFun, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
The trivial norm on a ring R
is the MulRingNorm
taking value 0
at 0
and 1
at every
other element.
Equations
- MulRingNorm.instOne R = { one := let __src := 1; let __src_1 := 1; { toMulRingSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }
Equations
- MulRingNorm.instInhabited R = { default := 1 }
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
.
Instances For
Equivalence of multiplicative ring norms is reflexive.
Equivalence of multiplicative ring norms is symmetric.
Equivalence of multiplicative ring norms is transitive.
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
The norm of a NonUnitalNormedRing
as a RingNorm
.
Equations
- normRingNorm R = { toAddGroupSeminorm := (normAddGroupNorm R).toAddGroupSeminorm, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }
Instances For
A multiplicative ring norm satisfies f n ≤ n
for every n : ℕ
.
A multiplicative norm composed with the absolute value on integers equals the norm itself.
The seminorm on a SeminormedRing
, as a RingSeminorm
.
Equations
- SeminormedRing.toRingSeminorm R = { toFun := norm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯ }
Instances For
The norm on a NormedRing
, as a RingNorm
.
Equations
- NormedRing.toRingNorm R = { toFun := norm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }
Instances For
The norm on a NormedField
, as a MulRingNorm
.
Equations
- NormedField.toMulRingNorm R = { toFun := norm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }