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, respect f (a * b) ≤ f a + f b, f a⁻¹ = f a and preserve zero.
• AddGroupNormClass: Homs are seminorms such that f x = 0 → x = 0 for all x.
• GroupNormClass: Homs are seminorms such that f x = 0 → x = 1 for all x.

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

class NonnegHomClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [Zero β] [LE β] [FunLike F α β] : Prop

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

• apply_nonneg : ∀ (f : F) (a : α), 0 ≤ f a

  the image of any element is non negative.

@[simp]

theorem NonnegHomClass.apply_nonneg {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : Zero β} {inst_1 : LE β} {inst_2 : FunLike F α β} [self : NonnegHomClass F α β] (f : F) (a : α), 0 ≤ f a

the image of any element is non negative.

class SubadditiveHomClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [Add α] [Add β] [LE β] [FunLike F α β] : Prop

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

• map_add_le_add : ∀ (f : F) (a b : α), f (a + b) ≤ f a + f b

  the image of a sum is less or equal than the sum of the images.

theorem SubadditiveHomClass.map_add_le_add {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : Add α} {inst_1 : Add β} {inst_2 : LE β} {inst_3 : FunLike F α β} [self : SubadditiveHomClass F α β] (f : F) (a b : α), f (a + b) ≤ f a + f b

the image of a sum is less or equal than the sum of the images.

class SubmultiplicativeHomClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [Mul α] [Mul β] [LE β] [FunLike F α β] : Prop

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

• map_mul_le_mul : ∀ (f : F) (a b : α), f (a * b) ≤ f a * f b

  the image of a product is less or equal than the product of the images.

theorem SubmultiplicativeHomClass.map_mul_le_mul {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : Mul α} {inst_1 : Mul β} {inst_2 : LE β} {inst_3 : FunLike F α β} [self : SubmultiplicativeHomClass F α β] (f : F) (a b : α), f (a * b) ≤ f a * f b

the image of a product is less or equal than the product of the images.

class MulLEAddHomClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [Mul α] [Add β] [LE β] [FunLike F α β] : Prop

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

• map_mul_le_add : ∀ (f : F) (a b : α), f (a * b) ≤ f a + f b

  the image of a product is less or equal than the sum of the images.

theorem MulLEAddHomClass.map_mul_le_add {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : Mul α} {inst_1 : Add β} {inst_2 : LE β} {inst_3 : FunLike F α β} [self : MulLEAddHomClass F α β] (f : F) (a b : α), f (a * b) ≤ f a + f b

the image of a product is less or equal than the sum of the images.

class NonarchimedeanHomClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [Add α] [LinearOrder β] [FunLike F α β] : Prop

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

• map_add_le_max : ∀ (f : F) (a b : α), f (a + b) ≤ max (f a) (f b)

  the image of a sum is less or equal than the maximum of the images.

theorem NonarchimedeanHomClass.map_add_le_max {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : Add α} {inst_1 : LinearOrder β} {inst_2 : FunLike F α β} [self : NonarchimedeanHomClass F α β] (f : F) (a b : α), f (a + b) ≤ max (f a) (f b)

the image of a sum is less or equal than the maximum of the images.

theorem le_map_add_map_sub {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [AddGroup α] [AddCommSemigroup β] [LE β] [SubadditiveHomClass F α β] (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} [FunLike F α β] [Group α] [CommSemigroup β] [LE β] [SubmultiplicativeHomClass F α β] (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} [FunLike F α β] [Group α] [AddCommSemigroup β] [LE β] [MulLEAddHomClass F α β] (f : F) (a : α) (b : α) : f a ≤ f b + f (a / b)

theorem le_map_sub_add_map_sub {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [AddGroup α] [AddCommSemigroup β] [LE β] [SubadditiveHomClass F α β] (f : F) (a : α) (b : α) (c : α) : f (a - c) ≤ f (a - b) + f (b - c)

theorem le_map_div_mul_map_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Group α] [CommSemigroup β] [LE β] [SubmultiplicativeHomClass F α β] (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} [FunLike F α β] [Group α] [AddCommSemigroup β] [LE β] [MulLEAddHomClass F α β] (f : F) (a : α) (b : α) (c : α) : f (a / c) ≤ f (a / b) + f (b / c)

def Mathlib.Meta.Positivity.evalMap : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: nonnegative maps take nonnegative values.

Equations

• One or more equations did not get rendered due to their size.

Group (semi)norms

class AddGroupSeminormClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [AddGroup α] [OrderedAddCommMonoid β] [FunLike F α β] extends SubadditiveHomClass : Prop

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

You should extend this class when you extend AddGroupSeminorm.

• map_add_le_add : ∀ (f : F) (a b : α), f (a + b) ≤ f a + f b
• map_zero : ∀ (f : F), f 0 = 0

  The image of zero is zero.

• map_neg_eq_map : ∀ (f : F) (a : α), f (-a) = f a

  The map is invariant under negation of its argument.

theorem AddGroupSeminormClass.map_zero {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : AddGroup α} {inst_1 : OrderedAddCommMonoid β} {inst_2 : FunLike F α β} [self : AddGroupSeminormClass F α β] (f : F), f 0 = 0

The image of zero is zero.

@[simp]

theorem AddGroupSeminormClass.map_neg_eq_map {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : AddGroup α} {inst_1 : OrderedAddCommMonoid β} {inst_2 : FunLike F α β} [self : AddGroupSeminormClass F α β] (f : F) (a : α), f (-a) = f a

The map is invariant under negation of its argument.

class GroupSeminormClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [Group α] [OrderedAddCommMonoid β] [FunLike F α β] extends MulLEAddHomClass : Prop

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

You should extend this class when you extend GroupSeminorm.

• map_mul_le_add : ∀ (f : F) (a b : α), f (a * b) ≤ f a + f b
• map_one_eq_zero : ∀ (f : F), f 1 = 0

  The image of one is zero.

• map_inv_eq_map : ∀ (f : F) (a : α), f a⁻¹ = f a

  The map is invariant under inversion of its argument.

@[simp]

theorem GroupSeminormClass.map_one_eq_zero {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : Group α} {inst_1 : OrderedAddCommMonoid β} {inst_2 : FunLike F α β} [self : GroupSeminormClass F α β] (f : F), f 1 = 0

The image of one is zero.

@[simp]

theorem GroupSeminormClass.map_inv_eq_map {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : Group α} {inst_1 : OrderedAddCommMonoid β} {inst_2 : FunLike F α β} [self : GroupSeminormClass F α β] (f : F) (a : α), f a⁻¹ = f a

The map is invariant under inversion of its argument.

class AddGroupNormClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [AddGroup α] [OrderedAddCommMonoid β] [FunLike F α β] extends AddGroupSeminormClass : Prop

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

You should extend this class when you extend AddGroupNorm.

• 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

  The argument is zero if its image under the map is zero.

theorem AddGroupNormClass.eq_zero_of_map_eq_zero {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : AddGroup α} {inst_1 : OrderedAddCommMonoid β} {inst_2 : FunLike F α β} [self : AddGroupNormClass F α β] (f : F) {a : α}, f a = 0 → a = 0

The argument is zero if its image under the map is zero.

class GroupNormClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [Group α] [OrderedAddCommMonoid β] [FunLike F α β] extends GroupSeminormClass : Prop

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

You should extend this class when you extend GroupNorm.

• 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

  The argument is one if its image under the map is zero.

theorem GroupNormClass.eq_one_of_map_eq_zero {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : Group α} {inst_1 : OrderedAddCommMonoid β} {inst_2 : FunLike F α β} [self : GroupNormClass F α β] (f : F) {a : α}, f a = 0 → a = 1

The argument is one if its image under the map is zero.

theorem AddGroupSeminormClass.toAddLEAddHomClass {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} : ∀ {inst : AddGroup α} {inst_1 : OrderedAddCommMonoid β} {inst_2 : FunLike F α β} [self : AddGroupSeminormClass F α β], SubadditiveHomClass F α β

@[instance 100]

instance AddGroupSeminormClass.toZeroHomClass {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [AddGroup α] [OrderedAddCommMonoid β] [AddGroupSeminormClass F α β] : ZeroHomClass F α β

Equations

• ⋯ = ⋯

theorem map_sub_le_add {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [AddGroup α] [OrderedAddCommMonoid β] [AddGroupSeminormClass F α β] (f : F) (x : α) (y : α) : f (x - y) ≤ f x + f y

theorem map_div_le_add {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Group α] [OrderedAddCommMonoid β] [GroupSeminormClass F α β] (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} [FunLike F α β] [AddGroup α] [OrderedAddCommMonoid β] [AddGroupSeminormClass F α β] (f : F) (x : α) (y : α) : f (x - y) = f (y - x)

theorem map_div_rev {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Group α] [OrderedAddCommMonoid β] [GroupSeminormClass F α β] (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} [FunLike F α β] [AddGroup α] [OrderedAddCommMonoid β] [AddGroupSeminormClass F α β] (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} [FunLike F α β] [Group α] [OrderedAddCommMonoid β] [GroupSeminormClass F α β] (f : F) (x : α) (y : α) : f x ≤ f y + f (y / x)

theorem abs_sub_map_le_sub {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [AddGroup α] [LinearOrderedAddCommGroup β] [AddGroupSeminormClass F α β] (f : F) (x : α) (y : α) : |f x - f y| ≤ f (x - y)

theorem abs_sub_map_le_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Group α] [LinearOrderedAddCommGroup β] [GroupSeminormClass F α β] (f : F) (x : α) (y : α) : |f x - f y| ≤ f (x / y)

@[instance 100]

instance AddGroupSeminormClass.toNonnegHomClass {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [AddGroup α] [LinearOrderedAddCommMonoid β] [AddGroupSeminormClass F α β] : NonnegHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance GroupSeminormClass.toNonnegHomClass {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Group α] [LinearOrderedAddCommMonoid β] [GroupSeminormClass F α β] : NonnegHomClass F α β

Equations

• ⋯ = ⋯

@[simp]

theorem map_eq_zero_iff_eq_zero {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [AddGroup α] [OrderedAddCommMonoid β] [AddGroupNormClass F α β] (f : F) {x : α} : f x = 0 ↔ x = 0

@[simp]

theorem map_eq_zero_iff_eq_one {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Group α] [OrderedAddCommMonoid β] [GroupNormClass F α β] (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} [FunLike F α β] [AddGroup α] [OrderedAddCommMonoid β] [AddGroupNormClass F α β] (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} [FunLike F α β] [Group α] [OrderedAddCommMonoid β] [GroupNormClass F α β] (f : F) {x : α} : f x ≠ 0 ↔ x ≠ 1

theorem map_pos_of_ne_zero {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [AddGroup α] [LinearOrderedAddCommMonoid β] [AddGroupNormClass F α β] (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} [FunLike F α β] [Group α] [LinearOrderedAddCommMonoid β] [GroupNormClass F α β] (f : F) {x : α} (hx : x ≠ 1) : 0 < f x

Ring (semi)norms

class RingSeminormClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [NonUnitalNonAssocRing α] [OrderedSemiring β] [FunLike F α β] extends AddGroupSeminormClass , SubmultiplicativeHomClass : Prop

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

You should extend this class when you extend RingSeminorm.

class RingNormClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [NonUnitalNonAssocRing α] [OrderedSemiring β] [FunLike F α β] extends RingSeminormClass : Prop

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

You should extend this class when you extend RingNorm.

• 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

  The argument is zero if its image under the map is zero.

class MulRingSeminormClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [NonAssocRing α] [OrderedSemiring β] [FunLike F α β] extends AddGroupSeminormClass , MonoidHomClass : Prop

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

You should extend this class when you extend MulRingSeminorm.

class MulRingNormClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [NonAssocRing α] [OrderedSemiring β] [FunLike F α β] extends MulRingSeminormClass : Prop

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

You should extend this class when you extend MulRingNorm.

• 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

  The argument is zero if its image under the map is zero.

@[instance 100]

instance RingSeminormClass.toNonnegHomClass {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [NonUnitalNonAssocRing α] [LinearOrderedSemiring β] [RingSeminormClass F α β] : NonnegHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance MulRingSeminormClass.toRingSeminormClass {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [NonAssocRing α] [OrderedSemiring β] [MulRingSeminormClass F α β] : RingSeminormClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance MulRingNormClass.toRingNormClass {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [NonAssocRing α] [OrderedSemiring β] [MulRingNormClass F α β] : RingNormClass F α β

Equations

• ⋯ = ⋯