mathlib documentation

order.preorder_hom

Preorder homomorphisms #

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

Main definitions #

In this file we define preorder_hom α β a.k.a. α →ₘ β to be a bundled monotone map.

We also define many preorder_homs. In some cases we define two versions, one with suffix and one without it (e.g., preorder_hom.compₘ and preorder_hom.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.

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

Tags #

monotone map, bundled morphism

structure preorder_hom (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :
Type (max u_1 u_2)

Bundled monotone (aka, increasing) function

@[instance]
def preorder_hom.has_coe_to_fun {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
Equations
theorem preorder_hom.monotone {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →ₘ β) :
theorem preorder_hom.mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →ₘ β) :
@[simp]
theorem preorder_hom.to_fun_eq_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α →ₘ β} :
@[simp]
theorem preorder_hom.coe_fun_mk {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :
{to_fun := f, monotone' := hf} = f
@[ext]
theorem preorder_hom.ext {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f g : α →ₘ β) (h : f = g) :
f = g
@[instance]
def preorder_hom.can_lift {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
can_lift (α → β) →ₘ β)

One can lift an unbundled monotone function to a bundled one.

Equations
def preorder_hom.id {α : Type u_1} [preorder α] :
α →ₘ α

The identity function as bundled monotone function.

Equations
@[simp]
theorem preorder_hom.id_coe {α : Type u_1} [preorder α] :
@[instance]
def preorder_hom.inhabited {α : Type u_1} [preorder α] :
Equations
@[instance]
def preorder_hom.preorder {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

The preorder structure of α →ₘ β is pointwise inequality: f ≤ g ↔ ∀ a, f a ≤ g a.

Equations
@[instance]
def preorder_hom.partial_order {α : Type u_1} [preorder α] {β : Type u_2} [partial_order β] :
Equations
theorem preorder_hom.le_def {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α →ₘ β} :
f g ∀ (x : α), f x g x
@[simp]
theorem preorder_hom.coe_le_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α →ₘ β} :
f g f g
@[simp]
theorem preorder_hom.mk_le_mk {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α → β} {hf : monotone f} {hg : monotone g} :
{to_fun := f, monotone' := hf} {to_fun := g, monotone' := hg} f g
theorem preorder_hom.apply_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f g : α →ₘ β} {x y : α} (h₁ : f g) (h₂ : x y) :
f x g y
def preorder_hom.curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] :
× β →ₘ γ) ≃o →ₘ β →ₘ γ)

Curry/uncurry as an order isomorphism between α × β →ₘ γ and α →ₘ β →ₘ γ.

Equations
@[simp]
theorem preorder_hom.curry_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α × β →ₘ γ) (x : α) (y : β) :
@[simp]
theorem preorder_hom.curry_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →ₘ β →ₘ γ) (x : α × β) :
@[simp]
theorem preorder_hom.comp_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (g : β →ₘ γ) (f : α →ₘ β) :
(g.comp f) = g f
def preorder_hom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (g : β →ₘ γ) (f : α →ₘ β) :
α →ₘ γ

The composition of two bundled monotone functions.

Equations
theorem preorder_hom.comp_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] ⦃g₁ g₂ : β →ₘ γ⦄ (hg : g₁ g₂) ⦃f₁ f₂ : α →ₘ β⦄ (hf : f₁ f₂) :
g₁.comp f₁ g₂.comp f₂
@[simp]
theorem preorder_hom.compₘ_coe_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (x : β →ₘ γ) (ᾰ : α →ₘ β) :
def preorder_hom.compₘ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] :
→ₘ γ) →ₘ →ₘ β) →ₘ α →ₘ γ

The composition of two bundled monotone functions, a fully bundled version.

Equations
@[simp]
theorem preorder_hom.comp_id {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →ₘ β) :
@[simp]
theorem preorder_hom.id_comp {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →ₘ β) :
@[simp]
theorem preorder_hom.const_coe_coe (α : Type u_1) [preorder α] {β : Type u_2} [preorder β] (b : β) :
def preorder_hom.const (α : Type u_1) [preorder α] {β : Type u_2} [preorder β] :
β →ₘ α →ₘ β

Constant function bundled as a preorder_hom.

Equations
@[simp]
theorem preorder_hom.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →ₘ β) (c : γ) :
@[simp]
theorem preorder_hom.comp_const {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (γ : Type u_3) [preorder γ] (f : α →ₘ β) (c : α) :
def preorder_hom.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →ₘ β) (g : α →ₘ γ) :
α →ₘ β × γ

Given two bundled monotone maps f, g, f.prod g is the map x ↦ (f x, g x) bundled as a preorder_hom.

Equations
@[simp]
theorem preorder_hom.prod_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →ₘ β) (g : α →ₘ γ) (x : α) :
(f.prod g) x = (f x, g x)
theorem preorder_hom.prod_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] {f₁ f₂ : α →ₘ β} (hf : f₁ f₂) {g₁ g₂ : α →ₘ γ} (hg : g₁ g₂) :
f₁.prod g₁ f₂.prod g₂
theorem preorder_hom.comp_prod_comp_same {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f₁ f₂ : β →ₘ γ) (g : α →ₘ β) :
(f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g
@[simp]
theorem preorder_hom.prodₘ_coe_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (x : α →ₘ β) (ᾰ : α →ₘ γ) (x_1 : α) :
((preorder_hom.prodₘ x) ᾰ) x_1 = (x x_1, ᾰ x_1)
def preorder_hom.prodₘ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] :
→ₘ β) →ₘ →ₘ γ) →ₘ α →ₘ β × γ

Given two bundled monotone maps f, g, f.prod g is the map x ↦ (f x, g x) bundled as a preorder_hom. This is a fully bundled version.

Equations
def preorder_hom.diag {α : Type u_1} [preorder α] :
α →ₘ α × α

Diagonal embedding of α into α × α as a preorder_hom.

Equations
@[simp]
theorem preorder_hom.diag_coe {α : Type u_1} [preorder α] (x : α) :
def preorder_hom.on_diag {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →ₘ α →ₘ β) :
α →ₘ β

Restriction of f : α →ₘ α →ₘ β to the diagonal.

Equations
@[simp]
theorem preorder_hom.on_diag_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →ₘ α →ₘ β) (ᾰ : α) :
(f.on_diag) ᾰ = (f ᾰ)
def preorder_hom.fst {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
α × β →ₘ α

prod.fst as a preorder_hom.

Equations
@[simp]
theorem preorder_hom.fst_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (self : α × β) :
def preorder_hom.snd {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
α × β →ₘ β

prod.snd as a preorder_hom.

Equations
@[simp]
theorem preorder_hom.snd_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (self : α × β) :
@[simp]
theorem preorder_hom.fst_prod_snd {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
@[simp]
theorem preorder_hom.fst_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →ₘ β) (g : α →ₘ γ) :
@[simp]
theorem preorder_hom.snd_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →ₘ β) (g : α →ₘ γ) :
@[simp]
theorem preorder_hom.prod_iso_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →ₘ β × γ) :
def preorder_hom.prod_iso {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] :
→ₘ β × γ) ≃o →ₘ β) × →ₘ γ)

Order isomorphism between the space of monotone maps to β × γ and the product of the spaces of monotone maps to β and γ.

Equations
@[simp]
theorem preorder_hom.prod_iso_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : →ₘ β) × →ₘ γ)) :
@[simp]
theorem preorder_hom.prod_map_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [preorder α] [preorder β] [preorder γ] [preorder δ] (f : α →ₘ β) (g : γ →ₘ δ) (x : α × γ) :
def preorder_hom.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [preorder α] [preorder β] [preorder γ] [preorder δ] (f : α →ₘ β) (g : γ →ₘ δ) :
α × γ →ₘ β × δ

prod.map of two preorder_homs as a preorder_hom.

Equations
def pi.eval_preorder_hom {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), preorder («π» i)] (i : ι) :
(Π (j : ι), «π» j) →ₘ «π» i

Evaluation of an unbundled function at a point (function.eval) as a preorder_hom.

Equations
@[simp]
theorem pi.eval_preorder_hom_coe {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), preorder («π» i)] (i : ι) :
def preorder_hom.coe_fn_hom {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
→ₘ β) →ₘ α → β

The "forgetful functor" from α →ₘ β to α → β that takes the underlying function, is monotone.

Equations
@[simp]
theorem preorder_hom.coe_fn_hom_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
@[simp]
theorem preorder_hom.apply_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (x : α) :
def preorder_hom.apply {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (x : α) :
→ₘ β) →ₘ β

Function application λ f, f a (for fixed a) is a monotone function from the monotone function space α →ₘ β to β. See also pi.eval_preorder_hom.

Equations
def preorder_hom.pi {α : Type u_1} [preorder α] {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), preorder («π» i)] (f : Π (i : ι), α →ₘ «π» i) :
α →ₘ Π (i : ι), «π» i

Construct a bundled monotone map α →ₘ Π i, π i from a family of monotone maps f i : α →ₘ π i.

Equations
@[simp]
theorem preorder_hom.pi_coe {α : Type u_1} [preorder α] {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), preorder («π» i)] (f : Π (i : ι), α →ₘ «π» i) (x : α) (i : ι) :
(preorder_hom.pi f) x i = (f i) x
def preorder_hom.pi_iso {α : Type u_1} [preorder α] {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), preorder («π» i)] :
→ₘ Π (i : ι), «π» i) ≃o Π (i : ι), α →ₘ «π» i

Order isomorphism between bundled monotone maps α →ₘ Π i, π i and families of bundled monotone maps Π i, α →ₘ π i.

Equations
@[simp]
theorem preorder_hom.pi_iso_symm_apply {α : Type u_1} [preorder α] {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), preorder («π» i)] (f : Π (i : ι), α →ₘ (λ (i : ι), «π» i) i) :
@[simp]
theorem preorder_hom.pi_iso_apply {α : Type u_1} [preorder α] {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), preorder («π» i)] (f : α →ₘ Π (i : ι), «π» i) (i : ι) :
def preorder_hom.subtype.val {α : Type u_1} [preorder α] (p : α → Prop) :

subtype.val as a bundled monotone function.

Equations
@[simp]
theorem preorder_hom.subtype.val_coe {α : Type u_1} [preorder α] (p : α → Prop) :
def preorder_hom.unique {α : Type u_1} [preorder α] [subsingleton α] :
unique →ₘ α)

There is a unique monotone map from a subsingleton to itself.

Equations
theorem preorder_hom.preorder_hom_eq_id {α : Type u_1} [preorder α] [subsingleton α] (g : α →ₘ α) :
def preorder_hom.dual {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

Reinterpret a bundled monotone function as a monotone function between dual orders.

Equations
@[simp]
theorem preorder_hom.dual_symm_apply_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : order_dual α →ₘ order_dual β) (ᾰ : α) :
@[simp]
theorem preorder_hom.dual_apply_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →ₘ β) (ᾰ : order_dual α) :
def preorder_hom.dual_iso (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :

preorder_hom.dual as an order isomorphism.

Equations
@[instance]
def preorder_hom.has_sup {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_sup β] :
has_sup →ₘ β)
Equations
@[simp]
theorem preorder_hom.has_sup_sup_coe {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_sup β] (f g : α →ₘ β) (a : α) :
(f g) a = f a g a
@[simp]
theorem preorder_hom.has_inf_inf_coe {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_inf β] (f g : α →ₘ β) (a : α) :
(f g) a = f a g a
@[instance]
def preorder_hom.has_inf {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_inf β] :
has_inf →ₘ β)
Equations
@[instance]
def preorder_hom.has_bot {α : Type u_1} [preorder α] {β : Type u_2} [order_bot β] :
has_bot →ₘ β)
Equations
@[simp]
theorem preorder_hom.has_bot_bot {α : Type u_1} [preorder α] {β : Type u_2} [order_bot β] :
@[instance]
def preorder_hom.has_top {α : Type u_1} [preorder α] {β : Type u_2} [order_top β] :
has_top →ₘ β)
Equations
@[simp]
theorem preorder_hom.has_top_top {α : Type u_1} [preorder α] {β : Type u_2} [order_top β] :
@[instance]
def preorder_hom.has_Inf {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] :
has_Inf →ₘ β)
Equations
@[simp]
theorem preorder_hom.Inf_apply {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] (s : set →ₘ β)) (x : α) :
(Inf s) x = ⨅ (f : α →ₘ β) (H : f s), f x
theorem preorder_hom.infi_apply {α : Type u_1} [preorder α] {ι : Sort u_2} {β : Type u_3} [complete_lattice β] (f : ι → α →ₘ β) (x : α) :
(⨅ (i : ι), f i) x = ⨅ (i : ι), (f i) x
@[simp]
theorem preorder_hom.coe_infi {α : Type u_1} [preorder α] {ι : Sort u_2} {β : Type u_3} [complete_lattice β] (f : ι → α →ₘ β) :
(⨅ (i : ι), f i) = ⨅ (i : ι), (f i)
@[instance]
def preorder_hom.has_Sup {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] :
has_Sup →ₘ β)
Equations
@[simp]
theorem preorder_hom.Sup_apply {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] (s : set →ₘ β)) (x : α) :
(Sup s) x = ⨆ (f : α →ₘ β) (H : f s), f x
theorem preorder_hom.supr_apply {α : Type u_1} [preorder α] {ι : Sort u_2} {β : Type u_3} [complete_lattice β] (f : ι → α →ₘ β) (x : α) :
(⨆ (i : ι), f i) x = ⨆ (i : ι), (f i) x
@[simp]
theorem preorder_hom.coe_supr {α : Type u_1} [preorder α] {ι : Sort u_2} {β : Type u_3} [complete_lattice β] (f : ι → α →ₘ β) :
(⨆ (i : ι), f i) = ⨆ (i : ι), (f i)
theorem preorder_hom.iterate_sup_le_sup_iff {α : Type u_1} [semilattice_sup α] (f : α →ₘ α) :
(∀ (n₁ n₂ : ) (a₁ a₂ : α), f^[n₁ + n₂] (a₁ a₂) f^[n₁] a₁ f^[n₂] a₂) ∀ (a₁ a₂ : α), f (a₁ a₂) f a₁ a₂
@[simp]
theorem order_embedding.to_preorder_hom_coe {X : Type u_1} {Y : Type u_2} [preorder X] [preorder Y] (f : X ↪o Y) :
def order_embedding.to_preorder_hom {X : Type u_1} {Y : Type u_2} [preorder X] [preorder Y] (f : X ↪o Y) :
X →ₘ Y

Convert an order_embedding to a preorder_hom.

Equations
@[simp]
theorem rel_hom.to_preorder_hom_coe {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] (f : has_lt.lt →r has_lt.lt) :
def rel_hom.to_preorder_hom {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] (f : has_lt.lt →r has_lt.lt) :
α →ₘ β

A bundled expression of the fact that a map between partial orders that is strictly monotone is weakly monotone.

Equations