Algebraic order homomorphism classes #
This file defines hom classes for common properties at the intersection of order theory and algebra.
Typeclasses #
Basic typeclasses
NonnegHomClass
: Homs are nonnegative:∀ f a, 0 ≤ f a
SubadditiveHomClass
: Homs are subadditive:∀ f a b, f (a + b) ≤ f a + f b
SubmultiplicativeHomClass
: Homs are submultiplicative:∀ f a b, f (a * b) ≤ f a * f b
MulLEAddHomClass
:∀ f a b, f (a * b) ≤ f a + f b
NonarchimedeanHomClass
:∀ a b, f (a + b) ≤ max (f a) (f b)
Group norms
AddGroupSeminormClass
: Homs are nonnegative, subadditive, even and preserve zero.GroupSeminormClass
: Homs are nonnegative, respectf (a * b) ≤ f a + f b
,f a⁻¹ = f a
and preserve zero.AddGroupNormClass
: Homs are seminorms such thatf x = 0 → x = 0
for allx
.GroupNormClass
: Homs are seminorms such thatf x = 0 → x = 1
for allx
.
Ring norms
RingSeminormClass
: Homs are submultiplicative group norms.RingNormClass
: Homs are ring seminorms that are also additive group norms.MulRingSeminormClass
: Homs are ring seminorms that are multiplicative.MulRingNormClass
: Homs are ring norms that are multiplicative.
Notes #
Typeclasses for seminorms are defined here while types of seminorms are defined in
Analysis.Normed.Group.Seminorm
and Analysis.Normed.Ring.Seminorm
because absolute values are
multiplicative ring norms but outside of this use we only consider real-valued seminorms.
TODO #
Finitary versions of the current lemmas.
Basics #
the image of any element is non negative.
map_nonneg : ∀ (f : F) (a : α), 0 ≤ ↑f a
NonnegHomClass F α β
states that F
is a type of nonnegative morphisms.
Instances
the image of a sum is less or equal than the sum of the images.
SubadditiveHomClass F α β
states that F
is a type of subadditive morphisms.
Instances
the image of a product is less or equal than the product of the images.
SubmultiplicativeHomClass F α β
states that F
is a type of submultiplicative morphisms.
Instances
the image of a product is less or equal than the sum of the images.
MulLEAddHomClass F α β
states that F
is a type of subadditive morphisms.
Instances
the image of a sum is less or equal than the maximum of the images.
NonarchimedeanHomClass F α β
states that F
is a type of non-archimedean morphisms.
Instances
Group (semi)norms #
The image of zero is zero.
map_zero : ∀ (f : F), ↑f 0 = 0The map is invariant under negation of its argument.
AddGroupSeminormClass F α
states that F
is a type of β
-valued seminorms on the additive
group α
.
You should extend this class when you extend AddGroupSeminorm
.
Instances
The image of one is zero.
map_one_eq_zero : ∀ (f : F), ↑f 1 = 0The map is invariant under inversion of its argument.
GroupSeminormClass F α
states that F
is a type of β
-valued seminorms on the group α
.
You should extend this class when you extend GroupSeminorm
.
Instances
The argument is zero if its image under the map is zero.
AddGroupNormClass F α
states that F
is a type of β
-valued norms on the additive group
α
.
You should extend this class when you extend AddGroupNorm
.
Instances
The argument is one if its image under the map is zero.
GroupNormClass F α
states that F
is a type of β
-valued norms on the group α
.
You should extend this class when you extend GroupNorm
.
Instances
Equations
- AddGroupSeminormClass.toAddLEAddHomClass = self.1
Equations
- AddGroupSeminormClass.toZeroHomClass = let src := inst; ZeroHomClass.mk (_ : ∀ (f : F), ↑f 0 = 0)
Equations
- AddGroupSeminormClass.toNonnegHomClass = let src := inst; NonnegHomClass.mk (_ : ∀ (f : F) (a : α), 0 ≤ ↑f a)
Equations
- GroupSeminormClass.toNonnegHomClass = let src := inst; NonnegHomClass.mk (_ : ∀ (f : F) (a : α), 0 ≤ ↑f a)
Ring (semi)norms #
the image of a product is less or equal than the product of the images.
RingSeminormClass F α
states that F
is a type of β
-valued seminorms on the ring α
.
You should extend this class when you extend RingSeminorm
.
Instances
The argument is zero if its image under the map is zero.
RingNormClass F α
states that F
is a type of β
-valued norms on the ring α
.
You should extend this class when you extend RingNorm
.
Instances
The proposition that the function preserves multiplication
The proposition that the function preserves 1
map_one : ∀ (f : F), ↑f 1 = 1
MulRingSeminormClass F α
states that F
is a type of β
-valued multiplicative seminorms
on the ring α
.
You should extend this class when you extend MulRingSeminorm
.
Instances
The argument is zero if its image under the map is zero.
MulRingNormClass F α
states that F
is a type of β
-valued multiplicative norms on the
ring α
.
You should extend this class when you extend MulRingNorm
.
Instances
Equations
- RingSeminormClass.toNonnegHomClass = AddGroupSeminormClass.toNonnegHomClass
Equations
- MulRingSeminormClass.toRingSeminormClass = let src := inst; RingSeminormClass.mk (_ : ∀ (f : F) (a b : α), ↑f (a * b) ≤ ↑f a * ↑f b)
Equations
- MulRingNormClass.toRingNormClass = let src := inst; let src_1 := MulRingSeminormClass.toRingSeminormClass; RingNormClass.mk (_ : ∀ (f : F) {a : α}, ↑f a = 0 → a = 0)