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)

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.

def LibraryNote.«out-param_inheritance» : Batteries.Util.LibraryNote

Diamond inheritance cannot depend on outParams in the following circumstances:

• there are three classes Top, Middle, Bottom
• all of these classes have a parameter (α : outParam _)
• all of these classes have an instance parameter [Root α] that depends on this outParam
• the Root class has two child classes: Left and Right, these are siblings in the hierarchy
• the instance Bottom.toMiddle takes a [Left α] parameter
• the instance Middle.toTop 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.toMiddle and Middle.toTop are satisfied.

There are two workarounds:

• You could replace the bundled inheritance implemented by the instance Middle.toTop 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.toMiddle instance by making it depend on a subclass of Middle.toTop's parameter, in this example replacing [Left α] with [Leaf α].

Equations

• LibraryNote.«out-param_inheritance» = default

Basics

class NonnegHomClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [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 nonnegative.

class SubadditiveHomClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [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.

class SubmultiplicativeHomClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [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.

class MulLEAddHomClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [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.

class NonarchimedeanHomClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [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 map_zero_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero α] [Zero β] [LE β] [ZeroHomClass F α β] [NonnegHomClass F α β] (f : F) (a : α) : f 0 ≤ f a

The value at zero of a zero-preserving nonnegative homomorphism is a minimum.

theorem le_map_mul_map_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [CommMagma β] [LE β] [SubmultiplicativeHomClass F α β] (f : F) (a b : α) : f a ≤ f b * f (a / b)

theorem le_map_add_map_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddGroup α] [AddCommMagma β] [LE β] [SubadditiveHomClass F α β] (f : F) (a b : α) : f a ≤ f b + f (a - b)

theorem le_map_add_map_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [AddCommMagma β] [LE β] [MulLEAddHomClass F α β] (f : F) (a b : α) : f a ≤ f b + f (a / b)

theorem le_map_div_mul_map_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [Mul β] [LE β] [SubmultiplicativeHomClass F α β] (f : F) (a b c : α) : f (a / c) ≤ f (a / b) * f (b / c)

theorem le_map_sub_add_map_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddGroup α] [Add β] [LE β] [SubadditiveHomClass 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_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [Add β] [LE β] [MulLEAddHomClass F α β] (f : F) (a b c : α) : f (a / c) ≤ f (a / b) + f (b / c)