# mathlib3documentation

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 #

• `order_add_monoid_hom`: Ordered additive monoid homomorphisms.
• `order_monoid_hom`: Ordered monoid homomorphisms.
• `order_monoid_with_zero_hom`: Ordered monoid with zero homomorphisms.

## Typeclasses #

• `order_add_monoid_hom_class`
• `order_monoid_hom_class`
• `order_monoid_with_zero_hom_class`

## Notation #

• `→+o`: Bundled ordered additive monoid homs. Also use for additive groups homs.
• `→*o`: Bundled ordered monoid homs. Also use for groups homs.
• `→*₀o`: Bundled ordered monoid with zero homs. Also use for groups with zero homs.

## 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 β]  :
Type (max u_6 u_7)
• to_add_monoid_hom : α →+ β
• monotone' :

`α →+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`
@[instance]
def order_add_monoid_hom_class.to_add_monoid_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β] [self : β] :
β
@[class]
structure order_add_monoid_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β]  :
Type (max u_6 u_7 u_8)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_add : (f : F) (x y : α), f (x + y) = f x + f y
• map_zero : (f : F), f 0 = 0
• monotone : (f : F),

`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`
structure order_monoid_hom (α : Type u_6) (β : Type u_7) [preorder α] [preorder β]  :
Type (max u_6 u_7)
• to_monoid_hom : α →* β
• monotone' :

`α →*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]
def order_monoid_hom_class.to_monoid_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β] [self : β] :
β
@[class]
structure order_monoid_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β]  :
Type (max u_6 u_7 u_8)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_mul : (f : F) (x y : α), f (x * y) = f x * f y
• map_one : (f : F), f 1 = 1
• monotone : (f : F),

`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_add_monoid_hom_class.to_order_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] :
β
Equations
@[protected, instance]
def order_monoid_hom_class.to_order_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] :
β
Equations
@[protected, instance]
def order_monoid_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] :
→*o β)
Equations
@[protected, instance]
def order_add_monoid_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] :
→+o β)
Equations
structure order_monoid_with_zero_hom (α : Type u_6) (β : Type u_7) [preorder α] [preorder β]  :
Type (max u_6 u_7)
• to_monoid_with_zero_hom : α →*₀ β
• monotone' :

`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`
@[instance]
def order_monoid_with_zero_hom_class.to_monoid_with_zero_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β] [self : β] :
@[class]
structure order_monoid_with_zero_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β]  :
Type (max u_6 u_7 u_8)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_mul : (f : F) (x y : α), f (x * y) = f x * f y
• map_one : (f : F), f 1 = 1
• map_zero : (f : F), f 0 = 0
• monotone : (f : F),

`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]
def order_monoid_with_zero_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β]  :
→*₀o β)
Equations
theorem map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) {a : α} (ha : 0 a) :
0 f a
theorem map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) {a : α} (ha : a 0) :
f a 0
theorem monotone_iff_map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) :
(a : α), 0 a 0 f a
theorem antitone_iff_map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) :
(a : α), 0 a f a 0
theorem monotone_iff_map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) :
(a : α), a 0 f a 0
theorem antitone_iff_map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) :
(a : α), a 0 0 f a
theorem strict_mono_iff_map_pos {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F)  :
(a : α), 0 < a 0 < f a
theorem strict_anti_iff_map_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F)  :
(a : α), 0 < a f a < 0
theorem strict_mono_iff_map_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F)  :
(a : α), a < 0 f a < 0
theorem strict_anti_iff_map_pos {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F)  :
(a : α), a < 0 0 < f a
@[protected, instance]
def order_add_monoid_hom.order_add_monoid_hom_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β]  :
α β
Equations
@[protected, instance]
def order_monoid_hom.order_monoid_hom_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β]  :
α β
Equations
@[protected, instance]
def order_add_monoid_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [preorder α] [preorder β]  :
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 β]  :
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 β] {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 β] {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 β] (f : α →*o β) :
theorem order_add_monoid_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+o β) :
@[simp]
theorem order_add_monoid_hom.coe_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+ β) (h : monotone f.to_fun) :
@[simp]
theorem order_monoid_hom.coe_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →* β) (h : monotone f.to_fun) :
@[simp]
theorem order_monoid_hom.mk_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*o β) (h : monotone f.to_fun) :
@[simp]
theorem order_add_monoid_hom.mk_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+o β) (h : monotone f.to_fun) :
def order_add_monoid_hom.to_order_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (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 β] (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 β] (f : α →*o β) :
@[simp]
theorem order_add_monoid_hom.coe_add_monoid_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+o β) :
@[simp]
theorem order_monoid_hom.coe_order_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*o β) :
@[simp]
theorem order_add_monoid_hom.coe_order_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+o β) :
theorem order_monoid_hom.to_monoid_hom_injective {α : Type u_2} {β : Type u_3} [preorder α] [preorder β]  :
theorem order_add_monoid_hom.to_order_hom_injective {α : Type u_2} {β : Type u_3} [preorder α] [preorder β]  :
theorem order_monoid_hom.to_order_hom_injective {α : Type u_2} {β : Type u_3} [preorder α] [preorder β]  :
@[protected]
def order_add_monoid_hom.copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (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 β] (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 β] (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 β] (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 β] (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 β] (f : α →+o β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]
def order_add_monoid_hom.id (α : Type u_2) [preorder α]  :
α →+o α

The identity map as an ordered additive monoid homomorphism.

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

The identity map as an ordered monoid homomorphism.

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

Composition of `order_add_monoid_hom`s as an `order_add_monoid_hom`

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

Composition of `order_monoid_hom`s 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 γ] (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 γ] (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 γ] (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 γ] (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 γ] (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 γ] (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 γ] (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 γ] (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 δ] (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 δ] (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 β] (f : α →+o β) :
= f
@[simp]
theorem order_monoid_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*o β) :
f.comp = f
@[simp]
theorem order_monoid_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*o β) :
f = f
@[simp]
theorem order_add_monoid_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →+o β) :
= f
theorem order_monoid_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] {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 γ] {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 γ] {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 γ] {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 β]  :
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 β]  :
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 β]  :
0 = 0
@[simp]
theorem order_monoid_hom.coe_one {α : Type u_2} {β : Type u_3} [preorder α] [preorder β]  :
1 = 1
@[simp]
theorem order_add_monoid_hom.zero_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (a : α) :
0 a = 0
@[simp]
theorem order_monoid_hom.one_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (a : α) :
1 a = 1
@[simp]
theorem order_add_monoid_hom.zero_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (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 γ] (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 γ] (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 γ] (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}  :
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} (f g : α →*o β) :
(f * g) = f * g
@[simp]
theorem order_add_monoid_hom.coe_add {α : Type u_2} {β : Type u_3} (f g : α →+o β) :
(f + g) = f + g
@[simp]
theorem order_monoid_hom.mul_apply {α : Type u_2} {β : Type u_3} (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} (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} (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} (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} (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} (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]
theorem order_add_monoid_hom.to_add_monoid_hom_eq_coe {α : Type u_2} {β : Type u_3} {hα : ordered_add_comm_monoid α} {hβ : ordered_add_comm_monoid β} (f : α →+o β) :
@[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) :
hf map_mul).to_monoid_hom = {to_fun := map_mul).to_fun, map_one' := _, map_mul' := _}
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 β]  :
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 β] {f g : α →*₀o β} (h : (a : α), f a = g a) :
f = g
theorem order_monoid_with_zero_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*₀o β) :
@[simp]
theorem order_monoid_with_zero_hom.coe_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*₀ β) (h : monotone f.to_fun) :
@[simp]
theorem order_monoid_with_zero_hom.mk_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*₀o β) (h : monotone f.to_fun) :
def order_monoid_with_zero_hom.to_order_monoid_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*₀o β) :
α →*o β

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

Equations
@[simp]
theorem order_monoid_with_zero_hom.coe_monoid_with_zero_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*₀o β) :
@[simp]
theorem order_monoid_with_zero_hom.coe_order_monoid_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*₀o β) :
@[protected]
def order_monoid_with_zero_hom.copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (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 β] (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 β] (f : α →*₀o β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]
def order_monoid_with_zero_hom.id (α : Type u_2) [preorder α]  :
α →*₀o α

The identity map as an ordered monoid with zero homomorphism.

Equations
@[simp]
theorem order_monoid_with_zero_hom.coe_id (α : Type u_2) [preorder α]  :
@[protected, instance]
Equations
def order_monoid_with_zero_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : β →*₀o γ) (g : α →*₀o β) :
α →*₀o γ

Composition of `order_monoid_with_zero_hom`s as an `order_monoid_with_zero_hom`.

Equations
@[simp]
theorem order_monoid_with_zero_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (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 γ] (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 γ] (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 γ] (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 δ] (f : γ →*₀o δ) (g : β →*₀o γ) (h : α →*₀o β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem order_monoid_with_zero_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*₀o β) :
@[simp]
theorem order_monoid_with_zero_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →*₀o β) :
theorem order_monoid_with_zero_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] {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 γ] {g : β →*₀o γ} {f₁ f₂ : α →*₀o β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected, instance]
def order_monoid_with_zero_hom.has_mul {α : Type u_2} {β : Type u_3}  :

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.coe_mul {α : Type u_2} {β : Type u_3} (f g : α →*₀o β) :
(f * g) = f * g
@[simp]
theorem order_monoid_with_zero_hom.mul_apply {α : Type u_2} {β : Type u_3} (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} (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} (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 β) :