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
Notation for an OrderHom
.
Equations
- «term_→o_» = Lean.ParserDescr.trailingNode `term_→o_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →o ") (Lean.ParserDescr.cat `term 25))
Instances For
An order embedding is an embedding f : α ↪ β
such that a ≤ b ↔ (f a) ≤ (f b)
.
This definition is an abbreviation of RelEmbedding (≤) (≤)
.
Instances For
Notation for an OrderEmbedding
.
Equations
- «term_↪o_» = Lean.ParserDescr.trailingNode `term_↪o_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↪o ") (Lean.ParserDescr.cat `term 26))
Instances For
An order isomorphism is an equivalence such that a ≤ b ↔ (f a) ≤ (f b)
.
This definition is an abbreviation of RelIso (≤) (≤)
.
Instances For
Notation for an OrderIso
.
Equations
- «term_≃o_» = Lean.ParserDescr.trailingNode `term_≃o_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃o ") (Lean.ParserDescr.cat `term 26))
Instances For
OrderHomClass F α b
asserts that F
is a type of ≤
-preserving morphisms.
Equations
- OrderHomClass F α β = RelHomClass F (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : β) => x1 ≤ x2
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
- ↑f = { toEquiv := ↑f, map_rel_iff' := ⋯ }
Instances For
Any type satisfying OrderIsoClass
can be cast into OrderIso
via
OrderIsoClass.toOrderIso
.
Equations
- instCoeTCOrderIsoOfOrderIsoClass = { coe := 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
- ↑f = { toFun := ⇑f, monotone' := ⋯ }
Instances For
Any type satisfying OrderHomClass
can be cast into OrderHom
via
OrderHomClass.toOrderHom
.
Equations
- OrderHomClass.instCoeTCOrderHom = { coe := OrderHomClass.toOrderHom }
Equations
- ⋯ = ⋯
See Note [custom simps projection]. We give this manually so that we use toFun
as the
projection directly instead.
Equations
- OrderHom.Simps.coe f = ⇑f
Instances For
The preorder structure of α →o β
is pointwise inequality: f ≤ g ↔ ∀ a, f a ≤ g a
.
Equations
- OrderHom.instPreorder = Preorder.lift OrderHom.toFun
Equations
- OrderHom.instPartialOrder = PartialOrder.lift OrderHom.toFun ⋯
Constant function bundled as an OrderHom
.
Equations
- OrderHom.const α = { toFun := fun (b : β) => { toFun := Function.const α b, monotone' := ⋯ }, monotone' := ⋯ }
Instances For
Given two bundled monotone maps f
, g
, f.prod g
is the map x ↦ (f x, g x)
bundled as a
OrderHom
.
Equations
- f.prod g = { toFun := fun (x : α) => (f x, g x), monotone' := ⋯ }
Instances For
Order isomorphism between the space of monotone maps to β × γ
and the product of the spaces
of monotone maps to β
and γ
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluation of an unbundled function at a point (Function.eval
) as an OrderHom
.
Equations
- Pi.evalOrderHom i = { toFun := Function.eval i, monotone' := ⋯ }
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
- OrderHom.apply x = (Pi.evalOrderHom x).comp OrderHom.coeFnHom
Instances For
Construct a bundled monotone map α →o Π i, π i
from a family of monotone maps
f i : α →o π i
.
Equations
- OrderHom.pi f = { toFun := fun (x : α) (i : ι) => (f i) x, monotone' := ⋯ }
Instances For
Order isomorphism between bundled monotone maps α →o Π i, π i
and families of bundled monotone
maps Π i, α →o π i
.
Equations
- OrderHom.piIso = { toFun := fun (f : α →o (i : ι) → π i) (i : ι) => (Pi.evalOrderHom i).comp f, invFun := OrderHom.pi, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
Instances For
Subtype.val
as a bundled monotone function.
Equations
- OrderHom.Subtype.val p = { toFun := Subtype.val, monotone' := ⋯ }
Instances For
Subtype.impEmbedding
as an order embedding.
Equations
- Subtype.orderEmbedding h = { toEmbedding := Subtype.impEmbedding p q h, map_rel_iff' := ⋯ }
Instances For
There is a unique monotone map from a subsingleton to itself.
Equations
- OrderHom.unique = { default := OrderHom.id, uniq := ⋯ }
OrderHom.dual
as an order isomorphism.
Equations
- OrderHom.dualIso α β = { toEquiv := OrderHom.dual.trans OrderDual.toDual, map_rel_iff' := ⋯ }
Instances For
Embeddings of partial orders that preserve <
also preserve ≤
.
Equations
- f.orderEmbeddingOfLTEmbedding = { toEmbedding := f.toEmbedding, map_rel_iff' := ⋯ }
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.
A version of WithBot.map
for order embeddings.
Equations
- f.withBotMap = { toFun := WithBot.map ⇑f, inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
A version of WithTop.map
for order embeddings.
Equations
- f.withTopMap = { toFun := WithTop.map ⇑f, inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
Coercion α → WithBot α
as an OrderEmbedding
.
Equations
- OrderEmbedding.withBotCoe = { toFun := WithBot.some, inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
Coercion α → WithTop α
as an OrderEmbedding
.
Equations
- OrderEmbedding.withTopCoe = { toFun := WithTop.some, inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
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
Embedding of a subtype into the ambient type as an OrderEmbedding
.
Equations
- OrderEmbedding.subtype p = { toEmbedding := Function.Embedding.subtype p, map_rel_iff' := ⋯ }
Instances For
The trivial embedding from an empty preorder to another preorder
Equations
- OrderEmbedding.ofIsEmpty = { toFun := fun (a : α) => isEmptyElim a, inj' := ⋯, map_rel_iff' := ⋯ }
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
- f.toOrderHom = { toFun := ⇑f, monotone' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Reinterpret an order isomorphism as an order embedding.
Equations
- e.toOrderEmbedding = RelIso.toRelEmbedding e
Instances For
Identity order isomorphism.
Equations
- OrderIso.refl α = RelIso.refl fun (x1 x2 : α) => x1 ≤ x2
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
The order isomorphism between a type and its double dual.
Equations
Instances For
Converts a RelIso (<) (<)
into an OrderIso
.
Equations
- OrderIso.ofRelIsoLT e = { toEquiv := e.toEquiv, map_rel_iff' := ⋯ }
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
- OrderIso.ofCmpEqCmp f g h = { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
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
- OrderIso.ofHomInv f g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
Instances For
Order isomorphism between α → β
and β
, where α
has a unique element.
Equations
- OrderIso.funUnique α β = { toEquiv := Equiv.funUnique α β, map_rel_iff' := ⋯ }
Instances For
If e
is an equivalence with monotone forward and inverse maps, then e
is an
order isomorphism.
Equations
- e.toOrderIso h₁ h₂ = { toEquiv := e, map_rel_iff' := ⋯ }
Instances For
A strictly monotone function with a right inverse is an order isomorphism.
Equations
- StrictMono.orderIsoOfRightInverse f h_mono g hg = { toFun := f, invFun := g, left_inv := ⋯, right_inv := hg, map_rel_iff' := ⋯ }
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
.
Equations
- WithBot.toDualTopEquiv = OrderIso.refl (WithBot αᵒᵈ)
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
.
Equations
- WithTop.toDualBotEquiv = OrderIso.refl (WithTop αᵒᵈ)
Instances For
A version of Equiv.optionCongr
for WithTop
.
Equations
- e.withTopCongr = { toEquiv := e.optionCongr, map_rel_iff' := ⋯ }
Instances For
A version of Equiv.optionCongr
for WithBot
.
Equations
- e.withBotCongr = { toEquiv := e.optionCongr, map_rel_iff' := ⋯ }