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 (≤) (≤)
.
Instances For
- 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
An order isomorphism respects
≤
.
OrderIsoClass F α β
states that F
is a type of order isomorphisms.
You should extend this class when you extend OrderIso
.
Instances
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 β
.
Instances For
Any type satisfying OrderIsoClass
can be cast into OrderIso
via
OrderIsoClass.toOrderIso
.
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 β
.
Instances For
Any type satisfying OrderHomClass
can be cast into OrderHom
via
OrderHomClass.toOrderHom
.
The identity function as bundled monotone function.
Instances For
Evaluation of an unbundled function at a point (Function.eval
) as an OrderHom
.
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
.
Instances For
Subtype.val
as a bundled monotone function.
Instances For
Subtype.impEmbedding
as an order embedding.
Instances For
There is a unique monotone map from a subsingleton to itself.
Embeddings of partial orders that preserve <
also preserve ≤
.
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
.
Instances For
A strictly monotone map from a linear order is an order embedding.
Instances For
Embedding of a subtype into the ambient type as an OrderEmbedding
.
Instances For
Convert an OrderEmbedding
to an OrderHom
.
Instances For
A bundled expression of the fact that a map between partial orders that is strictly monotone is weakly monotone.
Instances For
Converts a RelIso (<) (<)
into an OrderIso
.
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
.
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
Instances For
A strictly monotone function with a right inverse is an order isomorphism.
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
Taking the dual then adding ⊥
is the same as adding ⊤
then taking the dual.
This is the order iso form of WithBot.ofDual
, as proven by coe_toDualTopEquiv_eq
.
Instances For
Taking the dual then adding ⊤
is the same as adding ⊥
then taking the dual.
This is the order iso form of WithTop.ofDual
, as proven by coe_toDualBotEquiv_eq
.
Instances For
A version of Equiv.optionCongr
for WithTop
.
Instances For
A version of Equiv.optionCongr
for WithBot
.