Bounded order homomorphisms #

This file defines (bounded) order homomorphisms.

We use the DFunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

Types of morphisms #

TopHom: Maps which preserve ⊤.
BotHom: Maps which preserve ⊥.
BoundedOrderHom: Bounded order homomorphisms. Monotone maps which preserve ⊤ and ⊥.

Typeclasses #

source

structure TopHom (α : Type u_6) (β : Type u_7) [Top α] [Top β] :

Type (max u_6 u_7)

The type of ⊤-preserving functions from α to β.

toFun : α → β
The underlying function. The preferred spelling is DFunLike.coe.
map_top' : self.toFun ⊤ = ⊤
The function preserves the top element. The preferred spelling is map_top.

Instances For

source

structure BotHom (α : Type u_6) (β : Type u_7) [Bot α] [Bot β] :

Type (max u_6 u_7)

The type of ⊥-preserving functions from α to β.

toFun : α → β
The underlying function. The preferred spelling is DFunLike.coe.
map_bot' : self.toFun ⊥ = ⊥
The function preserves the bottom element. The preferred spelling is map_bot.

Instances For

source

structure BoundedOrderHom (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] extends OrderHom :

Type (max u_6 u_7)

The type of bounded order homomorphisms from α to β.

toFun : α → β
monotone' : Monotone self.toFun
map_top' : self.toFun ⊤ = ⊤
The function preserves the top element. The preferred spelling is map_top.
map_bot' : self.toFun ⊥ = ⊥
The function preserves the bottom element. The preferred spelling is map_bot.

Instances For

source

class TopHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [Top α] [Top β] [FunLike F α β] :

Prop

TopHomClass F α β states that F is a type of ⊤-preserving morphisms.

You should extend this class when you extend TopHom.

map_top : ∀ (f : F), f ⊤ = ⊤
A TopHomClass morphism preserves the top element.

Instances

source

class BotHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [Bot α] [Bot β] [FunLike F α β] :

Prop

BotHomClass F α β states that F is a type of ⊥-preserving morphisms.

You should extend this class when you extend BotHom.

map_bot : ∀ (f : F), f ⊥ = ⊥
A BotHomClass morphism preserves the bottom element.

Instances

source

class BoundedOrderHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [FunLike F α β] extends RelHomClass :

Prop

BoundedOrderHomClass F α β states that F is a type of bounded order morphisms.

You should extend this class when you extend BoundedOrderHom.

map_rel : ∀ (f : F) {a b : α}, a ≤ b → f a ≤ f b
map_top : ∀ (f : F), f ⊤ = ⊤
Morphisms preserve the top element. The preferred spelling is _root_.map_top.
map_bot : ∀ (f : F), f ⊥ = ⊥
Morphisms preserve the bottom element. The preferred spelling is _root_.map_bot.

Instances

source

instance BoundedOrderHomClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :

TopHomClass F α β

Equations

⋯ = ⋯

source

instance BoundedOrderHomClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :

BotHomClass F α β

Equations

⋯ = ⋯

source

instance OrderIsoClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [LE α] [OrderTop α] [PartialOrder β] [OrderTop β] [OrderIsoClass F α β] :

TopHomClass F α β

Equations

⋯ = ⋯

source

instance OrderIsoClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [LE α] [OrderBot α] [PartialOrder β] [OrderBot β] [OrderIsoClass F α β] :

BotHomClass F α β

Equations

⋯ = ⋯

source

instance OrderIsoClass.toBoundedOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [LE α] [BoundedOrder α] [PartialOrder β] [BoundedOrder β] [OrderIsoClass F α β] :

BoundedOrderHomClass F α β

Equations

⋯ = ⋯

source

@[simp]

theorem map_eq_top_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [LE α] [OrderTop α] [PartialOrder β] [OrderTop β] [OrderIsoClass F α β] (f : F) {a : α} :

f a = ⊤ ↔ a = ⊤

source

@[simp]

theorem map_eq_bot_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [LE α] [OrderBot α] [PartialOrder β] [OrderBot β] [OrderIsoClass F α β] (f : F) {a : α} :

f a = ⊥ ↔ a = ⊥

source

def TopHomClass.toTopHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Top α] [Top β] [TopHomClass F α β] (f : F) :

TopHom α β

Turn an element of a type F satisfying TopHomClass F α β into an actual TopHom. This is declared as the default coercion from F to TopHom α β.

Equations

↑f = { toFun := ⇑f, map_top' := ⋯ }

source

instance instCoeTCTopHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Top α] [Top β] [TopHomClass F α β] :

CoeTC F (TopHom α β)

Equations

instCoeTCTopHom = { coe := TopHomClass.toTopHom }

source

def BotHomClass.toBotHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Bot α] [Bot β] [BotHomClass F α β] (f : F) :

BotHom α β

Turn an element of a type F satisfying BotHomClass F α β into an actual BotHom. This is declared as the default coercion from F to BotHom α β.

Equations

↑f = { toFun := ⇑f, map_bot' := ⋯ }

source

instance instCoeTCBotHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Bot α] [Bot β] [BotHomClass F α β] :

CoeTC F (BotHom α β)

Equations

instCoeTCBotHom = { coe := BotHomClass.toBotHom }

source

def BoundedOrderHomClass.toBoundedOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] (f : F) :

BoundedOrderHom α β

Turn an element of a type F satisfying BoundedOrderHomClass F α β into an actual BoundedOrderHom. This is declared as the default coercion from F to BoundedOrderHom α β.

Equations

↑f = let __src := ↑f; { toOrderHom := { toFun := ⇑f, monotone' := ⋯ }, map_top' := ⋯, map_bot' := ⋯ }

source

instance instCoeTCBoundedOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :

CoeTC F (BoundedOrderHom α β)

Equations

instCoeTCBoundedOrderHom = { coe := BoundedOrderHomClass.toBoundedOrderHom }

Top homomorphisms #

source

instance TopHom.instFunLikeTopHom {α : Type u_2} {β : Type u_3} [Top α] [Top β] :

FunLike (TopHom α β) α β

Equations

TopHom.instFunLikeTopHom = { coe := TopHom.toFun, coe_injective' := ⋯ }

source

instance TopHom.instTopHomClassTopHomInstFunLikeTopHom {α : Type u_2} {β : Type u_3} [Top α] [Top β] :

TopHomClass (TopHom α β) α β

Equations

⋯ = ⋯

source

theorem TopHom.ext {α : Type u_2} {β : Type u_3} [Top α] [Top β] {f : TopHom α β} {g : TopHom α β} (h : ∀ (a : α), f a = g a) :

f = g

source

def TopHom.copy {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) (f' : α → β) (h : f' = ⇑f) :

TopHom α β

Copy of a TopHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

TopHom.copy f f' h = { toFun := f', map_top' := ⋯ }

source

@[simp]

theorem TopHom.coe_copy {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) (f' : α → β) (h : f' = ⇑f) :

⇑(TopHom.copy f f' h) = f'

source

theorem TopHom.copy_eq {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) (f' : α → β) (h : f' = ⇑f) :

TopHom.copy f f' h = f

source

instance TopHom.instInhabitedTopHom {α : Type u_2} {β : Type u_3} [Top α] [Top β] :

Inhabited (TopHom α β)

Equations

TopHom.instInhabitedTopHom = { default := { toFun := fun (x : α) => ⊤, map_top' := ⋯ } }

source

def TopHom.id (α : Type u_2) [Top α] :

TopHom α α

id as a TopHom.

Equations

TopHom.id α = { toFun := id, map_top' := ⋯ }

source

@[simp]

theorem TopHom.coe_id (α : Type u_2) [Top α] :

⇑(TopHom.id α) = id

source

@[simp]

theorem TopHom.id_apply {α : Type u_2} [Top α] (a : α) :

(TopHom.id α) a = a

source

def TopHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [Top γ] (f : TopHom β γ) (g : TopHom α β) :

TopHom α γ

Composition of TopHoms as a TopHom.

Equations

TopHom.comp f g = { toFun := ⇑f ∘ ⇑g, map_top' := ⋯ }

source

@[simp]

theorem TopHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [Top γ] (f : TopHom β γ) (g : TopHom α β) :

⇑(TopHom.comp f g) = ⇑f ∘ ⇑g

source

@[simp]

theorem TopHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [Top γ] (f : TopHom β γ) (g : TopHom α β) (a : α) :

(TopHom.comp f g) a = f (g a)

source

@[simp]

theorem TopHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Top α] [Top β] [Top γ] [Top δ] (f : TopHom γ δ) (g : TopHom β γ) (h : TopHom α β) :

TopHom.comp (TopHom.comp f g) h = TopHom.comp f (TopHom.comp g h)

source

@[simp]

theorem TopHom.comp_id {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) :

TopHom.comp f (TopHom.id α) = f

source

@[simp]

theorem TopHom.id_comp {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) :

TopHom.comp (TopHom.id β) f = f

source

@[simp]

theorem TopHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [Top γ] {g₁ : TopHom β γ} {g₂ : TopHom β γ} {f : TopHom α β} (hf : Function.Surjective ⇑f) :

TopHom.comp g₁ f = TopHom.comp g₂ f ↔ g₁ = g₂

source

@[simp]

theorem TopHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [Top γ] {g : TopHom β γ} {f₁ : TopHom α β} {f₂ : TopHom α β} (hg : Function.Injective ⇑g) :

TopHom.comp g f₁ = TopHom.comp g f₂ ↔ f₁ = f₂

source

instance TopHom.instPreorderTopHom {α : Type u_2} {β : Type u_3} [Top α] [Preorder β] [Top β] :

Preorder (TopHom α β)

Equations

TopHom.instPreorderTopHom = Preorder.lift DFunLike.coe

source

instance TopHom.instPartialOrderTopHom {α : Type u_2} {β : Type u_3} [Top α] [PartialOrder β] [Top β] :

PartialOrder (TopHom α β)

Equations

TopHom.instPartialOrderTopHom = PartialOrder.lift (fun (f : TopHom α β) => ⇑f) ⋯

source

instance TopHom.instOrderTopTopHomToTopToLEToLEInstPreorderTopHom {α : Type u_2} {β : Type u_3} [Top α] [Preorder β] [OrderTop β] :

OrderTop (TopHom α β)

Equations

TopHom.instOrderTopTopHomToTopToLEToLEInstPreorderTopHom = OrderTop.mk ⋯

source

@[simp]

theorem TopHom.coe_top {α : Type u_2} {β : Type u_3} [Top α] [Preorder β] [OrderTop β] :

⇑⊤ = ⊤

source

@[simp]

theorem TopHom.top_apply {α : Type u_2} {β : Type u_3} [Top α] [Preorder β] [OrderTop β] (a : α) :

⊤ a = ⊤

source

instance TopHom.instInfTopHomToTopToLEToPreorderToPartialOrder {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeInf β] [OrderTop β] :

Inf (TopHom α β)

Equations

TopHom.instInfTopHomToTopToLEToPreorderToPartialOrder = { inf := fun (f g : TopHom α β) => { toFun := ⇑f ⊓ ⇑g, map_top' := ⋯ } }

source

instance TopHom.instSemilatticeInfTopHomToTopToLEToPreorderToPartialOrder {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeInf β] [OrderTop β] :

SemilatticeInf (TopHom α β)

Equations

TopHom.instSemilatticeInfTopHomToTopToLEToPreorderToPartialOrder = Function.Injective.semilatticeInf (fun (f : TopHom α β) => ⇑f) ⋯ ⋯

source

@[simp]

theorem TopHom.coe_inf {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeInf β] [OrderTop β] (f : TopHom α β) (g : TopHom α β) :

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

source

@[simp]

theorem TopHom.inf_apply {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeInf β] [OrderTop β] (f : TopHom α β) (g : TopHom α β) (a : α) :

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

source

instance TopHom.instSupTopHomToTopToLEToPreorderToPartialOrder {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeSup β] [OrderTop β] :

Sup (TopHom α β)

Equations

TopHom.instSupTopHomToTopToLEToPreorderToPartialOrder = { sup := fun (f g : TopHom α β) => { toFun := ⇑f ⊔ ⇑g, map_top' := ⋯ } }

source

instance TopHom.instSemilatticeSupTopHomToTopToLEToPreorderToPartialOrder {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeSup β] [OrderTop β] :

SemilatticeSup (TopHom α β)

Equations

TopHom.instSemilatticeSupTopHomToTopToLEToPreorderToPartialOrder = Function.Injective.semilatticeSup (fun (f : TopHom α β) => ⇑f) ⋯ ⋯

source

@[simp]

theorem TopHom.coe_sup {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeSup β] [OrderTop β] (f : TopHom α β) (g : TopHom α β) :

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

source

@[simp]

theorem TopHom.sup_apply {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeSup β] [OrderTop β] (f : TopHom α β) (g : TopHom α β) (a : α) :

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

source

instance TopHom.instLatticeTopHomToTopToLEToPreorderToPartialOrderToSemilatticeInf {α : Type u_2} {β : Type u_3} [Top α] [Lattice β] [OrderTop β] :

Lattice (TopHom α β)

Equations

TopHom.instLatticeTopHomToTopToLEToPreorderToPartialOrderToSemilatticeInf = Function.Injective.lattice (fun (f : TopHom α β) => ⇑f) ⋯ ⋯ ⋯

source

instance TopHom.instDistribLatticeTopHomToTopToLEToPreorderToPartialOrderToSemilatticeInfToLattice {α : Type u_2} {β : Type u_3} [Top α] [DistribLattice β] [OrderTop β] :

DistribLattice (TopHom α β)

Equations

TopHom.instDistribLatticeTopHomToTopToLEToPreorderToPartialOrderToSemilatticeInfToLattice = Function.Injective.distribLattice (fun (f : TopHom α β) => ⇑f) ⋯ ⋯ ⋯

Bot homomorphisms #

source

instance BotHom.instFunLikeBotHom {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] :

FunLike (BotHom α β) α β

Equations

BotHom.instFunLikeBotHom = { coe := BotHom.toFun, coe_injective' := ⋯ }

source

instance BotHom.instBotHomClassBotHomInstFunLikeBotHom {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] :

BotHomClass (BotHom α β) α β

Equations

⋯ = ⋯

source

theorem BotHom.ext {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] {f : BotHom α β} {g : BotHom α β} (h : ∀ (a : α), f a = g a) :

f = g

source

def BotHom.copy {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) (f' : α → β) (h : f' = ⇑f) :

BotHom α β

Copy of a BotHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

BotHom.copy f f' h = { toFun := f', map_bot' := ⋯ }

source

@[simp]

theorem BotHom.coe_copy {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) (f' : α → β) (h : f' = ⇑f) :

⇑(BotHom.copy f f' h) = f'

source

theorem BotHom.copy_eq {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) (f' : α → β) (h : f' = ⇑f) :

BotHom.copy f f' h = f

source

instance BotHom.instInhabitedBotHom {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] :

Inhabited (BotHom α β)

Equations

BotHom.instInhabitedBotHom = { default := { toFun := fun (x : α) => ⊥, map_bot' := ⋯ } }

source

def BotHom.id (α : Type u_2) [Bot α] :

BotHom α α

id as a BotHom.

Equations

BotHom.id α = { toFun := id, map_bot' := ⋯ }

source

@[simp]

theorem BotHom.coe_id (α : Type u_2) [Bot α] :

⇑(BotHom.id α) = id

source

@[simp]

theorem BotHom.id_apply {α : Type u_2} [Bot α] (a : α) :

(BotHom.id α) a = a

source

def BotHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [Bot γ] (f : BotHom β γ) (g : BotHom α β) :

BotHom α γ

Composition of BotHoms as a BotHom.

Equations

BotHom.comp f g = { toFun := ⇑f ∘ ⇑g, map_bot' := ⋯ }

source

@[simp]

theorem BotHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [Bot γ] (f : BotHom β γ) (g : BotHom α β) :

⇑(BotHom.comp f g) = ⇑f ∘ ⇑g

source

@[simp]

theorem BotHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [Bot γ] (f : BotHom β γ) (g : BotHom α β) (a : α) :

(BotHom.comp f g) a = f (g a)

source

@[simp]

theorem BotHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Bot α] [Bot β] [Bot γ] [Bot δ] (f : BotHom γ δ) (g : BotHom β γ) (h : BotHom α β) :

BotHom.comp (BotHom.comp f g) h = BotHom.comp f (BotHom.comp g h)

source

@[simp]

theorem BotHom.comp_id {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) :

BotHom.comp f (BotHom.id α) = f

source

@[simp]

theorem BotHom.id_comp {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) :

BotHom.comp (BotHom.id β) f = f

source

@[simp]

theorem BotHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [Bot γ] {g₁ : BotHom β γ} {g₂ : BotHom β γ} {f : BotHom α β} (hf : Function.Surjective ⇑f) :

BotHom.comp g₁ f = BotHom.comp g₂ f ↔ g₁ = g₂

source

@[simp]

theorem BotHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [Bot γ] {g : BotHom β γ} {f₁ : BotHom α β} {f₂ : BotHom α β} (hg : Function.Injective ⇑g) :

BotHom.comp g f₁ = BotHom.comp g f₂ ↔ f₁ = f₂

source

instance BotHom.instPreorderBotHom {α : Type u_2} {β : Type u_3} [Bot α] [Preorder β] [Bot β] :

Preorder (BotHom α β)

Equations

BotHom.instPreorderBotHom = Preorder.lift DFunLike.coe

source

instance BotHom.instPartialOrderBotHom {α : Type u_2} {β : Type u_3} [Bot α] [PartialOrder β] [Bot β] :

PartialOrder (BotHom α β)

Equations

BotHom.instPartialOrderBotHom = PartialOrder.lift (fun (f : BotHom α β) => ⇑f) ⋯

source

instance BotHom.instOrderBotBotHomToBotToLEToLEInstPreorderBotHom {α : Type u_2} {β : Type u_3} [Bot α] [Preorder β] [OrderBot β] :

OrderBot (BotHom α β)

Equations

BotHom.instOrderBotBotHomToBotToLEToLEInstPreorderBotHom = OrderBot.mk ⋯

source

@[simp]

theorem BotHom.coe_bot {α : Type u_2} {β : Type u_3} [Bot α] [Preorder β] [OrderBot β] :

⇑⊥ = ⊥

source

@[simp]

theorem BotHom.bot_apply {α : Type u_2} {β : Type u_3} [Bot α] [Preorder β] [OrderBot β] (a : α) :

⊥ a = ⊥

source

instance BotHom.instInfBotHomToBotToLEToPreorderToPartialOrder {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeInf β] [OrderBot β] :

Inf (BotHom α β)

Equations

BotHom.instInfBotHomToBotToLEToPreorderToPartialOrder = { inf := fun (f g : BotHom α β) => { toFun := ⇑f ⊓ ⇑g, map_bot' := ⋯ } }

source

instance BotHom.instSemilatticeInfBotHomToBotToLEToPreorderToPartialOrder {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeInf β] [OrderBot β] :

SemilatticeInf (BotHom α β)

Equations

BotHom.instSemilatticeInfBotHomToBotToLEToPreorderToPartialOrder = Function.Injective.semilatticeInf (fun (f : BotHom α β) => ⇑f) ⋯ ⋯

source

@[simp]

theorem BotHom.coe_inf {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeInf β] [OrderBot β] (f : BotHom α β) (g : BotHom α β) :

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

source

@[simp]

theorem BotHom.inf_apply {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeInf β] [OrderBot β] (f : BotHom α β) (g : BotHom α β) (a : α) :

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

source

instance BotHom.instSupBotHomToBotToLEToPreorderToPartialOrder {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeSup β] [OrderBot β] :

Sup (BotHom α β)

Equations

BotHom.instSupBotHomToBotToLEToPreorderToPartialOrder = { sup := fun (f g : BotHom α β) => { toFun := ⇑f ⊔ ⇑g, map_bot' := ⋯ } }

source

instance BotHom.instSemilatticeSupBotHomToBotToLEToPreorderToPartialOrder {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeSup β] [OrderBot β] :

SemilatticeSup (BotHom α β)

Equations

BotHom.instSemilatticeSupBotHomToBotToLEToPreorderToPartialOrder = Function.Injective.semilatticeSup (fun (f : BotHom α β) => ⇑f) ⋯ ⋯

source

@[simp]

theorem BotHom.coe_sup {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeSup β] [OrderBot β] (f : BotHom α β) (g : BotHom α β) :

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

source

@[simp]

theorem BotHom.sup_apply {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeSup β] [OrderBot β] (f : BotHom α β) (g : BotHom α β) (a : α) :

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

source

instance BotHom.instLatticeBotHomToBotToLEToPreorderToPartialOrderToSemilatticeInf {α : Type u_2} {β : Type u_3} [Bot α] [Lattice β] [OrderBot β] :

Lattice (BotHom α β)

Equations

BotHom.instLatticeBotHomToBotToLEToPreorderToPartialOrderToSemilatticeInf = Function.Injective.lattice (fun (f : BotHom α β) => ⇑f) ⋯ ⋯ ⋯

source

instance BotHom.instDistribLatticeBotHomToBotToLEToPreorderToPartialOrderToSemilatticeInfToLattice {α : Type u_2} {β : Type u_3} [Bot α] [DistribLattice β] [OrderBot β] :

DistribLattice (BotHom α β)

Equations

BotHom.instDistribLatticeBotHomToBotToLEToPreorderToPartialOrderToSemilatticeInfToLattice = Function.Injective.distribLattice (fun (f : BotHom α β) => ⇑f) ⋯ ⋯ ⋯

Bounded order homomorphisms #

source

def BoundedOrderHom.toTopHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) :

TopHom α β

Reinterpret a BoundedOrderHom as a TopHom.

Equations

BoundedOrderHom.toTopHom f = { toFun := f.toFun, map_top' := ⋯ }

source

def BoundedOrderHom.toBotHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) :

BotHom α β

Reinterpret a BoundedOrderHom as a BotHom.

Equations

BoundedOrderHom.toBotHom f = { toFun := f.toFun, map_bot' := ⋯ }

source

instance BoundedOrderHom.instFunLikeBoundedOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] :

FunLike (BoundedOrderHom α β) α β

Equations

BoundedOrderHom.instFunLikeBoundedOrderHom = { coe := fun (f : BoundedOrderHom α β) => f.toFun, coe_injective' := ⋯ }

source

instance BoundedOrderHom.instBoundedOrderHomClassBoundedOrderHomToLEToLEInstFunLikeBoundedOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] :

BoundedOrderHomClass (BoundedOrderHom α β) α β

Equations

⋯ = ⋯

source

theorem BoundedOrderHom.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] {f : BoundedOrderHom α β} {g : BoundedOrderHom α β} (h : ∀ (a : α), f a = g a) :

f = g

source

def BoundedOrderHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) (f' : α → β) (h : f' = ⇑f) :

BoundedOrderHom α β

Copy of a BoundedOrderHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

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

source

@[simp]

theorem BoundedOrderHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) (f' : α → β) (h : f' = ⇑f) :

⇑(BoundedOrderHom.copy f f' h) = f'

source

theorem BoundedOrderHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) (f' : α → β) (h : f' = ⇑f) :

BoundedOrderHom.copy f f' h = f

source

def BoundedOrderHom.id (α : Type u_2) [Preorder α] [BoundedOrder α] :

BoundedOrderHom α α

id as a BoundedOrderHom.

Equations

BoundedOrderHom.id α = let __src := OrderHom.id; let __src_1 := TopHom.id α; let __src_2 := BotHom.id α; { toOrderHom := __src, map_top' := ⋯, map_bot' := ⋯ }

source

instance BoundedOrderHom.instInhabitedBoundedOrderHom (α : Type u_2) [Preorder α] [BoundedOrder α] :

Inhabited (BoundedOrderHom α α)

Equations

BoundedOrderHom.instInhabitedBoundedOrderHom α = { default := BoundedOrderHom.id α }

source

@[simp]

theorem BoundedOrderHom.coe_id (α : Type u_2) [Preorder α] [BoundedOrder α] :

⇑(BoundedOrderHom.id α) = id

source

@[simp]

theorem BoundedOrderHom.id_apply {α : Type u_2} [Preorder α] [BoundedOrder α] (a : α) :

(BoundedOrderHom.id α) a = a

source

def BoundedOrderHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :

BoundedOrderHom α γ

Composition of BoundedOrderHoms as a BoundedOrderHom.

Equations

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

source

@[simp]

theorem BoundedOrderHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :

⇑(BoundedOrderHom.comp f g) = ⇑f ∘ ⇑g

source

@[simp]

theorem BoundedOrderHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) (a : α) :

(BoundedOrderHom.comp f g) a = f (g a)

source

@[simp]

theorem BoundedOrderHom.coe_comp_orderHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :

↑(BoundedOrderHom.comp f g) = OrderHom.comp ↑f ↑g

source

@[simp]

theorem BoundedOrderHom.coe_comp_topHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :

↑(BoundedOrderHom.comp f g) = TopHom.comp ↑f ↑g

source

@[simp]

theorem BoundedOrderHom.coe_comp_botHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :

↑(BoundedOrderHom.comp f g) = BotHom.comp ↑f ↑g

source

@[simp]

theorem BoundedOrderHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] [BoundedOrder δ] (f : BoundedOrderHom γ δ) (g : BoundedOrderHom β γ) (h : BoundedOrderHom α β) :

BoundedOrderHom.comp (BoundedOrderHom.comp f g) h = BoundedOrderHom.comp f (BoundedOrderHom.comp g h)

source

@[simp]

theorem BoundedOrderHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) :

BoundedOrderHom.comp f (BoundedOrderHom.id α) = f

source

@[simp]

theorem BoundedOrderHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) :

BoundedOrderHom.comp (BoundedOrderHom.id β) f = f

source

@[simp]

theorem BoundedOrderHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] {g₁ : BoundedOrderHom β γ} {g₂ : BoundedOrderHom β γ} {f : BoundedOrderHom α β} (hf : Function.Surjective ⇑f) :

BoundedOrderHom.comp g₁ f = BoundedOrderHom.comp g₂ f ↔ g₁ = g₂

source

@[simp]

theorem BoundedOrderHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] {g : BoundedOrderHom β γ} {f₁ : BoundedOrderHom α β} {f₂ : BoundedOrderHom α β} (hg : Function.Injective ⇑g) :

BoundedOrderHom.comp g f₁ = BoundedOrderHom.comp g f₂ ↔ f₁ = f₂

Dual homs #

source

@[simp]

theorem TopHom.dual_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [OrderTop α] [LE β] [OrderTop β] (f : TopHom α β) (a : α) :

(TopHom.dual f) a = f a

source

@[simp]

theorem TopHom.dual_symm_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [OrderTop α] [LE β] [OrderTop β] (f : BotHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) :

(TopHom.dual.symm f) a = f a

source

def TopHom.dual {α : Type u_2} {β : Type u_3} [LE α] [OrderTop α] [LE β] [OrderTop β] :

TopHom α β ≃ BotHom αᵒᵈ βᵒᵈ

Reinterpret a top homomorphism as a bot homomorphism between the dual lattices.

Equations

TopHom.dual = { toFun := fun (f : TopHom α β) => { toFun := ⇑f, map_bot' := ⋯ }, invFun := fun (f : BotHom αᵒᵈ βᵒᵈ) => { toFun := ⇑f, map_top' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

source

@[simp]

theorem TopHom.dual_id {α : Type u_2} [LE α] [OrderTop α] :

TopHom.dual (TopHom.id α) = BotHom.id αᵒᵈ

source

@[simp]

theorem TopHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [OrderTop α] [LE β] [OrderTop β] [LE γ] [OrderTop γ] (g : TopHom β γ) (f : TopHom α β) :

TopHom.dual (TopHom.comp g f) = BotHom.comp (TopHom.dual g) (TopHom.dual f)

source

@[simp]

theorem TopHom.symm_dual_id {α : Type u_2} [LE α] [OrderTop α] :

TopHom.dual.symm (BotHom.id αᵒᵈ) = TopHom.id α

source

@[simp]

theorem TopHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [OrderTop α] [LE β] [OrderTop β] [LE γ] [OrderTop γ] (g : BotHom βᵒᵈ γᵒᵈ) (f : BotHom αᵒᵈ βᵒᵈ) :

TopHom.dual.symm (BotHom.comp g f) = TopHom.comp (TopHom.dual.symm g) (TopHom.dual.symm f)

source

@[simp]

theorem BotHom.dual_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [OrderBot α] [LE β] [OrderBot β] (f : BotHom α β) (a : α) :

(BotHom.dual f) a = f a

source

@[simp]

theorem BotHom.dual_symm_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [OrderBot α] [LE β] [OrderBot β] (f : TopHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) :

(BotHom.dual.symm f) a = f a

source

def BotHom.dual {α : Type u_2} {β : Type u_3} [LE α] [OrderBot α] [LE β] [OrderBot β] :

BotHom α β ≃ TopHom αᵒᵈ βᵒᵈ

Reinterpret a bot homomorphism as a top homomorphism between the dual lattices.

Equations

BotHom.dual = { toFun := fun (f : BotHom α β) => { toFun := ⇑f, map_top' := ⋯ }, invFun := fun (f : TopHom αᵒᵈ βᵒᵈ) => { toFun := ⇑f, map_bot' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

source

@[simp]

theorem BotHom.dual_id {α : Type u_2} [LE α] [OrderBot α] :

BotHom.dual (BotHom.id α) = TopHom.id αᵒᵈ

source

@[simp]

theorem BotHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [OrderBot α] [LE β] [OrderBot β] [LE γ] [OrderBot γ] (g : BotHom β γ) (f : BotHom α β) :

BotHom.dual (BotHom.comp g f) = TopHom.comp (BotHom.dual g) (BotHom.dual f)

source

@[simp]

theorem BotHom.symm_dual_id {α : Type u_2} [LE α] [OrderBot α] :

BotHom.dual.symm (TopHom.id αᵒᵈ) = BotHom.id α

source

@[simp]

theorem BotHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [OrderBot α] [LE β] [OrderBot β] [LE γ] [OrderBot γ] (g : TopHom βᵒᵈ γᵒᵈ) (f : TopHom αᵒᵈ βᵒᵈ) :

BotHom.dual.symm (TopHom.comp g f) = BotHom.comp (BotHom.dual.symm g) (BotHom.dual.symm f)

source

@[simp]

theorem BoundedOrderHom.dual_symm_apply_toOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [BoundedOrder α] [Preorder β] [BoundedOrder β] (f : BoundedOrderHom αᵒᵈ βᵒᵈ) :

(BoundedOrderHom.dual.symm f).toOrderHom = OrderHom.dual.symm f.toOrderHom

source

@[simp]

theorem BoundedOrderHom.dual_apply_toOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [BoundedOrder α] [Preorder β] [BoundedOrder β] (f : BoundedOrderHom α β) :

(BoundedOrderHom.dual f).toOrderHom = OrderHom.dual f.toOrderHom

source

def BoundedOrderHom.dual {α : Type u_2} {β : Type u_3} [Preorder α] [BoundedOrder α] [Preorder β] [BoundedOrder β] :

BoundedOrderHom α β ≃ BoundedOrderHom αᵒᵈ βᵒᵈ

Reinterpret a bounded order homomorphism as a bounded order homomorphism between the dual orders.

Equations

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

source

@[simp]

theorem BoundedOrderHom.dual_id {α : Type u_2} [Preorder α] [BoundedOrder α] :

BoundedOrderHom.dual (BoundedOrderHom.id α) = BoundedOrderHom.id αᵒᵈ

source

@[simp]

theorem BoundedOrderHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [BoundedOrder α] [Preorder β] [BoundedOrder β] [Preorder γ] [BoundedOrder γ] (g : BoundedOrderHom β γ) (f : BoundedOrderHom α β) :

BoundedOrderHom.dual (BoundedOrderHom.comp g f) = BoundedOrderHom.comp (BoundedOrderHom.dual g) (BoundedOrderHom.dual f)

source

@[simp]

theorem BoundedOrderHom.symm_dual_id {α : Type u_2} [Preorder α] [BoundedOrder α] :

BoundedOrderHom.dual.symm (BoundedOrderHom.id αᵒᵈ) = BoundedOrderHom.id α

source

@[simp]

theorem BoundedOrderHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [BoundedOrder α] [Preorder β] [BoundedOrder β] [Preorder γ] [BoundedOrder γ] (g : BoundedOrderHom βᵒᵈ γᵒᵈ) (f : BoundedOrderHom αᵒᵈ βᵒᵈ) :

BoundedOrderHom.dual.symm (BoundedOrderHom.comp g f) = BoundedOrderHom.comp (BoundedOrderHom.dual.symm g) (BoundedOrderHom.dual.symm f)

Documentation

Mathlib.Order.Hom.Bounded

Bounded order homomorphisms #

Types of morphisms #

Typeclasses #

Top homomorphisms #

Bot homomorphisms #

Bounded order homomorphisms #

Dual homs #