Ordered ring homomorphisms #
Homomorphisms between ordered (semi)rings that respect the ordering.
Main definitions #
OrderRingHom
: Monotone semiring homomorphisms.OrderRingIso
: Monotone semiring isomorphisms.
Notation #
→+*o
: Ordered ring homomorphisms.≃+*o
: Ordered ring isomorphisms.
Tags #
ordered ring homomorphism, order homomorphism
- toFun : α → β
- map_one' : OneHom.toFun (↑↑s.toRingHom) 1 = 1
- map_mul' : ∀ (x y : α), OneHom.toFun (↑↑s.toRingHom) (x * y) = OneHom.toFun (↑↑s.toRingHom) x * OneHom.toFun (↑↑s.toRingHom) y
- map_zero' : OneHom.toFun (↑↑s.toRingHom) 0 = 0
- map_add' : ∀ (x y : α), OneHom.toFun (↑↑s.toRingHom) (x + y) = OneHom.toFun (↑↑s.toRingHom) x + OneHom.toFun (↑↑s.toRingHom) y
- monotone' : Monotone s.toFun
The proposition that the function preserves the order.
OrderRingHom α β
is the type of monotone semiring homomorphisms from α
to β
.
When possible, instead of parametrizing results over (f : OrderRingHom α β)
,
you should parametrize over (F : Type*) [OrderRingHomClass F α β] (f : F)
.
When you extend this structure, make sure to extend OrderRingHomClass
.
Instances For
OrderRingHom α β
is the type of monotone semiring homomorphisms from α
to β
.
When possible, instead of parametrizing results over (f : OrderRingHom α β)
,
you should parametrize over (F : Type*) [OrderRingHomClass F α β] (f : F)
.
When you extend this structure, make sure to extend OrderRingHomClass
.
Instances For
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- map_mul' : ∀ (x y : α), Equiv.toFun s.toEquiv (x * y) = Equiv.toFun s.toEquiv x * Equiv.toFun s.toEquiv y
- map_add' : ∀ (x y : α), Equiv.toFun s.toEquiv (x + y) = Equiv.toFun s.toEquiv x + Equiv.toFun s.toEquiv y
- map_le_map_iff' : ∀ {a b : α}, Equiv.toFun s.toEquiv a ≤ Equiv.toFun s.toEquiv b ↔ a ≤ b
The proposition that the function preserves the order bijectively.
OrderRingHom α β
is the type of order-preserving semiring isomorphisms between α
and β
.
When possible, instead of parametrizing results over (f : OrderRingIso α β)
,
you should parametrize over (F : Type*) [OrderRingIsoClass F α β] (f : F)
.
When you extend this structure, make sure to extend OrderRingIsoClass
.
Instances For
OrderRingHom α β
is the type of order-preserving semiring isomorphisms between α
and β
.
When possible, instead of parametrizing results over (f : OrderRingIso α β)
,
you should parametrize over (F : Type*) [OrderRingIsoClass F α β] (f : F)
.
When you extend this structure, make sure to extend OrderRingIsoClass
.
Instances For
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
- map_one : ∀ (f : F), ↑f 1 = 1
- map_zero : ∀ (f : F), ↑f 0 = 0
- monotone : ∀ (f : F), Monotone ↑f
The proposition that the function preserves the order.
OrderRingHomClass F α β
states that F
is a type of ordered semiring homomorphisms.
You should extend this typeclass when you extend OrderRingHom
.
Instances
- coe : F → α → β
- inv : F → β → α
- left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
- right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
- coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
The proposition that the function preserves the order bijectively.
OrderRingIsoClass F α β
states that F
is a type of ordered semiring isomorphisms.
You should extend this class when you extend OrderRingIso
.
Instances
Turn an element of a type F
satisfying OrderRingHomClass F α β
into an actual
OrderRingHom
. This is declared as the default coercion from F
to α →+*o β
.
Instances For
Any type satisfying OrderRingHomClass
can be cast into OrderRingHom
via
OrderRingHomClass.toOrderRingHom
.
Turn an element of a type F
satisfying OrderRingIsoClass F α β
into an actual
OrderRingIso
. This is declared as the default coercion from F
to α ≃+*o β
.
Instances For
Any type satisfying OrderRingIsoClass
can be cast into OrderRingIso
via
OrderRingIsoClass.toOrderRingIso
.
Ordered ring homomorphisms #
Reinterpret an ordered ring homomorphism as an ordered additive monoid homomorphism.
Instances For
Reinterpret an ordered ring homomorphism as an order homomorphism.
Instances For
Copy of an OrderRingHom
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Instances For
The identity as an ordered ring homomorphism.
Instances For
Composition of two OrderRingHom
s as an OrderRingHom
.
Instances For
Ordered ring isomorphisms #
Reinterpret an ordered ring isomorphism as an ordered ring homomorphism.
Instances For
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.
There is at most one ordered ring homomorphism from a linear ordered field to an archimedean linear ordered field.
There is at most one ordered ring isomorphism between a linear ordered field and an archimedean linear ordered field.
There is at most one ordered ring isomorphism between an archimedean linear ordered field and a linear ordered field.