Lattice structure on order homomorphisms

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

Main definitions

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

Tags

monotone map, bundled morphism

ink

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

Equations

• OrderHom.instSupOrderHomToPreorderToPartialOrder = { sup := fun f g => { toFun := fun a => ↑f a ⊔ ↑g a, monotone' := (_ : Monotone (↑f ⊔ fun a => ↑g a)) } }

ink

@[simp]

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

ink

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

Equations

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

ink

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

Equations

• OrderHom.instInfOrderHomToPreorderToPartialOrder = { inf := fun f g => { toFun := fun a => ↑f a ⊓ ↑g a, monotone' := (_ : Monotone (↑f ⊓ fun a => ↑g a)) } }

ink

@[simp]

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

ink

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

Equations

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

ink

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

Equations

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

ink

@[simp]

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

ink

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

Equations

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

ink

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

Equations

• OrderHom.orderBot = OrderBot.mk (_ : ∀ (x : α →o β) (x_1 : α), ⊥ ≤ ↑x x_1)

ink

@[simp]

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

ink

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

Equations

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

ink

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

Equations

• OrderHom.orderTop = OrderTop.mk (_ : ∀ (x : α →o β) (x_1 : α), ↑x x_1 ≤ ⊤)

ink

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

Equations

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

ink

@[simp]

theorem OrderHom.infₛ_apply {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : CompleteLattice β] (s : Set (α →o β)) (x : α) : ↑(infₛ s) x = ⨅ f, ⨅ h, ↑f x

ink

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

ink

@[simp]

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

ink

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

Equations

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

ink

@[simp]

theorem OrderHom.supₛ_apply {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : CompleteLattice β] (s : Set (α →o β)) (x : α) : ↑(supₛ s) x = ⨆ f, ⨆ h, ↑f x

ink

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

ink

@[simp]

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

ink

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

Equations

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

ink

theorem OrderHom.iterate_sup_le_sup_iff {α : Type u_1} [inst : 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₂