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

source
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
source
@[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 β] [add_zero_class α] [add_zero_class β] [self : order_add_monoid_hom_class F α β] :
add_monoid_hom_class F α β
source
@[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
source
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
source
@[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 β] [mul_one_class α] [mul_one_class β] [self : order_monoid_hom_class F α β] :
monoid_hom_class F α β
source
@[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
source
@[protected, instance]
def order_add_monoid_hom_class.to_order_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] [order_add_monoid_hom_class F α β] :
order_hom_class F α β
Equations
source
@[protected, instance]
def order_monoid_hom_class.to_order_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] [order_monoid_hom_class F α β] :
order_hom_class F α β
Equations
source
@[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
source
@[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
source
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
source
@[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 β] [mul_zero_one_class α] [mul_zero_one_class β] [self : order_monoid_with_zero_hom_class F α β] :
monoid_with_zero_hom_class F α β
source
@[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
source
@[protected, instance]
def order_monoid_with_zero_hom_class.to_order_monoid_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] [order_monoid_with_zero_hom_class F α β] :
order_monoid_hom_class F α β
Equations
source
@[protected, instance]
def order_monoid_with_zero_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] [order_monoid_with_zero_hom_class F α β] :
has_coe_t F (α →*₀o β)
Equations
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[protected, instance]
def order_add_monoid_hom.order_add_monoid_hom_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] :
order_add_monoid_hom_class (α →+o β) α β
Equations
source
@[protected, instance]
def order_monoid_hom.order_monoid_hom_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] :
order_monoid_hom_class (α →*o β) α β
Equations
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem order_monoid_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) :
f.to_monoid_hom.to_fun = ⇑f
source
theorem order_add_monoid_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) :
f.to_add_monoid_hom.to_fun = ⇑f
source
@[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) :
⇑{to_add_monoid_hom := f, monotone' := h} = ⇑f
source
@[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) :
⇑{to_monoid_hom := f, monotone' := h} = ⇑f
source
@[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) :
{to_monoid_hom := ↑f, monotone' := h} = f
source
@[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) :
{to_add_monoid_hom := ↑f, monotone' := h} = f
source
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
source
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
source
@[simp]
theorem order_monoid_hom.coe_monoid_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) :
⇑↑f = ⇑f
source
@[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 β) :
⇑↑f = ⇑f
source
@[simp]
theorem order_monoid_hom.coe_order_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) :
⇑↑f = ⇑f
source
@[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 β) :
⇑↑f = ⇑f
source
theorem order_monoid_hom.to_monoid_hom_injective {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] :
function.injective order_monoid_hom.to_monoid_hom
source
theorem order_add_monoid_hom.to_add_monoid_hom_injective {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] :
function.injective order_add_monoid_hom.to_add_monoid_hom
source
theorem order_add_monoid_hom.to_order_hom_injective {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] :
function.injective order_add_monoid_hom.to_order_hom
source
theorem order_monoid_hom.to_order_hom_injective {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] :
function.injective order_monoid_hom.to_order_hom
source
@[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
source
@[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
source
@[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'
source
@[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'
source
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
source
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
source
@[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
source
@[protected]
def order_monoid_hom.id (α : Type u_2) [preorder α] [mul_one_class α] :
α →*o α

The identity map as an ordered monoid homomorphism.

Equations
source
@[simp]
theorem order_monoid_hom.coe_id (α : Type u_2) [preorder α] [mul_one_class α] :
⇑(order_monoid_hom.id α) = id
source
@[simp]
theorem order_add_monoid_hom.coe_id (α : Type u_2) [preorder α] [add_zero_class α] :
⇑(order_add_monoid_hom.id α) = id
source
@[protected, instance]
def order_add_monoid_hom.inhabited (α : Type u_2) [preorder α] [add_zero_class α] :
inhabited (α →+o α)
Equations
source
@[protected, instance]
def order_monoid_hom.inhabited (α : Type u_2) [preorder α] [mul_one_class α] :
inhabited (α →*o α)
Equations
source
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
source
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
source
@[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
source
@[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
source
@[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)
source
@[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)
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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)
source
@[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)
source
@[simp]
theorem order_add_monoid_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) :
f.comp (order_add_monoid_hom.id α) = f
source
@[simp]
theorem order_monoid_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) :
f.comp (order_monoid_hom.id α) = f
source
@[simp]
theorem order_monoid_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] (f : α →*o β) :
(order_monoid_hom.id β).comp f = f
source
@[simp]
theorem order_add_monoid_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] (f : α →+o β) :
(order_add_monoid_hom.id β).comp f = f
source
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₂
source
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₂
source
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₂
source
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₂
source
@[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
source
@[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
source
@[simp]
theorem order_add_monoid_hom.coe_zero {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [add_zero_class α] [add_zero_class β] :
⇑0 = 0
source
@[simp]
theorem order_monoid_hom.coe_one {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_one_class α] [mul_one_class β] :
⇑1 = 1
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[protected, instance]
def order_add_monoid_hom.has_add {α : Type u_2} {β : Type u_3} [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] :
has_add (α →+o β)

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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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₂
source
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₂
source
@[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 β) :
f.to_monoid_hom = ↑f
source
@[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 β) :
f.to_add_monoid_hom = ↑f
source
@[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 β) :
f.to_order_hom = ↑f
source
@[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 β) :
f.to_order_hom = ↑f
source
@[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) :
(order_add_monoid_hom.mk' f hf map_mul).to_add_monoid_hom = {to_fun := (add_monoid_hom.mk' f map_mul).to_fun, map_zero' := _, map_add' := _}
source
@[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) :
(order_monoid_hom.mk' f hf map_mul).to_monoid_hom = {to_fun := (monoid_hom.mk' f map_mul).to_fun, map_one' := _, map_mul' := _}
source
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
source
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
source
@[protected, instance]
def order_monoid_with_zero_hom.order_monoid_with_zero_hom_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] :
order_monoid_with_zero_hom_class (α →*₀o β) α β
Equations
source
@[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
source
@[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
source
theorem order_monoid_with_zero_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] (f : α →*₀o β) :
f.to_monoid_with_zero_hom.to_fun = ⇑f
source
@[simp]
theorem order_monoid_with_zero_hom.coe_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] (f : α →*₀ β) (h : monotone f.to_fun) :
⇑{to_monoid_with_zero_hom := f, monotone' := h} = ⇑f
source
@[simp]
theorem order_monoid_with_zero_hom.mk_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] (f : α →*₀o β) (h : monotone ↑f.to_fun) :
{to_monoid_with_zero_hom := ↑f, monotone' := h} = f
source
def order_monoid_with_zero_hom.to_order_monoid_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] (f : α →*₀o β) :
α →*o β

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

Equations
source
@[simp]
theorem order_monoid_with_zero_hom.coe_monoid_with_zero_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] (f : α →*₀o β) :
⇑↑f = ⇑f
source
@[simp]
theorem order_monoid_with_zero_hom.coe_order_monoid_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] (f : α →*₀o β) :
⇑↑f = ⇑f
source
theorem order_monoid_with_zero_hom.to_order_monoid_hom_injective {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] :
function.injective order_monoid_with_zero_hom.to_order_monoid_hom
source
theorem order_monoid_with_zero_hom.to_monoid_with_zero_hom_injective {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] :
function.injective order_monoid_with_zero_hom.to_monoid_with_zero_hom
source
@[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
source
@[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'
source
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
source
@[protected]
def order_monoid_with_zero_hom.id (α : Type u_2) [preorder α] [mul_zero_one_class α] :
α →*₀o α

The identity map as an ordered monoid with zero homomorphism.

Equations
source
@[simp]
theorem order_monoid_with_zero_hom.coe_id (α : Type u_2) [preorder α] [mul_zero_one_class α] :
⇑(order_monoid_with_zero_hom.id α) = id
source
@[protected, instance]
def order_monoid_with_zero_hom.inhabited (α : Type u_2) [preorder α] [mul_zero_one_class α] :
inhabited (α →*₀o α)
Equations
source
def order_monoid_with_zero_hom.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 β) :
α →*₀o γ

Composition of order_monoid_with_zero_homs as an order_monoid_with_zero_hom.

Equations
source
@[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
source
@[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)
source
@[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
source
@[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
source
@[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)
source
@[simp]
theorem order_monoid_with_zero_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] (f : α →*₀o β) :
f.comp (order_monoid_with_zero_hom.id α) = f
source
@[simp]
theorem order_monoid_with_zero_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [mul_zero_one_class α] [mul_zero_one_class β] (f : α →*₀o β) :
(order_monoid_with_zero_hom.id β).comp f = f
source
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₂
source
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₂
source
@[protected, instance]
def order_monoid_with_zero_hom.has_mul {α : Type u_2} {β : Type u_3} [linear_ordered_comm_monoid_with_zero α] [linear_ordered_comm_monoid_with_zero β] :
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
source
@[simp]
theorem order_monoid_with_zero_hom.coe_mul {α : Type u_2} {β : Type u_3} [linear_ordered_comm_monoid_with_zero α] [linear_ordered_comm_monoid_with_zero β] (f g : α →*₀o β) :
⇑(f * g) = ⇑f * ⇑g
source
@[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
source
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
source
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₂
source
@[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 β) :
f.to_monoid_with_zero_hom = ↑f
source
@[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 β) :
f.to_order_monoid_hom = ↑f