Lattice structure on order homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the lattice structure on order homomorphisms, which are bundled monotone functions.

Main definitions #

order_hom.complete_lattice: if β is a complete lattice, so is α →o β

Tags #

monotone map, bundled morphism

source

@[protected, instance]

def order_hom.has_sup {α : Type u_1} {β : Type u_2} [preorder α] [semilattice_sup β] :

has_sup (α →o β)

Equations

order_hom.has_sup = {sup := λ (f g : α →o β), {to_fun := λ (a : α), ⇑f a ⊔ ⇑g a, monotone' := _}}

source

@[simp]

theorem order_hom.has_sup_sup_coe {α : Type u_1} {β : Type u_2} [preorder α] [semilattice_sup β] (f g : α →o β) (a : α) :

⇑(f ⊔ g) a = ⇑f a ⊔ ⇑g a

source

@[protected, instance]

def order_hom.semilattice_sup {α : Type u_1} {β : Type u_2} [preorder α] [semilattice_sup β] :

semilattice_sup (α →o β)

Equations

order_hom.semilattice_sup = {sup := has_sup.sup order_hom.has_sup, le := partial_order.le order_hom.partial_order, lt := partial_order.lt order_hom.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[simp]

theorem order_hom.has_inf_inf_coe {α : Type u_1} {β : Type u_2} [preorder α] [semilattice_inf β] (f g : α →o β) (a : α) :

⇑(f ⊓ g) a = ⇑f a ⊓ ⇑g a

source

@[protected, instance]

def order_hom.has_inf {α : Type u_1} {β : Type u_2} [preorder α] [semilattice_inf β] :

has_inf (α →o β)

Equations

order_hom.has_inf = {inf := λ (f g : α →o β), {to_fun := λ (a : α), ⇑f a ⊓ ⇑g a, monotone' := _}}

source

@[protected, instance]

def order_hom.semilattice_inf {α : Type u_1} {β : Type u_2} [preorder α] [semilattice_inf β] :

semilattice_inf (α →o β)

Equations

order_hom.semilattice_inf = {inf := has_inf.inf order_hom.has_inf, le := partial_order.le order_hom.partial_order, lt := partial_order.lt order_hom.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

def order_hom.lattice {α : Type u_1} {β : Type u_2} [preorder α] [lattice β] :

lattice (α →o β)

Equations

order_hom.lattice = {sup := semilattice_sup.sup order_hom.semilattice_sup, le := semilattice_sup.le order_hom.semilattice_sup, lt := semilattice_sup.lt order_hom.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf order_hom.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

def order_hom.has_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_bot β] :

has_bot (α →o β)

Equations

order_hom.has_bot = {bot := ⇑(order_hom.const α) ⊥}

source

@[simp]

theorem order_hom.has_bot_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_bot β] :

⊥ = ⇑(order_hom.const α) ⊥

source

@[protected, instance]

def order_hom.order_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_bot β] :

order_bot (α →o β)

Equations

order_hom.order_bot = {bot := ⊥, bot_le := _}

source

@[simp]

theorem order_hom.has_top_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top β] :

⊤ = ⇑(order_hom.const α) ⊤

source

@[protected, instance]

def order_hom.has_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top β] :

has_top (α →o β)

Equations

order_hom.has_top = {top := ⇑(order_hom.const α) ⊤}

source

@[protected, instance]

def order_hom.order_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top β] :

order_top (α →o β)

Equations

order_hom.order_top = {top := ⊤, le_top := _}

source

@[protected, instance]

def order_hom.has_Inf {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] :

has_Inf (α →o β)

Equations

order_hom.has_Inf = {Inf := λ (s : set (α →o β)), {to_fun := λ (x : α), ⨅ (f : α →o β) (H : f ∈ s), ⇑f x, monotone' := _}}

source

@[simp]

theorem order_hom.Inf_apply {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] (s : set (α →o β)) (x : α) :

⇑(has_Inf.Inf s) x = ⨅ (f : α →o β) (H : f ∈ s), ⇑f x

source

theorem order_hom.infi_apply {α : Type u_1} {β : Type u_2} [preorder α] {ι : Sort u_3} [complete_lattice β] (f : ι → α →o β) (x : α) :

(⇑⨅ (i : ι), f i) x = ⨅ (i : ι), ⇑(f i) x

source

@[simp, norm_cast]

theorem order_hom.coe_infi {α : Type u_1} {β : Type u_2} [preorder α] {ι : Sort u_3} [complete_lattice β] (f : ι → α →o β) :

(⇑⨅ (i : ι), f i) = ⨅ (i : ι), ⇑(f i)

source

@[protected, instance]

def order_hom.has_Sup {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] :

has_Sup (α →o β)

Equations

order_hom.has_Sup = {Sup := λ (s : set (α →o β)), {to_fun := λ (x : α), ⨆ (f : α →o β) (H : f ∈ s), ⇑f x, monotone' := _}}

source

@[simp]

theorem order_hom.Sup_apply {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] (s : set (α →o β)) (x : α) :

⇑(has_Sup.Sup s) x = ⨆ (f : α →o β) (H : f ∈ s), ⇑f x

source

theorem order_hom.supr_apply {α : Type u_1} {β : Type u_2} [preorder α] {ι : Sort u_3} [complete_lattice β] (f : ι → α →o β) (x : α) :

(⇑⨆ (i : ι), f i) x = ⨆ (i : ι), ⇑(f i) x

source

@[simp, norm_cast]

theorem order_hom.coe_supr {α : Type u_1} {β : Type u_2} [preorder α] {ι : Sort u_3} [complete_lattice β] (f : ι → α →o β) :

(⇑⨆ (i : ι), f i) = ⨆ (i : ι), ⇑(f i)

source

@[protected, instance]

def order_hom.complete_lattice {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] :

complete_lattice (α →o β)

Equations

order_hom.complete_lattice = {sup := lattice.sup order_hom.lattice, le := lattice.le order_hom.lattice, lt := lattice.lt order_hom.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf order_hom.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup order_hom.has_Sup, le_Sup := _, Sup_le := _, Inf := has_Inf.Inf order_hom.has_Inf, Inf_le := _, le_Inf := _, top := order_top.top order_hom.order_top, bot := order_bot.bot order_hom.order_bot, le_top := _, bot_le := _}

source

theorem order_hom.iterate_sup_le_sup_iff {α : Type u_1} [semilattice_sup α] (f : α →o α) :

(∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), ⇑f^[n₁ + n₂] (a₁ ⊔ a₂) ≤ ⇑f^[n₁] a₁ ⊔ ⇑f^[n₂] a₂) ↔ ∀ (a₁ a₂ : α), ⇑f (a₁ ⊔ a₂) ≤ ⇑f a₁ ⊔ a₂