Bounded order homomorphisms

This file defines (bounded) order homomorphisms.

We use the FunLike 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

• TopHomClass
• BotHomClass
• BoundedOrderHomClass

ink

structure TopHom (α : Type u_1) (β : Type u_2) [inst : Top α] [inst : Top β] : Type (maxu_1u_2)

• The underlying function. The preferred spelling is FunLike.coe.

  toFun : α → β

• The function preserves the top element. The preferred spelling is map_top.

  map_top' : toFun ⊤ = ⊤

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

ink

structure BotHom (α : Type u_1) (β : Type u_2) [inst : Bot α] [inst : Bot β] : Type (maxu_1u_2)

• The underlying function. The preferred spelling is FunLike.coe.

  toFun : α → β

• The function preserves the bottom element. The preferred spelling is map_bot.

  map_bot' : toFun ⊥ = ⊥

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

ink

structure BoundedOrderHom (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] extends OrderHom : Type (maxu_1u_2)

• The function preserves the top element. The preferred spelling is map_top.

  map_top' : ↑toOrderHom ⊤ = ⊤

• The function preserves the bottom element. The preferred spelling is map_bot.

  map_bot' : ↑toOrderHom ⊥ = ⊥

The type of bounded order homomorphisms from α to β.

ink

class TopHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Top α] [inst : Top β] extends FunLike : Type (max(maxu_1u_2)u_3)

• A TopHomClass morphism preserves the top element.

  map_top : ∀ (f : F), ↑f ⊤ = ⊤

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

You should extend this class when you extend TopHom.

ink

class BotHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Bot α] [inst : Bot β] extends FunLike : Type (max(maxu_1u_2)u_3)

• A BotHomClass morphism preserves the bottom element.

  map_bot : ∀ (f : F), ↑f ⊥ = ⊥

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

You should extend this class when you extend BotHom.

ink

class BoundedOrderHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : LE α] [inst : LE β] [inst : BoundedOrder α] [inst : BoundedOrder β] extends RelHomClass : Type (max(maxu_1u_2)u_3)

• Morphisms preserve the top element. The preferred spelling is _root_.map_top.

  map_top : ∀ (f : F), ↑f ⊤ = ⊤

• Morphisms preserve the bottom element. The preferred spelling is _root_.map_bot.

  map_bot : ∀ (f : F), ↑f ⊥ = ⊥

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

You should extend this class when you extend BoundedOrderHom.

ink

instance BoundedOrderHomClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : LE α} → {x_1 : LE β} → {x_2 : BoundedOrder α} → {x_3 : BoundedOrder β} → [inst : BoundedOrderHomClass F α β] → TopHomClass F α β

Equations

• BoundedOrderHomClass.toTopHomClass = let src := inst; TopHomClass.mk (_ : ∀ (f : F), ↑f ⊤ = ⊤)

ink

instance BoundedOrderHomClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : LE α} → {x_1 : LE β} → {x_2 : BoundedOrder α} → {x_3 : BoundedOrder β} → [inst : BoundedOrderHomClass F α β] → BotHomClass F α β

Equations

• BoundedOrderHomClass.toBotHomClass = let src := inst; BotHomClass.mk (_ : ∀ (f : F), ↑f ⊥ = ⊥)

ink

instance OrderIsoClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : LE α} → {x_1 : OrderTop α} → {x_2 : PartialOrder β} → {x_3 : OrderTop β} → [inst : OrderIsoClass F α β] → TopHomClass F α β

Equations

• OrderIsoClass.toTopHomClass = let src := let_fun this := inferInstance; this; TopHomClass.mk (_ : ∀ (f : F), ↑f ⊤ = ⊤)

ink

instance OrderIsoClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : LE α} → {x_1 : OrderBot α} → {x_2 : PartialOrder β} → {x_3 : OrderBot β} → [inst : OrderIsoClass F α β] → BotHomClass F α β

Equations

• OrderIsoClass.toBotHomClass = let src := let_fun this := inferInstance; this; BotHomClass.mk (_ : ∀ (f : F), ↑f ⊥ = ⊥)

ink

instance OrderIsoClass.toBoundedOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : LE α} → {x_1 : BoundedOrder α} → {x_2 : PartialOrder β} → {x_3 : BoundedOrder β} → [inst : OrderIsoClass F α β] → BoundedOrderHomClass F α β

Equations

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

ink

@[simp]

theorem map_eq_top_iff {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : PartialOrder β] [inst : OrderTop β] [inst : OrderIsoClass F α β] (f : F) {a : α} : ↑f a = ⊤ ↔ a = ⊤

ink

@[simp]

theorem map_eq_bot_iff {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : PartialOrder β] [inst : OrderBot β] [inst : OrderIsoClass F α β] (f : F) {a : α} : ↑f a = ⊥ ↔ a = ⊥

ink

def TopHomClass.toTopHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Top α] [inst : Top β] [inst : 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' := (_ : ↑f ⊤ = ⊤) }

ink

instance instCoeTCTopHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Top α] [inst : Top β] [inst : TopHomClass F α β] : CoeTC F (TopHom α β)

Equations

• instCoeTCTopHom = { coe := TopHomClass.toTopHom }

ink

def BotHomClass.toBotHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst : Bot β] [inst : 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' := (_ : ↑f ⊥ = ⊥) }

ink

instance instCoeTCBotHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst : Bot β] [inst : BotHomClass F α β] : CoeTC F (BotHom α β)

Equations

• instCoeTCBotHom = { coe := BotHomClass.toBotHom }

ink

def BoundedOrderHomClass.toBoundedOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : 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' := (_ : Monotone ↑src) }, map_top' := (_ : ↑f ⊤ = ⊤), map_bot' := (_ : ↑f ⊥ = ⊥) }

ink

instance instCoeTCBoundedOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrderHomClass F α β] : CoeTC F (BoundedOrderHom α β)

Equations

• instCoeTCBoundedOrderHom = { coe := BoundedOrderHomClass.toBoundedOrderHom }

Top homomorphisms

ink

instance TopHom.instTopHomClassTopHom {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] : TopHomClass (TopHom α β) α β

Equations

• TopHom.instTopHomClassTopHom = TopHomClass.mk (_ : ∀ (self : TopHom α β), TopHom.toFun self ⊤ = ⊤)

ink

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

ink

def TopHom.copy {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : 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' := (_ : f' ⊤ = ⊤) }

ink

@[simp]

theorem TopHom.coe_copy {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] (f : TopHom α β) (f' : α → β) (h : f' = ↑f) : ↑(TopHom.copy f f' h) = f'

ink

theorem TopHom.copy_eq {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] (f : TopHom α β) (f' : α → β) (h : f' = ↑f) : TopHom.copy f f' h = f

ink

instance TopHom.instInhabitedTopHom {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] : Inhabited (TopHom α β)

Equations

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

ink

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

id as a TopHom.

Equations

• TopHom.id α = { toFun := id, map_top' := (_ : id ⊤ = id ⊤) }

ink

@[simp]

theorem TopHom.coe_id (α : Type u_1) [inst : Top α] : ↑(TopHom.id α) = id

ink

@[simp]

theorem TopHom.id_apply {α : Type u_1} [inst : Top α] (a : α) : ↑(TopHom.id α) a = a

ink

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

Composition of TopHoms as a TopHom.

Equations

• TopHom.comp f g = { toFun := ↑f ∘ ↑g, map_top' := (_ : (↑f ∘ ↑g) ⊤ = ⊤) }

ink

@[simp]

theorem TopHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Top α] [inst : Top β] [inst : Top γ] (f : TopHom β γ) (g : TopHom α β) : ↑(TopHom.comp f g) = ↑f ∘ ↑g

ink

@[simp]

theorem TopHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Top α] [inst : Top β] [inst : Top γ] (f : TopHom β γ) (g : TopHom α β) (a : α) : ↑(TopHom.comp f g) a = ↑f (↑g a)

ink

@[simp]

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

ink

@[simp]

theorem TopHom.comp_id {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] (f : TopHom α β) : TopHom.comp f (TopHom.id α) = f

ink

@[simp]

theorem TopHom.id_comp {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] (f : TopHom α β) : TopHom.comp (TopHom.id β) f = f

ink

theorem TopHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Top α] [inst : Top β] [inst : Top γ] {g₁ : TopHom β γ} {g₂ : TopHom β γ} {f : TopHom α β} (hf : Function.Surjective ↑f) : TopHom.comp g₁ f = TopHom.comp g₂ f ↔ g₁ = g₂

ink

theorem TopHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Top α] [inst : Top β] [inst : Top γ] {g : TopHom β γ} {f₁ : TopHom α β} {f₂ : TopHom α β} (hg : Function.Injective ↑g) : TopHom.comp g f₁ = TopHom.comp g f₂ ↔ f₁ = f₂

ink

instance TopHom.instPreorderTopHom {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Preorder β] [inst : Top β] : Preorder (TopHom α β)

Equations

• TopHom.instPreorderTopHom = Preorder.lift FunLike.coe

ink

instance TopHom.instPartialOrderTopHom {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : PartialOrder β] [inst : Top β] : PartialOrder (TopHom α β)

Equations

• TopHom.instPartialOrderTopHom = PartialOrder.lift (fun f => ↑f) (_ : Function.Injective fun f => ↑f)

ink

instance TopHom.instOrderTopTopHomToTopToLEToLEInstPreorderTopHom {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Preorder β] [inst : OrderTop β] : OrderTop (TopHom α β)

Equations

• TopHom.instOrderTopTopHomToTopToLEToLEInstPreorderTopHom = OrderTop.mk (_ : ∀ (x : TopHom α β), (fun i => ↑x i) ≤ ⊤)

ink

@[simp]

theorem TopHom.coe_top {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Preorder β] [inst : OrderTop β] : ↑⊤ = ⊤

ink

@[simp]

theorem TopHom.top_apply {α : Type u_2} {β : Type u_1} [inst : Top α] [inst : Preorder β] [inst : OrderTop β] (a : α) : ↑⊤ a = ⊤

ink

instance TopHom.instInfTopHomToTopToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeInf β] [inst : OrderTop β] : Inf (TopHom α β)

Equations

• TopHom.instInfTopHomToTopToLEToPreorderToPartialOrder = { inf := fun f g => { toFun := ↑f ⊓ ↑g, map_top' := (_ : ((α → β) ⊓ Pi.instInfForAll) ↑f ↑g ⊤ = ⊤) } }

ink

instance TopHom.instSemilatticeInfTopHomToTopToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeInf β] [inst : OrderTop β] : SemilatticeInf (TopHom α β)

Equations

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

ink

@[simp]

theorem TopHom.coe_inf {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeInf β] [inst : OrderTop β] (f : TopHom α β) (g : TopHom α β) : ↑(f ⊓ g) = ↑f ⊓ ↑g

ink

@[simp]

theorem TopHom.inf_apply {α : Type u_2} {β : Type u_1} [inst : Top α] [inst : SemilatticeInf β] [inst : OrderTop β] (f : TopHom α β) (g : TopHom α β) (a : α) : ↑(f ⊓ g) a = ↑f a ⊓ ↑g a

ink

instance TopHom.instSupTopHomToTopToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeSup β] [inst : OrderTop β] : Sup (TopHom α β)

Equations

• TopHom.instSupTopHomToTopToLEToPreorderToPartialOrder = { sup := fun f g => { toFun := ↑f ⊔ ↑g, map_top' := (_ : ((α → β) ⊔ Pi.instSupForAll) ↑f ↑g ⊤ = ⊤) } }

ink

instance TopHom.instSemilatticeSupTopHomToTopToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeSup β] [inst : OrderTop β] : SemilatticeSup (TopHom α β)

Equations

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

ink

@[simp]

theorem TopHom.coe_sup {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeSup β] [inst : OrderTop β] (f : TopHom α β) (g : TopHom α β) : ↑(f ⊔ g) = ↑f ⊔ ↑g

ink

@[simp]

theorem TopHom.sup_apply {α : Type u_2} {β : Type u_1} [inst : Top α] [inst : SemilatticeSup β] [inst : OrderTop β] (f : TopHom α β) (g : TopHom α β) (a : α) : ↑(f ⊔ g) a = ↑f a ⊔ ↑g a

ink

instance TopHom.instLatticeTopHomToTopToLEToPreorderToPartialOrderToSemilatticeInf {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Lattice β] [inst : OrderTop β] : Lattice (TopHom α β)

Equations

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

ink

instance TopHom.instDistribLatticeTopHomToTopToLEToPreorderToPartialOrderToSemilatticeInfToLattice {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : DistribLattice β] [inst : OrderTop β] : DistribLattice (TopHom α β)

Equations

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

Bot homomorphisms

ink

instance BotHom.instBotHomClassBotHom {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] : BotHomClass (BotHom α β) α β

Equations

• BotHom.instBotHomClassBotHom = BotHomClass.mk (_ : ∀ (self : BotHom α β), BotHom.toFun self ⊥ = ⊥)

ink

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

ink

def BotHom.copy {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : 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' := (_ : f' ⊥ = ⊥) }

ink

@[simp]

theorem BotHom.coe_copy {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] (f : BotHom α β) (f' : α → β) (h : f' = ↑f) : ↑(BotHom.copy f f' h) = f'

ink

theorem BotHom.copy_eq {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] (f : BotHom α β) (f' : α → β) (h : f' = ↑f) : BotHom.copy f f' h = f

ink

instance BotHom.instInhabitedBotHom {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] : Inhabited (BotHom α β)

Equations

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

ink

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

id as a BotHom.

Equations

• BotHom.id α = { toFun := id, map_bot' := (_ : id ⊥ = id ⊥) }

ink

@[simp]

theorem BotHom.coe_id (α : Type u_1) [inst : Bot α] : ↑(BotHom.id α) = id

ink

@[simp]

theorem BotHom.id_apply {α : Type u_1} [inst : Bot α] (a : α) : ↑(BotHom.id α) a = a

ink

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

Composition of BotHoms as a BotHom.

Equations

• BotHom.comp f g = { toFun := ↑f ∘ ↑g, map_bot' := (_ : (↑f ∘ ↑g) ⊥ = ⊥) }

ink

@[simp]

theorem BotHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bot α] [inst : Bot β] [inst : Bot γ] (f : BotHom β γ) (g : BotHom α β) : ↑(BotHom.comp f g) = ↑f ∘ ↑g

ink

@[simp]

theorem BotHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bot α] [inst : Bot β] [inst : Bot γ] (f : BotHom β γ) (g : BotHom α β) (a : α) : ↑(BotHom.comp f g) a = ↑f (↑g a)

ink

@[simp]

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

ink

@[simp]

theorem BotHom.comp_id {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] (f : BotHom α β) : BotHom.comp f (BotHom.id α) = f

ink

@[simp]

theorem BotHom.id_comp {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] (f : BotHom α β) : BotHom.comp (BotHom.id β) f = f

ink

theorem BotHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bot α] [inst : Bot β] [inst : Bot γ] {g₁ : BotHom β γ} {g₂ : BotHom β γ} {f : BotHom α β} (hf : Function.Surjective ↑f) : BotHom.comp g₁ f = BotHom.comp g₂ f ↔ g₁ = g₂

ink

theorem BotHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bot α] [inst : Bot β] [inst : Bot γ] {g : BotHom β γ} {f₁ : BotHom α β} {f₂ : BotHom α β} (hg : Function.Injective ↑g) : BotHom.comp g f₁ = BotHom.comp g f₂ ↔ f₁ = f₂

ink

instance BotHom.instPreorderBotHom {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Preorder β] [inst : Bot β] : Preorder (BotHom α β)

Equations

• BotHom.instPreorderBotHom = Preorder.lift FunLike.coe

ink

instance BotHom.instPartialOrderBotHom {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : PartialOrder β] [inst : Bot β] : PartialOrder (BotHom α β)

Equations

• BotHom.instPartialOrderBotHom = PartialOrder.lift (fun f => ↑f) (_ : Function.Injective fun f => ↑f)

ink

instance BotHom.instOrderBotBotHomToBotToLEToLEInstPreorderBotHom {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Preorder β] [inst : OrderBot β] : OrderBot (BotHom α β)

Equations

• BotHom.instOrderBotBotHomToBotToLEToLEInstPreorderBotHom = OrderBot.mk (_ : ∀ (x : BotHom α β), ⊥ ≤ fun i => ↑x i)

ink

@[simp]

theorem BotHom.coe_bot {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Preorder β] [inst : OrderBot β] : ↑⊥ = ⊥

ink

@[simp]

theorem BotHom.bot_apply {α : Type u_2} {β : Type u_1} [inst : Bot α] [inst : Preorder β] [inst : OrderBot β] (a : α) : ↑⊥ a = ⊥

ink

instance BotHom.instInfBotHomToBotToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeInf β] [inst : OrderBot β] : Inf (BotHom α β)

Equations

• BotHom.instInfBotHomToBotToLEToPreorderToPartialOrder = { inf := fun f g => { toFun := ↑f ⊓ ↑g, map_bot' := (_ : ((α → β) ⊓ Pi.instInfForAll) ↑f ↑g ⊥ = ⊥) } }

ink

instance BotHom.instSemilatticeInfBotHomToBotToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeInf β] [inst : OrderBot β] : SemilatticeInf (BotHom α β)

Equations

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

ink

@[simp]

theorem BotHom.coe_inf {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeInf β] [inst : OrderBot β] (f : BotHom α β) (g : BotHom α β) : ↑(f ⊓ g) = ↑f ⊓ ↑g

ink

@[simp]

theorem BotHom.inf_apply {α : Type u_2} {β : Type u_1} [inst : Bot α] [inst : SemilatticeInf β] [inst : OrderBot β] (f : BotHom α β) (g : BotHom α β) (a : α) : ↑(f ⊓ g) a = ↑f a ⊓ ↑g a

ink

instance BotHom.instSupBotHomToBotToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeSup β] [inst : OrderBot β] : Sup (BotHom α β)

Equations

• BotHom.instSupBotHomToBotToLEToPreorderToPartialOrder = { sup := fun f g => { toFun := ↑f ⊔ ↑g, map_bot' := (_ : ((α → β) ⊔ Pi.instSupForAll) ↑f ↑g ⊥ = ⊥) } }

ink

instance BotHom.instSemilatticeSupBotHomToBotToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeSup β] [inst : OrderBot β] : SemilatticeSup (BotHom α β)

Equations

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

ink

@[simp]

theorem BotHom.coe_sup {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeSup β] [inst : OrderBot β] (f : BotHom α β) (g : BotHom α β) : ↑(f ⊔ g) = ↑f ⊔ ↑g

ink

@[simp]

theorem BotHom.sup_apply {α : Type u_2} {β : Type u_1} [inst : Bot α] [inst : SemilatticeSup β] [inst : OrderBot β] (f : BotHom α β) (g : BotHom α β) (a : α) : ↑(f ⊔ g) a = ↑f a ⊔ ↑g a

ink

instance BotHom.instLatticeBotHomToBotToLEToPreorderToPartialOrderToSemilatticeInf {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Lattice β] [inst : OrderBot β] : Lattice (BotHom α β)

Equations

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

ink

instance BotHom.instDistribLatticeBotHomToBotToLEToPreorderToPartialOrderToSemilatticeInfToLattice {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : DistribLattice β] [inst : OrderBot β] : DistribLattice (BotHom α β)

Equations

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

Bounded order homomorphisms

ink

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

Reinterpret a BoundedOrderHom as a TopHom.

Equations

• BoundedOrderHom.toTopHom f = { toFun := ↑f.toOrderHom, map_top' := (_ : ↑f.toOrderHom ⊤ = ⊤) }

ink

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

Reinterpret a BoundedOrderHom as a BotHom.

Equations

• BoundedOrderHom.toBotHom f = { toFun := ↑f.toOrderHom, map_bot' := (_ : ↑f.toOrderHom ⊥ = ⊥) }

ink

instance BoundedOrderHom.instBoundedOrderHomClassBoundedOrderHomToLEToLE {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] : BoundedOrderHomClass (BoundedOrderHom α β) α β

Equations

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

ink

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

ink

def BoundedOrderHom.copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : 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.

ink

@[simp]

theorem BoundedOrderHom.coe_copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : BoundedOrderHom α β) (f' : α → β) (h : f' = ↑f) : ↑(BoundedOrderHom.copy f f' h) = f'

ink

theorem BoundedOrderHom.copy_eq {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : BoundedOrderHom α β) (f' : α → β) (h : f' = ↑f) : BoundedOrderHom.copy f f' h = f

ink

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

id as a BoundedOrderHom.

Equations

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

ink

instance BoundedOrderHom.instInhabitedBoundedOrderHom (α : Type u_1) [inst : Preorder α] [inst : BoundedOrder α] : Inhabited (BoundedOrderHom α α)

Equations

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

ink

@[simp]

theorem BoundedOrderHom.coe_id (α : Type u_1) [inst : Preorder α] [inst : BoundedOrder α] : ↑(BoundedOrderHom.id α) = id

ink

@[simp]

theorem BoundedOrderHom.id_apply {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] (a : α) : ↑(BoundedOrderHom.id α) a = a

ink

def BoundedOrderHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : 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.

ink

@[simp]

theorem BoundedOrderHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : ↑(BoundedOrderHom.comp f g) = ↑f ∘ ↑g

ink

@[simp]

theorem BoundedOrderHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) (a : α) : ↑(BoundedOrderHom.comp f g) a = ↑f (↑g a)

ink

@[simp]

theorem BoundedOrderHom.coe_comp_orderHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : ↑(BoundedOrderHom.comp f g) = OrderHom.comp ↑f ↑g

ink

@[simp]

theorem BoundedOrderHom.coe_comp_topHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : ↑(BoundedOrderHom.comp f g) = TopHom.comp ↑f ↑g

ink

@[simp]

theorem BoundedOrderHom.coe_comp_botHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : ↑(BoundedOrderHom.comp f g) = BotHom.comp ↑f ↑g

ink

@[simp]

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

ink

@[simp]

theorem BoundedOrderHom.comp_id {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : BoundedOrderHom α β) : BoundedOrderHom.comp f (BoundedOrderHom.id α) = f

ink

@[simp]

theorem BoundedOrderHom.id_comp {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : BoundedOrderHom α β) : BoundedOrderHom.comp (BoundedOrderHom.id β) f = f

ink

theorem BoundedOrderHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] {g₁ : BoundedOrderHom β γ} {g₂ : BoundedOrderHom β γ} {f : BoundedOrderHom α β} (hf : Function.Surjective ↑f) : BoundedOrderHom.comp g₁ f = BoundedOrderHom.comp g₂ f ↔ g₁ = g₂

ink

theorem BoundedOrderHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] {g : BoundedOrderHom β γ} {f₁ : BoundedOrderHom α β} {f₂ : BoundedOrderHom α β} (hg : Function.Injective ↑g) : BoundedOrderHom.comp g f₁ = BoundedOrderHom.comp g f₂ ↔ f₁ = f₂

Dual homs

ink

@[simp]

theorem TopHom.dual_symm_apply_apply {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : LE β] [inst : OrderTop β] (f : BotHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) : ↑(↑(Equiv.symm TopHom.dual) f) a = ↑f a

ink

@[simp]

theorem TopHom.dual_apply_apply {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : LE β] [inst : OrderTop β] (f : TopHom α β) (a : α) : ↑(↑TopHom.dual f) a = ↑f a

ink

def TopHom.dual {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : LE β] [inst : OrderTop β] : TopHom α β ≃ BotHom αᵒᵈ βᵒᵈ

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

Equations

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

ink

@[simp]

theorem TopHom.dual_id {α : Type u_1} [inst : LE α] [inst : OrderTop α] : ↑TopHom.dual (TopHom.id α) = BotHom.id αᵒᵈ

ink

@[simp]

theorem TopHom.dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : LE β] [inst : OrderTop β] [inst : LE γ] [inst : OrderTop γ] (g : TopHom β γ) (f : TopHom α β) : ↑TopHom.dual (TopHom.comp g f) = BotHom.comp (↑TopHom.dual g) (↑TopHom.dual f)

ink

@[simp]

theorem TopHom.symm_dual_id {α : Type u_1} [inst : LE α] [inst : OrderTop α] : ↑(Equiv.symm TopHom.dual) (BotHom.id αᵒᵈ) = TopHom.id α

ink

@[simp]

theorem TopHom.symm_dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : LE β] [inst : OrderTop β] [inst : LE γ] [inst : OrderTop γ] (g : BotHom βᵒᵈ γᵒᵈ) (f : BotHom αᵒᵈ βᵒᵈ) : ↑(Equiv.symm TopHom.dual) (BotHom.comp g f) = TopHom.comp (↑(Equiv.symm TopHom.dual) g) (↑(Equiv.symm TopHom.dual) f)

ink

@[simp]

theorem BotHom.dual_apply_apply {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] [inst : OrderBot β] (f : BotHom α β) (a : α) : ↑(↑BotHom.dual f) a = ↑f a

ink

@[simp]

theorem BotHom.dual_symm_apply_apply {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] [inst : OrderBot β] (f : TopHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) : ↑(↑(Equiv.symm BotHom.dual) f) a = ↑f a

ink

def BotHom.dual {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] [inst : OrderBot β] : BotHom α β ≃ TopHom αᵒᵈ βᵒᵈ

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

Equations

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

ink

@[simp]

theorem BotHom.dual_id {α : Type u_1} [inst : LE α] [inst : OrderBot α] : ↑BotHom.dual (BotHom.id α) = TopHom.id αᵒᵈ

ink

@[simp]

theorem BotHom.dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] [inst : OrderBot β] [inst : LE γ] [inst : OrderBot γ] (g : BotHom β γ) (f : BotHom α β) : ↑BotHom.dual (BotHom.comp g f) = TopHom.comp (↑BotHom.dual g) (↑BotHom.dual f)

ink

@[simp]

theorem BotHom.symm_dual_id {α : Type u_1} [inst : LE α] [inst : OrderBot α] : ↑(Equiv.symm BotHom.dual) (TopHom.id αᵒᵈ) = BotHom.id α

ink

@[simp]

theorem BotHom.symm_dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] [inst : OrderBot β] [inst : LE γ] [inst : OrderBot γ] (g : TopHom βᵒᵈ γᵒᵈ) (f : TopHom αᵒᵈ βᵒᵈ) : ↑(Equiv.symm BotHom.dual) (TopHom.comp g f) = BotHom.comp (↑(Equiv.symm BotHom.dual) g) (↑(Equiv.symm BotHom.dual) f)

ink

@[simp]

theorem BoundedOrderHom.dual_apply_toOrderHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : BoundedOrder α] [inst : Preorder β] [inst : BoundedOrder β] (f : BoundedOrderHom α β) : (↑BoundedOrderHom.dual f).toOrderHom = ↑OrderHom.dual f.toOrderHom

ink

@[simp]

theorem BoundedOrderHom.dual_symm_apply_toOrderHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : BoundedOrder α] [inst : Preorder β] [inst : BoundedOrder β] (f : BoundedOrderHom αᵒᵈ βᵒᵈ) : (↑(Equiv.symm BoundedOrderHom.dual) f).toOrderHom = ↑(Equiv.symm OrderHom.dual) f.toOrderHom

ink

def BoundedOrderHom.dual {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : BoundedOrder α] [inst : Preorder β] [inst : 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.

ink

@[simp]

theorem BoundedOrderHom.dual_id {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] : ↑BoundedOrderHom.dual (BoundedOrderHom.id α) = BoundedOrderHom.id αᵒᵈ

ink

@[simp]

theorem BoundedOrderHom.dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : BoundedOrder α] [inst : Preorder β] [inst : BoundedOrder β] [inst : Preorder γ] [inst : BoundedOrder γ] (g : BoundedOrderHom β γ) (f : BoundedOrderHom α β) : ↑BoundedOrderHom.dual (BoundedOrderHom.comp g f) = BoundedOrderHom.comp (↑BoundedOrderHom.dual g) (↑BoundedOrderHom.dual f)

ink

@[simp]

theorem BoundedOrderHom.symm_dual_id {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] : ↑(Equiv.symm BoundedOrderHom.dual) (BoundedOrderHom.id αᵒᵈ) = BoundedOrderHom.id α

ink

@[simp]

theorem BoundedOrderHom.symm_dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : BoundedOrder α] [inst : Preorder β] [inst : BoundedOrder β] [inst : Preorder γ] [inst : BoundedOrder γ] (g : BoundedOrderHom βᵒᵈ γᵒᵈ) (f : BoundedOrderHom αᵒᵈ βᵒᵈ) : ↑(Equiv.symm BoundedOrderHom.dual) (BoundedOrderHom.comp g f) = BoundedOrderHom.comp (↑(Equiv.symm BoundedOrderHom.dual) g) (↑(Equiv.symm BoundedOrderHom.dual) f)