mathlib documentation

algebra.order.hom.ring

Ordered ring homomorphisms #

Homomorphisms between ordered (semi)rings that respect the ordering.

Main definitions #

Notation #

Tags #

ordered ring homomorphism, order homomorphism

structure order_ring_hom (α : Type u_6) (β : Type u_7) [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] :
Type (max u_6 u_7)

order_ring_hom α β is the type of monotone semiring homomorphisms from α to β.

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

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

Instances for order_ring_hom
structure order_ring_iso (α : Type u_6) (β : Type u_7) [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] :
Type (max u_6 u_7)

order_ring_hom α β is the type of order-preserving semiring isomorphisms between α and β.

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

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

Instances for order_ring_iso
@[class]
structure order_ring_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] :
Type (max u_6 u_7 u_8)

order_ring_hom_class F α β states that F is a type of ordered semiring homomorphisms. You should extend this typeclass when you extend order_ring_hom.

Instances of this typeclass
Instances of other typeclasses for order_ring_hom_class
  • order_ring_hom_class.has_sizeof_inst
@[class]
structure order_ring_iso_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] :
Type (max u_6 u_7 u_8)

order_ring_iso_class F α β states that F is a type of ordered semiring isomorphisms. You should extend this class when you extend order_ring_iso.

Instances of this typeclass
Instances of other typeclasses for order_ring_iso_class
  • order_ring_iso_class.has_sizeof_inst
@[protected, instance]
def order_ring_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] [order_ring_hom_class F α β] :
has_coe_t F →+*o β)
Equations
@[protected, instance]
def order_ring_iso.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] [order_ring_iso_class F α β] :
has_coe_t F ≃+*o β)
Equations

Ordered ring homomorphisms #

def order_ring_hom.to_order_add_monoid_hom {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) :
α →+o β

Reinterpret an ordered ring homomorphism as an ordered additive monoid homomorphism.

Equations
def order_ring_hom.to_order_monoid_with_zero_hom {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) :
α →*₀o β

Reinterpret an ordered ring homomorphism as an order homomorphism.

Equations
@[protected, instance]
def order_ring_hom.order_ring_hom_class {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] :
Equations
@[protected, instance]
def order_ring_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [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
theorem order_ring_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) :
@[ext]
theorem order_ring_hom.ext {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] {f g : α →+*o β} (h : ∀ (a : α), f a = g a) :
f = g
@[simp]
theorem order_ring_hom.to_ring_hom_eq_coe {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) :
@[simp]
theorem order_ring_hom.to_order_add_monoid_hom_eq_coe {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) :
@[simp]
theorem order_ring_hom.coe_coe_ring_hom {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) :
@[simp]
theorem order_ring_hom.coe_coe_order_add_monoid_hom {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) :
@[simp]
theorem order_ring_hom.coe_coe_order_monoid_with_zero_hom {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) :
@[norm_cast]
theorem order_ring_hom.coe_ring_hom_apply {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) (a : α) :
f a = f a
@[norm_cast]
theorem order_ring_hom.coe_order_add_monoid_hom_apply {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) (a : α) :
f a = f a
@[norm_cast]
theorem order_ring_hom.coe_order_monoid_with_zero_hom_apply {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) (a : α) :
f a = f a
@[protected]
def order_ring_hom.copy {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) (f' : α → β) (h : f' = f) :
α →+*o β

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

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

The identity as an ordered ring homomorphism.

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

Composition of two order_ring_homs as an order_ring_hom.

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

Ordered ring isomorphisms #

def order_ring_iso.to_order_iso {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
α ≃o β

Reinterpret an ordered ring isomorphism as an order isomorphism.

Equations
@[protected, instance]
def order_ring_iso.order_ring_iso_class {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] :
Equations
@[protected, instance]
def order_ring_iso.has_coe_to_fun {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] :
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
theorem order_ring_iso.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
@[ext]
theorem order_ring_iso.ext {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] {f g : α ≃+*o β} (h : ∀ (a : α), f a = g a) :
f = g
@[simp]
theorem order_ring_iso.coe_mk {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+* β) (h : ∀ {a b : α}, e.to_fun a e.to_fun b a b) :
@[simp]
theorem order_ring_iso.mk_coe {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) (h : ∀ {a b : α}, e.to_fun a e.to_fun b a b) :
@[simp]
theorem order_ring_iso.to_ring_equiv_eq_coe {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
@[simp]
theorem order_ring_iso.to_order_iso_eq_coe {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
@[simp, norm_cast]
theorem order_ring_iso.coe_to_ring_equiv {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
@[simp, norm_cast]
theorem order_ring_iso.coe_to_order_iso {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (f : α ≃+*o β) :
@[protected, refl]
def order_ring_iso.refl (α : Type u_2) [has_mul α] [has_add α] [has_le α] :
α ≃+*o α

The identity map as an ordered ring isomorphism.

Equations
@[protected, instance]
def order_ring_iso.inhabited (α : Type u_2) [has_mul α] [has_add α] [has_le α] :
Equations
@[simp]
theorem order_ring_iso.refl_apply (α : Type u_2) [has_mul α] [has_add α] [has_le α] (x : α) :
@[simp]
@[simp]
@[protected, symm]
def order_ring_iso.symm {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) :
β ≃+*o α

The inverse of an ordered ring isomorphism as an ordered ring isomorphism.

Equations
def order_ring_iso.simps.symm_apply {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) :
β → α

See Note [custom simps projection]

Equations
@[simp]
theorem order_ring_iso.symm_symm {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) :
e.symm.symm = e
@[simp]
theorem order_ring_iso.trans_to_ring_equiv {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] [has_mul γ] [has_add γ] [has_le γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
@[protected, trans]
def order_ring_iso.trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] [has_mul γ] [has_add γ] [has_le γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
α ≃+*o γ

Composition of order_ring_isos as an order_ring_iso.

Equations
@[simp]
theorem order_ring_iso.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] [has_mul γ] [has_add γ] [has_le γ] (f : α ≃+*o β) (g : β ≃+*o γ) (a : α) :
(f.trans g) a = g (f a)
@[simp]
theorem order_ring_iso.self_trans_symm {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) :
@[simp]
theorem order_ring_iso.symm_trans_self {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] (e : α ≃+*o β) :
theorem order_ring_iso.symm_bijective {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] :
def order_ring_iso.to_order_ring_hom {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α ≃+*o β) :
α →+*o β

Reinterpret an ordered ring isomorphism as an ordered ring homomorphism.

Equations
@[simp]
theorem order_ring_iso.to_order_ring_hom_eq_coe {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α ≃+*o β) :
@[simp, norm_cast]
theorem order_ring_iso.coe_to_order_ring_hom {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α ≃+*o β) :

Uniqueness #

There is at most one ordered ring homomorphism from a linear ordered field to an archimedean linear ordered field. Reciprocally, such an ordered ring homomorphism exists when the codomain is further conditionally complete.

@[protected, instance]
def order_ring_hom.subsingleton {α : Type u_2} {β : Type u_3} [linear_ordered_field α] [linear_ordered_field β] [archimedean β] :

There is at most one ordered ring homomorphism from a linear ordered field to an archimedean linear ordered field.

@[protected, instance]
def order_ring_iso.subsingleton_right {α : Type u_2} {β : Type u_3} [linear_ordered_field α] [linear_ordered_field β] [archimedean β] :

There is at most one ordered ring isomorphism between a linear ordered field and an archimedean linear ordered field.

@[protected, instance]
def order_ring_iso.subsingleton_left {α : Type u_2} {β : Type u_3} [linear_ordered_field α] [archimedean α] [linear_ordered_field β] :

There is at most one ordered ring isomorphism between an archimedean linear ordered field and a linear ordered field.