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. An OrderHom α β is a function f : α → β such that a₁ ≤ a₂ → f a₁ ≤ f a₂
OrderEmbedding α β a.k.a. α ↪o β: Relation embedding. An OrderEmbedding α β is an embedding f : α ↪ β such that a ≤ b ↔ f a ≤ f b. Defined as an abbreviation of @RelEmbedding α β (≤) (≤).
OrderIso: Relation isomorphism. An OrderIso α β is an equivalence f : α ≃ β such that a ≤ b ↔ f a ≤ f b. Defined as an abbreviation of @RelIso α β (≤) (≤).

We also define many OrderHoms. 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 of OrderHom.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: projection Prod.fst : α × β → α as a bundled monotone map;
OrderHom.snd: projection Prod.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 point Function.eval i as a bundled monotone map;
OrderHom.coeFnHom: coercion to function as a bundled monotone map;
OrderHom.apply: application of an OrderHom at a point as a bundled monotone map;
OrderHom.pi: combine a family of monotone maps f 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: embedding Subtype.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 a RelHom between strict orders to an OrderHom.

Tags #

monotone map, bundled morphism