# mathlib3documentation

algebra.order.hom.basic

# Algebraic order homomorphism classes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines hom classes for common properties at the intersection of order theory and algebra.

## Typeclasses #

Basic typeclasses

• nonneg_hom_class: Homs are nonnegative: ∀ f a, 0 ≤ f a
• subadditive_hom_class: Homs are subadditive: ∀ f a b, f (a + b) ≤ f a + f b
• submultiplicative_hom_class: Homs are submultiplicative: ∀ f a b, f (a * b) ≤ f a * f b
• mul_le_add_hom_class: ∀ f a b, f (a * b) ≤ f a + f b
• nonarchimedean_hom_class: ∀ a b, f (a + b) ≤ max (f a) (f b)

Group norms

• add_group_seminorm_class: Homs are nonnegative, subadditive, even and preserve zero.
• group_seminorm_class: Homs are nonnegative, respect f (a * b) ≤ f a + f b, f a⁻¹ = f a and preserve zero.
• add_group_norm_class: Homs are seminorms such that f x = 0 → x = 0 for all x.
• group_norm_class: Homs are seminorms such that f x = 0 → x = 1 for all x.

Ring norms

• ring_seminorm_class: Homs are submultiplicative group norms.
• ring_norm_class: Homs are ring seminorms that are also additive group norms.
• mul_ring_seminorm_class: Homs are ring seminorms that are multiplicative.
• mul_ring_norm_class: 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.

Diamond inheritance cannot depend on out_params in the following circumstances:

• there are three classes top, middle, bottom
• all of these classes have a parameter (α : out_param _)
• all of these classes have an instance parameter [root α] that depends on this out_param
• the root class has two child classes: left and right, these are siblings in the hierarchy
• the instance bottom.to_middle takes a [left α] parameter
• the instance middle.to_top takes a [right α] parameter
• there is a leaf class that inherits from both left and right. In that case, given instances bottom α and leaf α, Lean cannot synthesize a top α instance, even though the hypotheses of the instances bottom.to_middle and middle.to_top are satisfied.

There are two workarounds:

• You could replace the bundled inheritance implemented by the instance middle.to_top with unbundled inheritance implemented by adding a [top α] parameter to the middle class. This is the preferred option since it is also more compatible with Lean 4, at the cost of being more work to implement and more verbose to use.
• You could weaken the bottom.to_middle instance by making it depend on a subclass of middle.to_top's parameter, in this example replacing [left α] with [leaf α].

### Basics #

@[class]
structure nonneg_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_zero β] [has_le β] :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_nonneg : (f : F) (a : α), 0 f a

nonneg_hom_class F α β states that F is a type of nonnegative morphisms.

Instances of this typeclass
Instances of other typeclasses for nonneg_hom_class
• nonneg_hom_class.has_sizeof_inst
@[instance]
def nonneg_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_zero β] [has_le β] [self : β] :
α (λ (_x : α), β)
@[instance]
def subadditive_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_add α] [has_add β] [has_le β] [self : β] :
α (λ (_x : α), β)
@[class]
structure subadditive_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_add α] [has_add β] [has_le β] :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_add_le_add : (f : F) (a b : α), f (a + b) f a + f b

subadditive_hom_class F α β states that F is a type of subadditive morphisms.

Instances of this typeclass
Instances of other typeclasses for subadditive_hom_class
@[instance]
def submultiplicative_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_mul α] [has_mul β] [has_le β] [self : β] :
α (λ (_x : α), β)
@[class]
structure submultiplicative_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_mul α] [has_mul β] [has_le β] :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_mul_le_mul : (f : F) (a b : α), f (a * b) f a * f b

submultiplicative_hom_class F α β states that F is a type of submultiplicative morphisms.

Instances of this typeclass
Instances of other typeclasses for submultiplicative_hom_class
• submultiplicative_hom_class.has_sizeof_inst
@[class]
structure mul_le_add_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_mul α] [has_add β] [has_le β] :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_mul_le_add : (f : F) (a b : α), f (a * b) f a + f b

mul_le_add_hom_class F α β states that F is a type of subadditive morphisms.

Instances of this typeclass
Instances of other typeclasses for mul_le_add_hom_class
@[instance]
def mul_le_add_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_mul α] [has_add β] [has_le β] [self : β] :
α (λ (_x : α), β)
@[class]
structure nonarchimedean_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_add α] [linear_order β] :
Type (max u_7 u_8 u_9)

nonarchimedean_hom_class F α β states that F is a type of non-archimedean morphisms.

Instances of this typeclass
Instances of other typeclasses for nonarchimedean_hom_class
• nonarchimedean_hom_class.has_sizeof_inst
@[instance]
def nonarchimedean_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_add α] [linear_order β] [self : β] :
α (λ (_x : α), β)
theorem le_map_add_map_sub {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [has_le β] [ β] (f : F) (a b : α) :
f a f b + f (a - b)
theorem le_map_mul_map_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [has_le β] [ β] (f : F) (a b : α) :
f a f b * f (a / b)
theorem le_map_add_map_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [has_le β] [ β] (f : F) (a b : α) :
f a f b + f (a / b)
theorem le_map_div_mul_map_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [has_le β] [ β] (f : F) (a b c : α) :
f (a / c) f (a / b) * f (b / c)
theorem le_map_sub_add_map_sub {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [has_le β] [ β] (f : F) (a b c : α) :
f (a - c) f (a - b) + f (b - c)
theorem le_map_div_add_map_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [has_le β] [ β] (f : F) (a b c : α) :
f (a / c) f (a / b) + f (b / c)

### Group (semi)norms #

@[class]
structure add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [add_group α]  :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_add_le_add : (f : F) (a b : α), f (a + b) f a + f b
• map_zero : (f : F), f 0 = 0
• map_neg_eq_map : (f : F) (a : α), f (-a) = f a

add_group_seminorm_class F α states that F is a type of β-valued seminorms on the additive group α.

You should extend this class when you extend add_group_seminorm.

Instances of this typeclass
Instances of other typeclasses for add_group_seminorm_class
@[instance]
def add_group_seminorm_class.to_subadditive_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [add_group α] [self : β] :
@[instance]
def group_seminorm_class.to_mul_le_add_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [group α] [self : β] :
β
@[class]
structure group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [group α]  :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_mul_le_add : (f : F) (a b : α), f (a * b) f a + f b
• map_one_eq_zero : (f : F), f 1 = 0
• map_inv_eq_map : (f : F) (a : α), f a⁻¹ = f a

group_seminorm_class F α states that F is a type of β-valued seminorms on the group α.

You should extend this class when you extend group_seminorm.

Instances of this typeclass
Instances of other typeclasses for group_seminorm_class
• group_seminorm_class.has_sizeof_inst
@[instance]
def add_group_norm_class.to_add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [add_group α] [self : β] :
@[class]
structure add_group_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [add_group α]  :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_add_le_add : (f : F) (a b : α), f (a + b) f a + f b
• map_zero : (f : F), f 0 = 0
• map_neg_eq_map : (f : F) (a : α), f (-a) = f a
• eq_zero_of_map_eq_zero : (f : F) {a : α}, f a = 0 a = 0

add_group_norm_class F α states that F is a type of β-valued norms on the additive group α.

You should extend this class when you extend add_group_norm.

Instances of this typeclass
Instances of other typeclasses for add_group_norm_class
@[class]
structure group_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [group α]  :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_mul_le_add : (f : F) (a b : α), f (a * b) f a + f b
• map_one_eq_zero : (f : F), f 1 = 0
• map_inv_eq_map : (f : F) (a : α), f a⁻¹ = f a
• eq_one_of_map_eq_zero : (f : F) {a : α}, f a = 0 a = 1

group_norm_class F α states that F is a type of β-valued norms on the group α.

You should extend this class when you extend group_norm.

Instances of this typeclass
Instances of other typeclasses for group_norm_class
• group_norm_class.has_sizeof_inst
@[instance]
def group_norm_class.to_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [group α] [self : β] :
β
@[instance]
def add_group_seminorm_class.to_add_le_add_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [add_group α] [self : β] :
@[protected, instance]
def add_group_seminorm_class.to_zero_hom_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ β] :
β
Equations
theorem map_div_le_add {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ β] (f : F) (x y : α) :
f (x / y) f x + f y
theorem map_sub_le_add {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ β] (f : F) (x y : α) :
f (x - y) f x + f y
theorem map_sub_rev {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ β] (f : F) (x y : α) :
f (x - y) = f (y - x)
theorem map_div_rev {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ β] (f : F) (x y : α) :
f (x / y) = f (y / x)
theorem le_map_add_map_sub' {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ β] (f : F) (x y : α) :
f x f y + f (y - x)
theorem le_map_add_map_div' {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ β] (f : F) (x y : α) :
f x f y + f (y / x)
theorem abs_sub_map_le_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ β] (f : F) (x y : α) :
|f x - f y| f (x / y)
theorem abs_sub_map_le_sub {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ β] (f : F) (x y : α) :
|f x - f y| f (x - y)
@[protected, instance]
def add_group_seminorm_class.to_nonneg_hom_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ β] :
β
Equations
@[protected, instance]
def group_seminorm_class.to_nonneg_hom_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ β] :
β
Equations
@[simp]
theorem map_eq_zero_iff_eq_one {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ β] (f : F) {x : α} :
f x = 0 x = 1
@[simp]
theorem map_eq_zero_iff_eq_zero {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ β] (f : F) {x : α} :
f x = 0 x = 0
theorem map_ne_zero_iff_ne_one {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ β] (f : F) {x : α} :
f x 0 x 1
theorem map_ne_zero_iff_ne_zero {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ β] (f : F) {x : α} :
f x 0 x 0
theorem map_pos_of_ne_zero {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ β] (f : F) {x : α} (hx : x 0) :
0 < f x
theorem map_pos_of_ne_one {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ β] (f : F) {x : α} (hx : x 1) :
0 < f x

### Ring (semi)norms #

@[instance]
def ring_seminorm_class.to_submultiplicative_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [self : β] :
@[class]
structure ring_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9))  :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_add_le_add : (f : F) (a b : α), f (a + b) f a + f b
• map_zero : (f : F), f 0 = 0
• map_neg_eq_map : (f : F) (a : α), f (-a) = f a
• map_mul_le_mul : (f : F) (a b : α), f (a * b) f a * f b

ring_seminorm_class F α states that F is a type of β-valued seminorms on the ring α.

You should extend this class when you extend ring_seminorm.

Instances of this typeclass
Instances of other typeclasses for ring_seminorm_class
• ring_seminorm_class.has_sizeof_inst
@[instance]
def ring_seminorm_class.to_add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [self : β] :
@[instance]
def ring_norm_class.to_add_group_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [self : β] :
β
@[instance]
def ring_norm_class.to_ring_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [self : β] :
β
@[class]
structure ring_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9))  :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_add_le_add : (f : F) (a b : α), f (a + b) f a + f b
• map_zero : (f : F), f 0 = 0
• map_neg_eq_map : (f : F) (a : α), f (-a) = f a
• map_mul_le_mul : (f : F) (a b : α), f (a * b) f a * f b
• eq_zero_of_map_eq_zero : (f : F) {a : α}, f a = 0 a = 0

ring_norm_class F α states that F is a type of β-valued norms on the ring α.

You should extend this class when you extend ring_norm.

Instances of this typeclass
Instances of other typeclasses for ring_norm_class
• ring_norm_class.has_sizeof_inst
@[instance]
def mul_ring_seminorm_class.to_add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [self : β] :
@[class]
structure mul_ring_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9))  :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_add_le_add : (f : F) (a b : α), f (a + b) f a + f b
• map_zero : (f : F), f 0 = 0
• map_neg_eq_map : (f : F) (a : α), f (-a) = f a
• map_mul : (f : F) (x y : α), f (x * y) = f x * f y
• map_one : (f : F), f 1 = 1

mul_ring_seminorm_class F α states that F is a type of β-valued multiplicative seminorms on the ring α.

You should extend this class when you extend mul_ring_seminorm.

Instances of this typeclass
Instances of other typeclasses for mul_ring_seminorm_class
• mul_ring_seminorm_class.has_sizeof_inst
@[instance]
def mul_ring_seminorm_class.to_monoid_with_zero_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [self : β] :
@[instance]
def mul_ring_norm_class.to_mul_ring_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [self : β] :
@[instance]
def mul_ring_norm_class.to_add_group_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [self : β] :
β
@[class]
structure mul_ring_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9))  :
Type (max u_7 u_8 u_9)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_add_le_add : (f : F) (a b : α), f (a + b) f a + f b
• map_zero : (f : F), f 0 = 0
• map_neg_eq_map : (f : F) (a : α), f (-a) = f a
• map_mul : (f : F) (x y : α), f (x * y) = f x * f y
• map_one : (f : F), f 1 = 1
• eq_zero_of_map_eq_zero : (f : F) {a : α}, f a = 0 a = 0

mul_ring_norm_class F α states that F is a type of β-valued multiplicative norms on the ring α.

You should extend this class when you extend mul_ring_norm.

Instances of this typeclass
Instances of other typeclasses for mul_ring_norm_class
• mul_ring_norm_class.has_sizeof_inst
@[protected, instance]
def ring_seminorm_class.to_nonneg_hom_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [ β] :
β
Equations
@[protected, instance]
def mul_ring_seminorm_class.to_ring_seminorm_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [ β] :
β
Equations
@[protected, instance]
def mul_ring_norm_class.to_ring_norm_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [ β] :
β
Equations