Algebraic order homomorphism classes

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

Typeclasses

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.

Ring (semi)norms

class RingSeminormClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [NonUnitalNonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] extends AddGroupSeminormClass F α β, SubmultiplicativeHomClass F α β : Prop

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

You should extend this class when you extend RingSeminorm.

• 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

class RingNormClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [NonUnitalNonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] extends RingSeminormClass F α β, AddGroupNormClass F α β : 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

class MulRingSeminormClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] extends AddGroupSeminormClass F α β, MonoidWithZeroHomClass F α β : 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.

• 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

class MulRingNormClass (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] extends MulRingSeminormClass F α β, AddGroupNormClass F α β : 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

@[instance 100]

instance RingSeminormClass.toNonnegHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonUnitalNonAssocRing α] [Semiring β] [LinearOrder β] [IsOrderedAddMonoid β] [RingSeminormClass F α β] : NonnegHomClass F α β

@[instance 100]

instance MulRingSeminormClass.toRingSeminormClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonAssocRing α] [Semiring β] [PartialOrder β] [MulRingSeminormClass F α β] : RingSeminormClass F α β

@[instance 100]

instance MulRingNormClass.toRingNormClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonAssocRing α] [Semiring β] [PartialOrder β] [MulRingNormClass F α β] : RingNormClass F α β