Algebraic order homomorphism classes

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

Typeclasses

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.

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.

Group (semi)norms

class AddGroupSeminormClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [AddGroup α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] extends SubadditiveHomClass F α β : 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.

class GroupSeminormClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [Group α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] extends MulLEAddHomClass F α β : 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.

class AddGroupNormClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [AddGroup α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] extends AddGroupSeminormClass F α β : 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.

class GroupNormClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [Group α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] extends GroupSeminormClass F α β : 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.

@[instance 100]

instance AddGroupSeminormClass.toZeroHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddGroup α] [AddCommMonoid β] [PartialOrder β] [AddGroupSeminormClass F α β] : ZeroHomClass F α β

theorem map_div_le_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [AddCommMonoid β] [PartialOrder β] [GroupSeminormClass F α β] (f : F) (x y : α) : f (x / y) ≤ f x + f y

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

theorem map_div_rev {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [AddCommMonoid β] [PartialOrder β] [GroupSeminormClass F α β] (f : F) (x y : α) : f (x / y) = f (y / x)

theorem map_sub_rev {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddGroup α] [AddCommMonoid β] [PartialOrder β] [AddGroupSeminormClass F α β] (f : F) (x y : α) : f (x - y) = f (y - x)

theorem map_inv_mul {F : Type u_1} {β : Type u_3} [AddCommMonoid β] [PartialOrder β] (f : F) {α : Type u_4} [FunLike F α β] [CommGroup α] [GroupSeminormClass F α β] (x y : α) : f (x⁻¹ * y) = f (x * y⁻¹)

theorem map_neg_add {F : Type u_1} {β : Type u_3} [AddCommMonoid β] [PartialOrder β] (f : F) {α : Type u_4} [FunLike F α β] [AddCommGroup α] [AddGroupSeminormClass F α β] (x y : α) : f (-x + y) = f (x + -y)

theorem le_map_add_map_div' {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [AddCommMonoid β] [PartialOrder β] [GroupSeminormClass F α β] (f : F) (x y : α) : f x ≤ f y + f (y / x)

theorem le_map_add_map_sub' {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddGroup α] [AddCommMonoid β] [PartialOrder β] [AddGroupSeminormClass F α β] (f : F) (x y : α) : f x ≤ f y + f (y - x)

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

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

@[instance 100]

instance GroupSeminormClass.toNonnegHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [GroupSeminormClass F α β] : NonnegHomClass F α β

@[instance 100]

instance AddGroupSeminormClass.toNonnegHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddGroup α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [AddGroupSeminormClass F α β] : NonnegHomClass F α β

theorem map_eq_zero_iff_eq_one {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [AddCommMonoid β] [PartialOrder β] [GroupNormClass F α β] (f : F) {x : α} : f x = 0 ↔ x = 1

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

theorem map_ne_zero_iff_ne_one {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [AddCommMonoid β] [PartialOrder β] [GroupNormClass F α β] (f : F) {x : α} : f x ≠ 0 ↔ x ≠ 1

theorem map_ne_zero_iff_ne_zero {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddGroup α] [AddCommMonoid β] [PartialOrder β] [AddGroupNormClass F α β] (f : F) {x : α} : f x ≠ 0 ↔ x ≠ 0

theorem map_pos_of_ne_one {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [GroupNormClass F α β] (f : F) {x : α} (hx : x ≠ 1) : 0 < f x

theorem map_pos_of_ne_zero {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddGroup α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [AddGroupNormClass F α β] (f : F) {x : α} (hx : x ≠ 0) : 0 < f x