Lattice structure on order homomorphisms

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

Main definitions

• OrderHom.instCompleteLattice: if β is a complete lattice, so is α →o β

Tags

monotone map, bundled morphism

@[instance_reducible]

instance OrderHom.instMax {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeSup β] : Max (α →o β)

Equations

• OrderHom.instMax = { max := fun (f g : α →o β) => { toFun := fun (a : α) => f a ⊔ g a, monotone' := ⋯ } }

@[simp]

theorem OrderHom.coe_sup {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeSup β] (f g : α →o β) : ⇑(f ⊔ g) = ⇑f ⊔ ⇑g

@[instance_reducible]

instance OrderHom.instSemilatticeSup {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeSup β] : SemilatticeSup (α →o β)

Equations

• OrderHom.instSemilatticeSup = { toPartialOrder := OrderHom.instPartialOrder, sup := max, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }

@[instance_reducible]

instance OrderHom.instMin {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] : Min (α →o β)

Equations

• OrderHom.instMin = { min := fun (f g : α →o β) => { toFun := fun (a : α) => f a ⊓ g a, monotone' := ⋯ } }

@[simp]

theorem OrderHom.coe_inf {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] (f g : α →o β) : ⇑(f ⊓ g) = ⇑f ⊓ ⇑g

@[instance_reducible]

instance OrderHom.instSemilatticeInf {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] : SemilatticeInf (α →o β)

Equations

• OrderHom.instSemilatticeInf = { toPartialOrder := OrderHom.instPartialOrder, inf := fun (x1 x2 : α →o β) => x1 ⊓ x2, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[instance_reducible]

instance OrderHom.lattice {α : Type u_1} {β : Type u_2} [Preorder α] [Lattice β] : Lattice (α →o β)

Equations

• OrderHom.lattice = { toSemilatticeSup := OrderHom.instSemilatticeSup, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[instance_reducible]

instance OrderHom.instBotOfOrderBot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] : Bot (α →o β)

Equations

• OrderHom.instBotOfOrderBot = { bot := (OrderHom.const α) ⊥ }

@[simp]

theorem OrderHom.bot_def {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] : ⊥ = (const α) ⊥

@[instance_reducible]

instance OrderHom.orderBot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] : OrderBot (α →o β)

Equations

• OrderHom.orderBot = { toBot := OrderHom.instBotOfOrderBot, bot_le := ⋯ }

@[instance_reducible]

instance OrderHom.instTopOrderHom {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] : Top (α →o β)

Equations

• OrderHom.instTopOrderHom = { top := (OrderHom.const α) ⊤ }

@[simp]

theorem OrderHom.top_def {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] : ⊤ = (const α) ⊤

@[instance_reducible]

instance OrderHom.orderTop {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] : OrderTop (α →o β)

Equations

• OrderHom.orderTop = { toTop := OrderHom.instTopOrderHom, le_top := ⋯ }

@[instance_reducible]

instance OrderHom.instInfSet {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] : InfSet (α →o β)

Equations

• OrderHom.instInfSet = { sInf := fun (s : Set (α →o β)) => { toFun := fun (x : α) => ⨅ f ∈ s, f x, monotone' := ⋯ } }

@[simp]

theorem OrderHom.sInf_apply {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] (s : Set (α →o β)) (x : α) : (sInf s) x = ⨅ f ∈ s, f x

theorem OrderHom.iInf_apply {α : Type u_1} {β : Type u_2} [Preorder α] {ι : Sort u_3} [CompleteLattice β] (f : ι → α →o β) (x : α) : (⨅ (i : ι), f i) x = ⨅ (i : ι), (f i) x

@[simp]

theorem OrderHom.coe_iInf {α : Type u_1} {β : Type u_2} [Preorder α] {ι : Sort u_3} [CompleteLattice β] (f : ι → α →o β) : ⇑(⨅ (i : ι), f i) = ⨅ (i : ι), ⇑(f i)

@[instance_reducible]

instance OrderHom.instSupSet {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] : SupSet (α →o β)

Equations

• OrderHom.instSupSet = { sSup := fun (s : Set (α →o β)) => { toFun := fun (x : α) => ⨆ f ∈ s, f x, monotone' := ⋯ } }

@[simp]

theorem OrderHom.sSup_apply {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] (s : Set (α →o β)) (x : α) : (sSup s) x = ⨆ f ∈ s, f x

theorem OrderHom.iSup_apply {α : Type u_1} {β : Type u_2} [Preorder α] {ι : Sort u_3} [CompleteLattice β] (f : ι → α →o β) (x : α) : (⨆ (i : ι), f i) x = ⨆ (i : ι), (f i) x

@[simp]

theorem OrderHom.coe_iSup {α : Type u_1} {β : Type u_2} [Preorder α] {ι : Sort u_3} [CompleteLattice β] (f : ι → α →o β) : ⇑(⨆ (i : ι), f i) = ⨆ (i : ι), ⇑(f i)

@[instance_reducible]

instance OrderHom.instCompleteLattice {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] : CompleteLattice (α →o β)

Equations

• One or more equations did not get rendered due to their size.

theorem OrderHom.iterate_sup_le_sup_iff {α : Type u_3} [SemilatticeSup α] (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₂