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.
Implementation notes #
This file used to define typeclasses for order-preserving ring homomorphisms and isomorphisms.
In https://github.com/leanprover-community/mathlib4/pull/10544, we migrated from assumptions like [FunLike F R S] [OrderRingHomClass F R S]
to assumptions like [FunLike F R S] [OrderHomClass F R S] [RingHomClass F R S]
,
making some typeclasses and instances irrelevant.
Tags #
ordered ring homomorphism, order homomorphism
OrderRingHom α β
, denoted α →+*o β
,
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
.
- toFun : α → β
The proposition that the function preserves the order.
Instances For
OrderRingHom α β
, denoted α →+*o β
,
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
.
Equations
Instances For
OrderRingIso α β
, denoted as α ≃+*o β
,
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
.
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
The proposition that the function preserves the order bijectively.
Instances For
OrderRingIso α β
, denoted as α ≃+*o β
,
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
.
Equations
Instances For
Turn an element of a type F
satisfying OrderHomClass F α β
and RingHomClass F α β
into an actual OrderRingHom
.
This is declared as the default coercion from F
to α →+*o β
.
Equations
Instances For
Any type satisfying OrderRingHomClass
can be cast into OrderRingHom
via
OrderRingHomClass.toOrderRingHom
.
Equations
Turn an element of a type F
satisfying OrderIsoClass F α β
and RingEquivClass F α β
into an actual OrderRingIso
.
This is declared as the default coercion from F
to α ≃+*o β
.
Equations
Instances For
Any type satisfying OrderRingIsoClass
can be cast into OrderRingIso
via
OrderRingIsoClass.toOrderRingIso
.
Equations
Ordered ring homomorphisms #
Reinterpret an ordered ring homomorphism as an ordered additive monoid homomorphism.
Equations
Instances For
Reinterpret an ordered ring homomorphism as an order homomorphism.
Equations
Instances For
Equations
Copy of an OrderRingHom
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Equations
Instances For
The identity as an ordered ring homomorphism.
Equations
Instances For
Equations
Composition of two OrderRingHom
s as an OrderRingHom
.
Equations
Instances For
Equations
Equations
Ordered ring isomorphisms #
This lemma used to be generated by [simps] on trans
, but the lhs of this simplifies under
simp. Removed [simps] attribute and added aux version below.
Reinterpret an ordered ring isomorphism as an ordered ring homomorphism.