Order homomorphisms #
This file defines order homomorphisms, which are bundled monotone functions. A preorder
homomorphism f : α →o β
is a function α → β
along with a proof that ∀ x y, x ≤ y → f x ≤ f y
.
Main definitions #
In this file we define the following bundled monotone maps:
OrderHom α β
a.k.a.α →o β
: Preorder homomorphism. AnOrderHom α β
is a functionf : α → β
such thata₁ ≤ a₂ → f a₁ ≤ f a₂
OrderEmbedding α β
a.k.a.α ↪o β
: Relation embedding. AnOrderEmbedding α β
is an embeddingf : α ↪ β
such thata ≤ b ↔ f a ≤ f b
. Defined as an abbreviation of@RelEmbedding α β (≤) (≤)
.OrderIso
: Relation isomorphism. AnOrderIso α β
is an equivalencef : α ≃ β
such thata ≤ b ↔ f a ≤ f b
. Defined as an abbreviation of@RelIso α β (≤) (≤)
.
We also define many OrderHom
s. In some cases we define two versions, one with ₘ
suffix and
one without it (e.g., OrderHom.compₘ
and OrderHom.comp
). This means that the former
function is a "more bundled" version of the latter. We can't just drop the "less bundled" version
because the more bundled version usually does not work with dot notation.
OrderHom.id
: identity map asα →o α
;OrderHom.curry
: an order isomorphism betweenα × β →o γ
andα →o β →o γ
;OrderHom.comp
: composition of two bundled monotone maps;OrderHom.compₘ
: composition of bundled monotone maps as a bundled monotone map;OrderHom.const
: constant function as a bundled monotone map;OrderHom.prod
: combineα →o β
andα →o γ
intoα →o β × γ
;OrderHom.prodₘ
: a more bundled version ofOrderHom.prod
;OrderHom.prodIso
: order isomorphism betweenα →o β × γ
and(α →o β) × (α →o γ)
;OrderHom.diag
: diagonal embedding ofα
intoα × α
as a bundled monotone map;OrderHom.onDiag
: restrict a monotone mapα →o α →o β
to the diagonal;OrderHom.fst
: projectionProd.fst : α × β → α
as a bundled monotone map;OrderHom.snd
: projectionProd.snd : α × β → β
as a bundled monotone map;OrderHom.prodMap
:Prod.map f g
as a bundled monotone map;Pi.evalOrderHom
: evaluation of a function at a pointFunction.eval i
as a bundled monotone map;OrderHom.coeFnHom
: coercion to function as a bundled monotone map;OrderHom.apply
: application of anOrderHom
at a point as a bundled monotone map;OrderHom.pi
: combine a family of monotone mapsf i : α →o π i
into a monotone mapα →o Π i, π i
;OrderHom.piIso
: order isomorphism betweenα →o Π i, π i
andΠ i, α →o π i
;OrderHom.subtype.val
: embeddingSubtype.val : Subtype p → α
as a bundled monotone map;OrderHom.dual
: reinterpret a monotone mapα →o β
as a monotone mapαᵒᵈ →o βᵒᵈ
;OrderHom.dualIso
: order isomorphism betweenα →o β
and(αᵒᵈ →o βᵒᵈ)ᵒᵈ
;OrderHom.compl
: order isomorphismα ≃o αᵒᵈ
given by taking complements in a boolean algebra;
We also define two functions to convert other bundled maps to α →o β
:
OrderEmbedding.toOrderHom
: convertα ↪o β
toα →o β
;RelHom.toOrderHom
: convert aRelHom
between strict orders to anOrderHom
.
Tags #
monotone map, bundled morphism
An order embedding is an embedding f : α ↪ β
such that a ≤ b ↔ (f a) ≤ (f b)
.
This definition is an abbreviation of RelEmbedding (≤) (≤)
.
Equations
Instances For
Turn an element of a type F
satisfying OrderIsoClass F α β
into an actual
OrderIso
. This is declared as the default coercion from F
to α ≃o β
.
Equations
Instances For
Any type satisfying OrderIsoClass
can be cast into OrderIso
via
OrderIsoClass.toOrderIso
.
Equations
Turn an element of a type F
satisfying OrderHomClass F α β
into an actual
OrderHom
. This is declared as the default coercion from F
to α →o β
.
Equations
Instances For
Any type satisfying OrderHomClass
can be cast into OrderHom
via
OrderHomClass.toOrderHom
.
Equations
One can lift an unbundled monotone function to a bundled one.
The identity function as bundled monotone function.
Equations
Instances For
Equations
Evaluation of an unbundled function at a point (Function.eval
) as an OrderHom
.
Equations
Instances For
Function application fun f => f a
(for fixed a
) is a monotone function from the
monotone function space α →o β
to β
. See also Pi.evalOrderHom
.
Equations
Instances For
There is a unique monotone map from a subsingleton to itself.
Equations
Embeddings of partial orders that preserve <
also preserve ≤
.
Equations
Instances For
A preorder which embeds into a well-founded preorder is itself well-founded.
A preorder which embeds into a preorder in which (· > ·)
is well-founded
also has (· > ·)
well-founded.
To define an order embedding from a partial order to a preorder it suffices to give a function
together with a proof that it satisfies f a ≤ f b ↔ a ≤ b
.
Equations
Instances For
A strictly monotone map from a linear order is an order embedding.
Equations
Instances For
Convert an OrderEmbedding
to an OrderHom
.
Equations
Instances For
If the images by an order embedding of two elements are disjoint, then they are themselves disjoint.
If the images by an order embedding of two elements are codisjoint, then they are themselves codisjoint.
If the images by an order embedding of two elements are complements, then they are themselves complements.
A bundled expression of the fact that a map between partial orders that is strictly monotone is weakly monotone.
Equations
Instances For
Identity order isomorphism.
Equations
Instances For
An order isomorphism between the domains and codomains of two prosets of order homomorphisms gives an order isomorphism between the two function prosets.
Equations
Instances For
Alias of the reverse direction of OrderIso.le_iff_le
.
Alias of the reverse direction of OrderIso.lt_iff_lt
.
Converts a RelIso (<) (<)
into an OrderIso
.
Equations
Instances For
To show that f : α → β
, g : β → α
make up an order isomorphism of linear orders,
it suffices to prove cmp a (g b) = cmp (f a) b
.
Equations
Instances For
To show that f : α →o β
and g : β →o α
make up an order isomorphism it is enough to show
that g
is the inverse of f
.
Equations
Instances For
A strictly monotone function with a right inverse is an order isomorphism.
Equations
Instances For
Note that this goal could also be stated (Disjoint on f) a b
Note that this goal could also be stated (Codisjoint on f) a b