Order homomorphisms #

This file defines order homomorphisms, which are bundled monotone functions. A preorder homomorphism f : α →o β→o β is a function α → β→ β along with a proof that ∀ x y, x ≤ y → f x ≤ f y∀ x y, x ≤ y → f x ≤ f y≤ y → f x ≤ f y→ f x ≤ f y≤ f y.

Main definitions #

In this file we define the following bundled monotone maps:

OrderHom α β a.k.a. α →o β→o β: Preorder homomorphism. An OrderHom α β is a function f : α → β→ β such that a₁ ≤ a₂ → f a₁ ≤ f a₂≤ a₂ → f a₁ ≤ f a₂→ f a₁ ≤ f a₂≤ f a₂
OrderEmbedding α β a.k.a. α ↪o β↪o β: Relation embedding. An OrderEmbedding α β is an embedding f : α ↪ β↪ β such that a ≤ b ↔ f a ≤ f b≤ b ↔ f a ≤ f b↔ f a ≤ f b≤ 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≤ b ↔ f a ≤ f b↔ f a ≤ f b≤ 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 α→o α;
OrderHom.curry: an order isomorphism between α × β →o γ× β →o γ→o γ and α →o β →o γ→o β →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 β→o β and α →o γ→o γ into α →o β × γ→o β × γ× γ;
OrderHom.prodₘ: a more bundled version of OrderHom.prod;
OrderHom.prodIso: order isomorphism between α →o β × γ→o β × γ× γ and (α →o β) × (α →o γ)→o β) × (α →o γ)× (α →o γ)→o γ);
OrderHom.diag: diagonal embedding of α into α × α× α as a bundled monotone map;
OrderHom.onDiag: restrict a monotone map α →o α →o β→o α →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 a OrderHom at a point as a bundled monotone map;
OrderHom.pi: combine a family of monotone maps f i : α →o π i→o π i into a monotone map α →o Π i, π i→o Π i, π i;
OrderHom.piIso: order isomorphism between α →o Π i, π i→o Π i, π i and Π i, α →o π i→o π i;
OrderHom.subtype.val: embedding Subtype.val : Subtype p → α→ α as a bundled monotone map;
OrderHom.dual: reinterpret a monotone map α →o β→o β as a monotone map αᵒᵈ →o βᵒᵈ→o βᵒᵈ;
OrderHom.dualIso: order isomorphism between α →o β→o β and (αᵒᵈ →o βᵒᵈ)ᵒᵈ→o βᵒᵈ)ᵒᵈ;
OrderHom.compl: order isomorphism α ≃o αᵒᵈ≃o αᵒᵈ given by taking complements in a boolean algebra;

We also define two functions to convert other bundled maps to α →o β→o β:

OrderEmbedding.toOrderHom: convert α ↪o β↪o β to α →o β→o β;
RelHom.toOrderHom: convert a RelHom between strict orders to an OrderHom.

Tags #

monotone map, bundled morphism