algebra.order.hom.ring - mathlib3 docs

source

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

Type (max u_6 u_7)

to_ring_hom : α →+* β
monotone' : monotone self.to_ring_hom.to_fun

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

order_ring_hom.has_sizeof_inst
order_ring_hom.has_coe_t
order_ring_hom.order_ring_hom_class
order_ring_hom.has_coe_to_fun
order_ring_hom.inhabited
order_ring_hom.preorder
order_ring_hom.partial_order
order_ring_hom.subsingleton
linear_ordered_field.order_ring_hom.unique

source

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)

to_ring_equiv : α ≃+* β
map_le_map_iff' : ∀ {a b : α}, self.to_ring_equiv.to_fun a ≤ self.to_ring_equiv.to_fun b ↔ a ≤ b

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

order_ring_iso.has_sizeof_inst
order_ring_iso.has_coe_t
order_ring_iso.order_ring_iso_class
order_ring_iso.has_coe_to_fun
order_ring_iso.inhabited
order_ring_iso.subsingleton_right
order_ring_iso.subsingleton_left
linear_ordered_field.order_ring_iso.unique

source

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

to_ring_hom_class : ring_hom_class F α β
monotone : ∀ (f : F), monotone ⇑f

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

source

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

to_ring_equiv_class : ring_equiv_class F α β
map_le_map_iff : ∀ (f : F) {a b : α}, ⇑f a ≤ ⇑f b ↔ a ≤ b

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

order_ring_iso.order_ring_iso_class

Instances of other typeclasses for order_ring_iso_class

order_ring_iso_class.has_sizeof_inst

source

@[protected, instance]

def order_ring_hom_class.to_order_add_monoid_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] [order_ring_hom_class F α β] :

order_add_monoid_hom_class F α β

Equations

order_ring_hom_class.to_order_add_monoid_hom_class = {coe := ring_hom_class.coe order_ring_hom_class.to_ring_hom_class, coe_injective' := _, map_add := _, map_zero := _, monotone := _}

source

@[protected, instance]

def order_ring_hom_class.to_order_monoid_with_zero_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] [order_ring_hom_class F α β] :

order_monoid_with_zero_hom_class F α β

Equations

order_ring_hom_class.to_order_monoid_with_zero_hom_class = {coe := ring_hom_class.coe order_ring_hom_class.to_ring_hom_class, coe_injective' := _, map_mul := _, map_one := _, map_zero := _, monotone := _}

source

@[protected, instance]

def order_ring_iso_class.to_order_iso_class {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 α β] :

order_iso_class F α β

Equations

order_ring_iso_class.to_order_iso_class = {coe := ring_equiv_class.coe order_ring_iso_class.to_ring_equiv_class, inv := ring_equiv_class.inv order_ring_iso_class.to_ring_equiv_class, left_inv := _, right_inv := _, coe_injective' := _, map_le_map_iff := _}

source

@[protected, instance]

def order_ring_iso_class.to_order_ring_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] [order_ring_iso_class F α β] :

order_ring_hom_class F α β

Equations

order_ring_iso_class.to_order_ring_hom_class = {to_ring_hom_class := ring_equiv_class.to_ring_hom_class F α β order_ring_iso_class.to_ring_equiv_class, monotone := _}

source

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

order_ring_hom.has_coe_t = {coe := λ (f : F), {to_ring_hom := ↑f, monotone' := _}}

source

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

order_ring_iso.has_coe_t = {coe := λ (f : F), {to_ring_equiv := ↑f, map_le_map_iff' := _}}

source

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

f.to_order_add_monoid_hom = {to_add_monoid_hom := {to_fun := f.to_ring_hom.to_fun, map_zero' := _, map_add' := _}, monotone' := _}

source

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

f.to_order_monoid_with_zero_hom = {to_monoid_with_zero_hom := {to_fun := f.to_ring_hom.to_fun, map_zero' := _, map_one' := _, map_mul' := _}, monotone' := _}

source

@[protected, instance]

def order_ring_hom.order_ring_hom_class {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] :

order_ring_hom_class (α →+*o β) α β

Equations

order_ring_hom.order_ring_hom_class = {to_ring_hom_class := {coe := λ (f : α →+*o β), f.to_ring_hom.to_fun, coe_injective' := _, map_mul := _, map_one := _, map_add := _, map_zero := _}, monotone := _}

source

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

order_ring_hom.has_coe_to_fun = {coe := λ (f : α →+*o β), f.to_ring_hom.to_fun}

source

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

f.to_ring_hom.to_fun = ⇑f

source

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

source

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

f.to_ring_hom = ↑f

source

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

f.to_order_add_monoid_hom = ↑f

source

@[simp]

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

f.to_order_monoid_with_zero_hom = ↑f

source

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

⇑↑f = ⇑f

source

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

⇑↑f = ⇑f

source

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

⇑↑f = ⇑f

source

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

source

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

source

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

source

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

f.copy f' h = {to_ring_hom := {to_fun := (f.to_ring_hom.copy f' h).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, monotone' := _}

source

@[simp]

theorem order_ring_hom.coe_copy {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) (f' : α → β) (h : f' = ⇑f) :

⇑(f.copy f' h) = f'

source

theorem order_ring_hom.copy_eq {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] (f : α →+*o β) (f' : α → β) (h : f' = ⇑f) :

f.copy f' h = f

source

@[protected]

def order_ring_hom.id (α : Type u_2) [non_assoc_semiring α] [preorder α] :

α →+*o α

The identity as an ordered ring homomorphism.

Equations

order_ring_hom.id α = {to_ring_hom := {to_fun := (ring_hom.id α).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, monotone' := _}

source

@[protected, instance]

def order_ring_hom.inhabited (α : Type u_2) [non_assoc_semiring α] [preorder α] :

inhabited (α →+*o α)

Equations

order_ring_hom.inhabited α = {default := order_ring_hom.id α _inst_2}

source

@[simp]

theorem order_ring_hom.coe_id (α : Type u_2) [non_assoc_semiring α] [preorder α] :

⇑(order_ring_hom.id α) = id

source

@[simp]

theorem order_ring_hom.id_apply {α : Type u_2} [non_assoc_semiring α] [preorder α] (a : α) :

⇑(order_ring_hom.id α) a = a

source

@[simp]

theorem order_ring_hom.coe_ring_hom_id {α : Type u_2} [non_assoc_semiring α] [preorder α] :

↑(order_ring_hom.id α) = ring_hom.id α

source

@[simp]

theorem order_ring_hom.coe_order_add_monoid_hom_id {α : Type u_2} [non_assoc_semiring α] [preorder α] :

↑(order_ring_hom.id α) = order_add_monoid_hom.id α

source

@[simp]

theorem order_ring_hom.coe_order_monoid_with_zero_hom_id {α : Type u_2} [non_assoc_semiring α] [preorder α] :

↑(order_ring_hom.id α) = order_monoid_with_zero_hom.id α

source

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

f.comp g = {to_ring_hom := {to_fun := (f.to_ring_hom.comp g.to_ring_hom).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, monotone' := _}

source

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

source

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

source

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)

source

@[simp]

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

f.comp (order_ring_hom.id α) = f

source

@[simp]

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

(order_ring_hom.id β).comp f = f

source

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₂

source

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₂

source

@[protected, instance]

def order_ring_hom.preorder {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] :

preorder (α →+*o β)

Equations

order_ring_hom.preorder = preorder.lift coe_fn

source

@[protected, instance]

def order_ring_hom.partial_order {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [partial_order β] :

partial_order (α →+*o β)

Equations

order_ring_hom.partial_order = partial_order.lift coe_fn order_ring_hom.partial_order._proof_1

source

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

f.to_order_iso = {to_equiv := f.to_ring_equiv.to_equiv, map_rel_iff' := _}

source

@[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 β] :

order_ring_iso_class (α ≃+*o β) α β

Equations

order_ring_iso.order_ring_iso_class = {to_ring_equiv_class := {coe := λ (f : α ≃+*o β), f.to_ring_equiv.to_fun, inv := λ (f : α ≃+*o β), f.to_ring_equiv.inv_fun, left_inv := _, right_inv := _, coe_injective' := _, map_mul := _, map_add := _}, map_le_map_iff := _}

source

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

order_ring_iso.has_coe_to_fun = fun_like.has_coe_to_fun

source

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 β) :

f.to_ring_equiv.to_fun = ⇑f

source

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

source

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

⇑{to_ring_equiv := e, map_le_map_iff' := h} = ⇑e

source

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

{to_ring_equiv := ↑e, map_le_map_iff' := h} = e

source

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

f.to_ring_equiv = ↑f

source

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

f.to_order_iso = ↑f

source

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

⇑↑f = ⇑f

source

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

⇑↑f = ⇑f

source

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

order_ring_iso.refl α = {to_ring_equiv := ring_equiv.refl α _inst_2, map_le_map_iff' := _}

source

@[protected, instance]

def order_ring_iso.inhabited (α : Type u_2) [has_mul α] [has_add α] [has_le α] :

inhabited (α ≃+*o α)

Equations

order_ring_iso.inhabited α = {default := order_ring_iso.refl α _inst_3}

source

@[simp]

theorem order_ring_iso.refl_apply (α : Type u_2) [has_mul α] [has_add α] [has_le α] (x : α) :

⇑(order_ring_iso.refl α) x = x

source

@[simp]

theorem order_ring_iso.coe_ring_equiv_refl (α : Type u_2) [has_mul α] [has_add α] [has_le α] :

↑(order_ring_iso.refl α) = ring_equiv.refl α

source

@[simp]

theorem order_ring_iso.coe_order_iso_refl (α : Type u_2) [has_mul α] [has_add α] [has_le α] :

↑(order_ring_iso.refl α) = order_iso.refl α

source

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

e.symm = {to_ring_equiv := e.to_ring_equiv.symm, map_le_map_iff' := _}

source

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

order_ring_iso.simps.symm_apply e = ⇑(e.symm)

source

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

source

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

(f.trans g).to_ring_equiv = f.to_ring_equiv.trans g.to_ring_equiv

source

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

f.trans g = {to_ring_equiv := f.to_ring_equiv.trans g.to_ring_equiv, map_le_map_iff' := _}

source

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

source

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

e.trans e.symm = order_ring_iso.refl α

source

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

e.symm.trans e = order_ring_iso.refl β

source

theorem order_ring_iso.symm_bijective {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_le α] [has_mul β] [has_add β] [has_le β] :

function.bijective order_ring_iso.symm

source

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

f.to_order_ring_hom = {to_ring_hom := f.to_ring_equiv.to_ring_hom, monotone' := _}

source

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

f.to_order_ring_hom = ↑f

source

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

⇑↑f = ⇑f

source

@[simp]

theorem order_ring_iso.coe_to_order_ring_hom_refl {α : Type u_2} [non_assoc_semiring α] [preorder α] :

↑(order_ring_iso.refl α) = order_ring_hom.id α

source

theorem order_ring_iso.to_order_ring_hom_injective {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [preorder α] [non_assoc_semiring β] [preorder β] :

function.injective order_ring_iso.to_order_ring_hom

source

@[protected, instance]

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

subsingleton (α →+*o β)

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

source

@[protected, instance]

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

subsingleton (α ≃+*o β)

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

source

@[protected, instance]

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

subsingleton (α ≃+*o β)

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

mathlib3 documentation

Ordered ring homomorphisms #

Main definitions #

Notation #

Tags #

Ordered ring homomorphisms #

Ordered ring isomorphisms #

Uniqueness #