mathlib3 documentation

algebra.order.hom.monoid

Ordered monoid and group homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines morphisms between (additive) ordered monoids.

Types of morphisms #

Typeclasses #

Notation #

Implementation notes #

There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

There is no order_group_hom -- the idea is that order_monoid_hom is used. The constructor for order_monoid_hom needs a proof of map_one as well as map_mul; a separate constructor order_monoid_hom.mk' will construct ordered group homs (i.e. ordered monoid homs between ordered groups) given only a proof that multiplication is preserved,

Implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type order_monoid_hom. When they can be inferred from the type it is faster to use this method than to use type class inference.

Tags #

ordered monoid, ordered group, monoid with zero

structure order_add_monoid_hom (α : Type u_6) (β : Type u_7) [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] :
Type (max u_6 u_7)

α →+o β is the type of monotone functions α → β that preserve the ordered_add_comm_monoid structure.

order_add_monoid_hom is also used for ordered group homomorphisms.

When possible, instead of parametrizing results over (f : α →+o β), you should parametrize over (F : Type*) [order_add_monoid_hom_class F α β] (f : F).

When you extend this structure, make sure to extend order_add_monoid_hom_class.

Instances for order_add_monoid_hom
@[class]
structure order_add_monoid_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] :
Type (max u_6 u_7 u_8)

order_add_monoid_hom_class F α β states that F is a type of ordered monoid homomorphisms.

You should also extend this typeclass when you extend order_add_monoid_hom.

Instances of this typeclass
Instances of other typeclasses for order_add_monoid_hom_class
  • order_add_monoid_hom_class.has_sizeof_inst
structure order_monoid_hom (α : Type u_6) (β : Type u_7) [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] :
Type (max u_6 u_7)

α →*o β is the type of functions α → β that preserve the ordered_comm_monoid structure.

order_monoid_hom is also used for ordered group homomorphisms.

When possible, instead of parametrizing results over (f : α →*o β), you should parametrize over (F : Type*) [order_monoid_hom_class F α β] (f : F).

When you extend this structure, make sure to extend order_monoid_hom_class.

Instances for order_monoid_hom
@[instance]
@[class]
structure order_monoid_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] :
Type (max u_6 u_7 u_8)

order_monoid_hom_class F α β states that F is a type of ordered monoid homomorphisms.

You should also extend this typeclass when you extend order_monoid_hom.

Instances of this typeclass
Instances of other typeclasses for order_monoid_hom_class
  • order_monoid_hom_class.has_sizeof_inst
@[protected, instance]
def order_monoid_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] [order_monoid_hom_class F α β] :
has_coe_t F →*o β)
Equations
@[protected, instance]
def order_add_monoid_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] [order_add_monoid_hom_class F α β] :
has_coe_t F →+o β)
Equations
structure order_monoid_with_zero_hom (α : Type u_6) (β : Type u_7) [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] :
Type (max u_6 u_7)

order_monoid_with_zero_hom α β is the type of functions α → β that preserve the monoid_with_zero structure.

order_monoid_with_zero_hom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : α →+ β), you should parametrize over (F : Type*) [order_monoid_with_zero_hom_class F α β] (f : F).

When you extend this structure, make sure to extend order_monoid_with_zero_hom_class.

Instances for order_monoid_with_zero_hom
@[class]
structure order_monoid_with_zero_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] :
Type (max u_6 u_7 u_8)

order_monoid_with_zero_hom_class F α β states that F is a type of ordered monoid with zero homomorphisms.

You should also extend this typeclass when you extend order_monoid_with_zero_hom.

Instances of this typeclass
Instances of other typeclasses for order_monoid_with_zero_hom_class
  • order_monoid_with_zero_hom_class.has_sizeof_inst
@[protected, instance]
Equations
theorem map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [order_add_monoid_hom_class F α β] (f : F) {a : α} (ha : 0 a) :
0 f a
theorem map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [order_add_monoid_hom_class F α β] (f : F) {a : α} (ha : a 0) :
f a 0
theorem monotone_iff_map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_add_comm_group α] [ordered_add_comm_monoid β] [add_monoid_hom_class F α β] (f : F) :
monotone f (a : α), 0 a 0 f a
theorem antitone_iff_map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_add_comm_group α] [ordered_add_comm_monoid β] [add_monoid_hom_class F α β] (f : F) :
antitone f (a : α), 0 a f a 0
theorem monotone_iff_map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_add_comm_group α] [ordered_add_comm_monoid β] [add_monoid_hom_class F α β] (f : F) :
monotone f (a : α), a 0 f a 0
theorem antitone_iff_map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_add_comm_group α] [ordered_add_comm_monoid β] [add_monoid_hom_class F α β] (f : F) :
antitone f (a : α), a 0 0 f a
theorem strict_mono_iff_map_pos {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_add_comm_group α] [ordered_add_comm_monoid β] [add_monoid_hom_class F α β] (f : F) [covariant_class β β has_add.add has_lt.lt] :
strict_mono f (a : α), 0 < a 0 < f a
theorem strict_anti_iff_map_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_add_comm_group α] [ordered_add_comm_monoid β] [add_monoid_hom_class F α β] (f : F) [covariant_class β β has_add.add has_lt.lt] :
strict_anti f (a : α), 0 < a f a < 0
theorem strict_mono_iff_map_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_add_comm_group α] [ordered_add_comm_monoid β] [add_monoid_hom_class F α β] (f : F) [covariant_class β β has_add.add has_lt.lt] :
strict_mono f (a : α), a < 0 f a < 0
theorem strict_anti_iff_map_pos {F : Type u_1} {α : Type u_2} {β : Type u_3} [ordered_add_comm_group α] [ordered_add_comm_monoid β] [add_monoid_hom_class F α β] (f : F) [covariant_class β β has_add.add has_lt.lt] :
strict_anti f (a : α), a < 0 0 < f a
@[protected, instance]
Equations
@[protected, instance]
def order_add_monoid_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] :
has_coe_to_fun →+o β) (λ (_x : α →+o β), α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[protected, instance]
def order_monoid_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] :
has_coe_to_fun →*o β) (λ (_x : α →*o β), α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[ext]
theorem order_add_monoid_hom.ext {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] {f g : α →+o β} (h : (a : α), f a = g a) :
f = g
@[ext]
theorem order_monoid_hom.ext {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] {f g : α →*o β} (h : (a : α), f a = g a) :
f = g
theorem order_monoid_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) :
@[simp]
theorem order_add_monoid_hom.coe_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+ β) (h : monotone f.to_fun) :
@[simp]
theorem order_monoid_hom.coe_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →* β) (h : monotone f.to_fun) :
@[simp]
theorem order_monoid_hom.mk_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) (h : monotone f.to_fun) :
@[simp]
theorem order_add_monoid_hom.mk_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) (h : monotone f.to_fun) :
def order_add_monoid_hom.to_order_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) :
α →o β

Reinterpret an ordered additive monoid homomorphism as an order homomorphism.

Equations
def order_monoid_hom.to_order_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) :
α →o β

Reinterpret an ordered monoid homomorphism as an order homomorphism.

Equations
@[simp]
theorem order_monoid_hom.coe_monoid_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) :
@[simp]
theorem order_add_monoid_hom.coe_add_monoid_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) :
@[simp]
theorem order_monoid_hom.coe_order_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) :
@[simp]
theorem order_add_monoid_hom.coe_order_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) :
@[protected]
def order_add_monoid_hom.copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) (f' : α β) (h : f' = f) :
α →+o β

Copy of an order_monoid_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
def order_monoid_hom.copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) (f' : α β) (h : f' = f) :
α →*o β

Copy of an order_monoid_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem order_add_monoid_hom.coe_copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
@[simp]
theorem order_monoid_hom.coe_copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem order_monoid_hom.copy_eq {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) (f' : α β) (h : f' = f) :
f.copy f' h = f
theorem order_add_monoid_hom.copy_eq {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]
def order_add_monoid_hom.id (α : Type u_2) [preorder α] [add_zero_class α] :
α →+o α

The identity map as an ordered additive monoid homomorphism.

Equations
@[protected]
def order_monoid_hom.id (α : Type u_2) [preorder α] [mul_one_class α] :
α →*o α

The identity map as an ordered monoid homomorphism.

Equations
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
def order_add_monoid_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [add_zero_class α] [add_zero_class β] [add_zero_class γ] (f : β →+o γ) (g : α →+o β) :
α →+o γ

Composition of order_add_monoid_homs as an order_add_monoid_hom

Equations
def order_monoid_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_one_class α] [mul_one_class β] [mul_one_class γ] (f : β →*o γ) (g : α →*o β) :
α →*o γ

Composition of order_monoid_homs as an order_monoid_hom.

Equations
@[simp]
theorem order_monoid_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_one_class α] [mul_one_class β] [mul_one_class γ] (f : β →*o γ) (g : α →*o β) :
(f.comp g) = f g
@[simp]
theorem order_add_monoid_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [add_zero_class α] [add_zero_class β] [add_zero_class γ] (f : β →+o γ) (g : α →+o β) :
(f.comp g) = f g
@[simp]
theorem order_monoid_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_one_class α] [mul_one_class β] [mul_one_class γ] (f : β →*o γ) (g : α →*o β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem order_add_monoid_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [add_zero_class α] [add_zero_class β] [add_zero_class γ] (f : β →+o γ) (g : α →+o β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem order_monoid_hom.coe_comp_monoid_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_one_class α] [mul_one_class β] [mul_one_class γ] (f : β →*o γ) (g : α →*o β) :
(f.comp g) = f.comp g
@[simp]
theorem order_add_monoid_hom.coe_comp_add_monoid_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [add_zero_class α] [add_zero_class β] [add_zero_class γ] (f : β →+o γ) (g : α →+o β) :
(f.comp g) = f.comp g
@[simp]
theorem order_monoid_hom.coe_comp_order_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_one_class α] [mul_one_class β] [mul_one_class γ] (f : β →*o γ) (g : α →*o β) :
(f.comp g) = f.comp g
@[simp]
theorem order_add_monoid_hom.coe_comp_order_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [add_zero_class α] [add_zero_class β] [add_zero_class γ] (f : β →+o γ) (g : α →+o β) :
(f.comp g) = f.comp g
@[simp]
theorem order_monoid_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [preorder α] [preorder β] [preorder γ] [preorder δ] [mul_one_class α] [mul_one_class β] [mul_one_class γ] [mul_one_class δ] (f : γ →*o δ) (g : β →*o γ) (h : α →*o β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem order_add_monoid_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [preorder α] [preorder β] [preorder γ] [preorder δ] [add_zero_class α] [add_zero_class β] [add_zero_class γ] [add_zero_class δ] (f : γ →+o δ) (g : β →+o γ) (h : α →+o β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem order_add_monoid_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) :
@[simp]
theorem order_monoid_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) :
@[simp]
theorem order_monoid_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) :
@[simp]
theorem order_add_monoid_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) :
theorem order_monoid_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_one_class α] [mul_one_class β] [mul_one_class γ] {g₁ g₂ : β →*o γ} {f : α →*o β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem order_add_monoid_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [add_zero_class α] [add_zero_class β] [add_zero_class γ] {g₁ g₂ : β →+o γ} {f : α →+o β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem order_add_monoid_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [add_zero_class α] [add_zero_class β] [add_zero_class γ] {g : β →+o γ} {f₁ f₂ : α →+o β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem order_monoid_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_one_class α] [mul_one_class β] [mul_one_class γ] {g : β →*o γ} {f₁ f₂ : α →*o β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected, instance]
def order_monoid_hom.has_one {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] :
has_one →*o β)

1 is the homomorphism sending all elements to 1.

Equations
@[protected, instance]
def order_add_monoid_hom.has_zero {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] :
has_zero →+o β)

1 is the homomorphism sending all elements to 1.

Equations
@[simp]
theorem order_add_monoid_hom.coe_zero {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] :
0 = 0
@[simp]
theorem order_monoid_hom.coe_one {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] :
1 = 1
@[simp]
theorem order_add_monoid_hom.zero_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (a : α) :
0 a = 0
@[simp]
theorem order_monoid_hom.one_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (a : α) :
1 a = 1
@[simp]
theorem order_add_monoid_hom.zero_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [add_zero_class α] [add_zero_class β] [add_zero_class γ] (f : α →+o β) :
0.comp f = 0
@[simp]
theorem order_monoid_hom.one_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_one_class α] [mul_one_class β] [mul_one_class γ] (f : α →*o β) :
1.comp f = 1
@[simp]
theorem order_add_monoid_hom.comp_zero {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [add_zero_class α] [add_zero_class β] [add_zero_class γ] (f : β →+o γ) :
f.comp 0 = 0
@[simp]
theorem order_monoid_hom.comp_one {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_one_class α] [mul_one_class β] [mul_one_class γ] (f : β →*o γ) :
f.comp 1 = 1
@[protected, instance]

For two ordered additive monoid morphisms f and g, their product is the ordered additive monoid morphism sending a to f a + g a.

Equations
@[protected, instance]
def order_monoid_hom.has_mul {α : Type u_2} {β : Type u_3} [ordered_comm_monoid α] [ordered_comm_monoid β] :
has_mul →*o β)

For two ordered monoid morphisms f and g, their product is the ordered monoid morphism sending a to f a * g a.

Equations
@[simp]
theorem order_monoid_hom.coe_mul {α : Type u_2} {β : Type u_3} [ordered_comm_monoid α] [ordered_comm_monoid β] (f g : α →*o β) :
(f * g) = f * g
@[simp]
theorem order_add_monoid_hom.coe_add {α : Type u_2} {β : Type u_3} [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] (f g : α →+o β) :
(f + g) = f + g
@[simp]
theorem order_monoid_hom.mul_apply {α : Type u_2} {β : Type u_3} [ordered_comm_monoid α] [ordered_comm_monoid β] (f g : α →*o β) (a : α) :
(f * g) a = f a * g a
@[simp]
theorem order_add_monoid_hom.add_apply {α : Type u_2} {β : Type u_3} [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] (f g : α →+o β) (a : α) :
(f + g) a = f a + g a
theorem order_monoid_hom.mul_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ordered_comm_monoid α] [ordered_comm_monoid β] [ordered_comm_monoid γ] (g₁ g₂ : β →*o γ) (f : α →*o β) :
(g₁ * g₂).comp f = g₁.comp f * g₂.comp f
theorem order_add_monoid_hom.add_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [ordered_add_comm_monoid γ] (g₁ g₂ : β →+o γ) (f : α →+o β) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
theorem order_add_monoid_hom.comp_add {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [ordered_add_comm_monoid γ] (g : β →+o γ) (f₁ f₂ : α →+o β) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
theorem order_monoid_hom.comp_mul {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ordered_comm_monoid α] [ordered_comm_monoid β] [ordered_comm_monoid γ] (g : β →*o γ) (f₁ f₂ : α →*o β) :
g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
@[simp]
theorem order_monoid_hom.to_monoid_hom_eq_coe {α : Type u_2} {β : Type u_3} {hα : ordered_comm_monoid α} {hβ : ordered_comm_monoid β} (f : α →*o β) :
@[simp]
@[simp]
theorem order_add_monoid_hom.to_order_hom_eq_coe {α : Type u_2} {β : Type u_3} {hα : ordered_add_comm_monoid α} {hβ : ordered_add_comm_monoid β} (f : α →+o β) :
@[simp]
theorem order_monoid_hom.to_order_hom_eq_coe {α : Type u_2} {β : Type u_3} {hα : ordered_comm_monoid α} {hβ : ordered_comm_monoid β} (f : α →*o β) :
@[simp]
theorem order_add_monoid_hom.mk'_to_add_monoid_hom {α : Type u_2} {β : Type u_3} {hα : ordered_add_comm_group α} {hβ : ordered_add_comm_group β} (f : α β) (hf : monotone f) (map_mul : (a b : α), f (a + b) = f a + f b) :
@[simp]
theorem order_monoid_hom.mk'_to_monoid_hom {α : Type u_2} {β : Type u_3} {hα : ordered_comm_group α} {hβ : ordered_comm_group β} (f : α β) (hf : monotone f) (map_mul : (a b : α), f (a * b) = f a * f b) :
def order_add_monoid_hom.mk' {α : Type u_2} {β : Type u_3} {hα : ordered_add_comm_group α} {hβ : ordered_add_comm_group β} (f : α β) (hf : monotone f) (map_mul : (a b : α), f (a + b) = f a + f b) :
α →+o β

Makes an ordered additive group homomorphism from a proof that the map preserves addition.

Equations
def order_monoid_hom.mk' {α : Type u_2} {β : Type u_3} {hα : ordered_comm_group α} {hβ : ordered_comm_group β} (f : α β) (hf : monotone f) (map_mul : (a b : α), f (a * b) = f a * f b) :
α →*o β

Makes an ordered group homomorphism from a proof that the map preserves multiplication.

Equations
@[protected, instance]
def order_monoid_with_zero_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] :
has_coe_to_fun →*₀o β) (λ (_x : α →*₀o β), α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[ext]
theorem order_monoid_with_zero_hom.ext {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] {f g : α →*₀o β} (h : (a : α), f a = g a) :
f = g
@[simp]
@[simp]

Reinterpret an ordered monoid with zero homomorphism as an order monoid homomorphism.

Equations
@[simp]
@[protected]
def order_monoid_with_zero_hom.copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] (f : α →*₀o β) (f' : α β) (h : f' = f) :
α →*o β

Copy of an order_monoid_with_zero_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem order_monoid_with_zero_hom.coe_copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] (f : α →*₀o β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem order_monoid_with_zero_hom.copy_eq {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] (f : α →*₀o β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]

The identity map as an ordered monoid with zero homomorphism.

Equations
@[simp]
theorem order_monoid_with_zero_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_zero_one_class α] [mul_zero_one_class β] [mul_zero_one_class γ] (f : β →*₀o γ) (g : α →*₀o β) :
(f.comp g) = f g
@[simp]
theorem order_monoid_with_zero_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_zero_one_class α] [mul_zero_one_class β] [mul_zero_one_class γ] (f : β →*₀o γ) (g : α →*₀o β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem order_monoid_with_zero_hom.coe_comp_monoid_with_zero_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_zero_one_class α] [mul_zero_one_class β] [mul_zero_one_class γ] (f : β →*₀o γ) (g : α →*₀o β) :
(f.comp g) = f.comp g
@[simp]
theorem order_monoid_with_zero_hom.coe_comp_order_monoid_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_zero_one_class α] [mul_zero_one_class β] [mul_zero_one_class γ] (f : β →*₀o γ) (g : α →*₀o β) :
(f.comp g) = f.comp g
@[simp]
theorem order_monoid_with_zero_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [preorder α] [preorder β] [preorder γ] [preorder δ] [mul_zero_one_class α] [mul_zero_one_class β] [mul_zero_one_class γ] [mul_zero_one_class δ] (f : γ →*₀o δ) (g : β →*₀o γ) (h : α →*₀o β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
@[simp]
theorem order_monoid_with_zero_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_zero_one_class α] [mul_zero_one_class β] [mul_zero_one_class γ] {g₁ g₂ : β →*₀o γ} {f : α →*₀o β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem order_monoid_with_zero_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [mul_zero_one_class α] [mul_zero_one_class β] [mul_zero_one_class γ] {g : β →*₀o γ} {f₁ f₂ : α →*₀o β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected, instance]

For two ordered monoid morphisms f and g, their product is the ordered monoid morphism sending a to f a * g a.

Equations
@[simp]
theorem order_monoid_with_zero_hom.mul_apply {α : Type u_2} {β : Type u_3} [linear_ordered_comm_monoid_with_zero α] [linear_ordered_comm_monoid_with_zero β] (f g : α →*₀o β) (a : α) :
(f * g) a = f a * g a
theorem order_monoid_with_zero_hom.mul_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [linear_ordered_comm_monoid_with_zero α] [linear_ordered_comm_monoid_with_zero β] [linear_ordered_comm_monoid_with_zero γ] (g₁ g₂ : β →*₀o γ) (f : α →*₀o β) :
(g₁ * g₂).comp f = g₁.comp f * g₂.comp f
theorem order_monoid_with_zero_hom.comp_mul {α : Type u_2} {β : Type u_3} {γ : Type u_4} [linear_ordered_comm_monoid_with_zero α] [linear_ordered_comm_monoid_with_zero β] [linear_ordered_comm_monoid_with_zero γ] (g : β →*₀o γ) (f₁ f₂ : α →*₀o β) :
g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
@[simp]
theorem order_monoid_with_zero_hom.to_monoid_with_zero_hom_eq_coe {α : Type u_2} {β : Type u_3} {hα : preorder α} {hα' : mul_zero_one_class α} {hβ : preorder β} {hβ' : mul_zero_one_class β} (f : α →*₀o β) :
@[simp]
theorem order_monoid_with_zero_hom.to_order_monoid_hom_eq_coe {α : Type u_2} {β : Type u_3} {hα : preorder α} {hα' : mul_zero_one_class α} {hβ : preorder β} {hβ' : mul_zero_one_class β} (f : α →*₀o β) :