mathlib documentation

algebra.order.hom.basic

Algebraic order homomorphism classes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. https://github.com/leanprover-community/mathlib4/pull/627 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 #

TODO #

Finitary versions of the current lemmas.

@[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)

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 : nonneg_hom_class F α β] :
fun_like F α (λ (_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 : subadditive_hom_class F α β] :
fun_like F α (λ (_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)

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
  • subadditive_hom_class.has_sizeof_inst
@[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 : submultiplicative_hom_class F α β] :
fun_like F α (λ (_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)

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)

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
  • mul_le_add_hom_class.has_sizeof_inst
@[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 : mul_le_add_hom_class F α β] :
fun_like F α (λ (_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 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 : nonarchimedean_hom_class F α β] :
fun_like F α (λ (_x : α), β)
theorem le_map_add_map_sub {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [add_comm_semigroup β] [has_le β] [subadditive_hom_class 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} [group α] [comm_semigroup β] [has_le β] [submultiplicative_hom_class 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} [group α] [add_comm_semigroup β] [has_le β] [mul_le_add_hom_class F α β] (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 α] [comm_semigroup β] [has_le β] [submultiplicative_hom_class 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_2} {α : Type u_3} {β : Type u_4} [add_group α] [add_comm_semigroup β] [has_le β] [subadditive_hom_class 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} [group α] [add_comm_semigroup β] [has_le β] [mul_le_add_hom_class F α β] (f : F) (a b c : α) :
f (a / c) f (a / b) + f (b / c)