Documentation

Mathlib.Order.Hom.Bounded

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 #

Typeclasses #

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.

theorem TopHom.map_top' {α : Type u_6} {β : Type u_7} [Top α] [Top β] (self : TopHom α β) :
self.toFun =

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

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.

theorem BotHom.map_bot' {α : Type u_6} {β : Type u_7} [Bot α] [Bot β] (self : BotHom α β) :
self.toFun =

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

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.

theorem BoundedOrderHom.map_top' {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (self : BoundedOrderHom α β) :
self.toFun =

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

theorem BoundedOrderHom.map_bot' {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (self : BoundedOrderHom α β) :
self.toFun =

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

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

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

You should extend this class when you extend TopHom.

Instances
    @[simp]
    theorem TopHomClass.map_top {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} :
    ∀ {inst : Top α} {inst_1 : Top β} {inst_2 : FunLike F α β} [self : TopHomClass F α β] (f : F), f =

    A TopHomClass morphism preserves the top element.

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

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

    You should extend this class when you extend BotHom.

    Instances
      @[simp]
      theorem BotHomClass.map_bot {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} :
      ∀ {inst : Bot α} {inst_1 : Bot β} {inst_2 : FunLike F α β} [self : BotHomClass F α β] (f : F), f =

      A BotHomClass morphism preserves the bottom element.

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

      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 bf 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
        theorem BoundedOrderHomClass.map_top {F : Type u_6} {α : Type u_7} {β : Type u_8} :
        ∀ {inst : LE α} {inst_1 : LE β} {inst_2 : BoundedOrder α} {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedOrderHomClass F α β] (f : F), f =

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

        theorem BoundedOrderHomClass.map_bot {F : Type u_6} {α : Type u_7} {β : Type u_8} :
        ∀ {inst : LE α} {inst_1 : LE β} {inst_2 : BoundedOrder α} {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedOrderHomClass F α β] (f : F), f =

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

        @[instance 100]
        instance BoundedOrderHomClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
        TopHomClass F α β
        Equations
        • =
        @[instance 100]
        instance BoundedOrderHomClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
        BotHomClass F α β
        Equations
        • =
        @[instance 100]
        instance OrderIsoClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [LE α] [OrderTop α] [PartialOrder β] [OrderTop β] [OrderIsoClass F α β] :
        TopHomClass F α β
        Equations
        • =
        @[instance 100]
        instance OrderIsoClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [LE α] [OrderBot α] [PartialOrder β] [OrderBot β] [OrderIsoClass F α β] :
        BotHomClass F α β
        Equations
        • =
        @[instance 100]
        instance OrderIsoClass.toBoundedOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [LE α] [BoundedOrder α] [PartialOrder β] [BoundedOrder β] [OrderIsoClass F α β] :
        Equations
        • =
        @[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 =
        @[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 =
        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' := }
        instance instCoeTCTopHomOfTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Top α] [Top β] [TopHomClass F α β] :
        CoeTC F (TopHom α β)
        Equations
        • instCoeTCTopHomOfTopHomClass = { coe := TopHomClass.toTopHom }
        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' := }
        instance instCoeTCBotHomOfBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Bot α] [Bot β] [BotHomClass F α β] :
        CoeTC F (BotHom α β)
        Equations
        • instCoeTCBotHomOfBotHomClass = { coe := BotHomClass.toBotHom }
        def BoundedOrderHomClass.toBoundedOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] (f : F) :

        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 = { toFun := f, monotone' := , map_top' := , map_bot' := }
        instance instCoeTCBoundedOrderHomOfBoundedOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
        Equations
        • instCoeTCBoundedOrderHomOfBoundedOrderHomClass = { coe := BoundedOrderHomClass.toBoundedOrderHom }

        Top homomorphisms #

        instance TopHom.instFunLike {α : Type u_2} {β : Type u_3} [Top α] [Top β] :
        FunLike (TopHom α β) α β
        Equations
        • TopHom.instFunLike = { coe := TopHom.toFun, coe_injective' := }
        instance TopHom.instTopHomClass {α : Type u_2} {β : Type u_3} [Top α] [Top β] :
        TopHomClass (TopHom α β) α β
        Equations
        • =
        theorem TopHom.ext_iff {α : Type u_2} {β : Type u_3} [Top α] [Top β] {f : TopHom α β} {g : TopHom α β} :
        f = g ∀ (a : α), f a = g a
        theorem TopHom.ext {α : Type u_2} {β : Type u_3} [Top α] [Top β] {f : TopHom α β} {g : TopHom α β} (h : ∀ (a : α), f a = g a) :
        f = g
        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
        • f.copy f' h = { toFun := f', map_top' := }
        @[simp]
        theorem TopHom.coe_copy {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) (f' : αβ) (h : f' = f) :
        (f.copy f' h) = f'
        theorem TopHom.copy_eq {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) (f' : αβ) (h : f' = f) :
        f.copy f' h = f
        instance TopHom.instInhabited {α : Type u_2} {β : Type u_3} [Top α] [Top β] :
        Equations
        • TopHom.instInhabited = { default := { toFun := fun (x : α) => , map_top' := } }
        def TopHom.id (α : Type u_2) [Top α] :
        TopHom α α

        id as a TopHom.

        Equations
        @[simp]
        theorem TopHom.coe_id (α : Type u_2) [Top α] :
        (TopHom.id α) = id
        @[simp]
        theorem TopHom.id_apply {α : Type u_2} [Top α] (a : α) :
        (TopHom.id α) a = a
        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
        • f.comp g = { toFun := f g, map_top' := }
        @[simp]
        theorem TopHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [Top γ] (f : TopHom β γ) (g : TopHom α β) :
        (f.comp g) = f g
        @[simp]
        theorem TopHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [Top γ] (f : TopHom β γ) (g : TopHom α β) (a : α) :
        (f.comp g) a = f (g a)
        @[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 α β) :
        (f.comp g).comp h = f.comp (g.comp h)
        @[simp]
        theorem TopHom.comp_id {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) :
        f.comp (TopHom.id α) = f
        @[simp]
        theorem TopHom.id_comp {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) :
        (TopHom.id β).comp f = f
        @[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) :
        g₁.comp f = g₂.comp f g₁ = g₂
        @[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) :
        g.comp f₁ = g.comp f₂ f₁ = f₂
        instance TopHom.instLE {α : Type u_2} {β : Type u_3} [Top α] [LE β] [Top β] :
        LE (TopHom α β)
        Equations
        • TopHom.instLE = { le := fun (f g : TopHom α β) => f g }
        instance TopHom.instPreorder {α : Type u_2} {β : Type u_3} [Top α] [Preorder β] [Top β] :
        Equations
        instance TopHom.instPartialOrder {α : Type u_2} {β : Type u_3} [Top α] [PartialOrder β] [Top β] :
        Equations
        instance TopHom.instOrderTop {α : Type u_2} {β : Type u_3} [Top α] [LE β] [OrderTop β] :
        Equations
        @[simp]
        theorem TopHom.coe_top {α : Type u_2} {β : Type u_3} [Top α] [LE β] [OrderTop β] :
        =
        @[simp]
        theorem TopHom.top_apply {α : Type u_2} {β : Type u_3} [Top α] [LE β] [OrderTop β] (a : α) :
        instance TopHom.instInf {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeInf β] [OrderTop β] :
        Inf (TopHom α β)
        Equations
        • TopHom.instInf = { inf := fun (f g : TopHom α β) => { toFun := f g, map_top' := } }
        instance TopHom.instSemilatticeInf {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeInf β] [OrderTop β] :
        Equations
        @[simp]
        theorem TopHom.coe_inf {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeInf β] [OrderTop β] (f : TopHom α β) (g : TopHom α β) :
        (f g) = f g
        @[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
        instance TopHom.instSup {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeSup β] [OrderTop β] :
        Sup (TopHom α β)
        Equations
        • TopHom.instSup = { sup := fun (f g : TopHom α β) => { toFun := f g, map_top' := } }
        instance TopHom.instSemilatticeSup {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeSup β] [OrderTop β] :
        Equations
        @[simp]
        theorem TopHom.coe_sup {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeSup β] [OrderTop β] (f : TopHom α β) (g : TopHom α β) :
        (f g) = f g
        @[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
        instance TopHom.instLattice {α : Type u_2} {β : Type u_3} [Top α] [Lattice β] [OrderTop β] :
        Lattice (TopHom α β)
        Equations
        instance TopHom.instDistribLattice {α : Type u_2} {β : Type u_3} [Top α] [DistribLattice β] [OrderTop β] :
        Equations

        Bot homomorphisms #

        instance BotHom.instFunLike {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] :
        FunLike (BotHom α β) α β
        Equations
        • BotHom.instFunLike = { coe := BotHom.toFun, coe_injective' := }
        instance BotHom.instBotHomClass {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] :
        BotHomClass (BotHom α β) α β
        Equations
        • =
        theorem BotHom.ext_iff {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] {f : BotHom α β} {g : BotHom α β} :
        f = g ∀ (a : α), f a = g a
        theorem BotHom.ext {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] {f : BotHom α β} {g : BotHom α β} (h : ∀ (a : α), f a = g a) :
        f = g
        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
        • f.copy f' h = { toFun := f', map_bot' := }
        @[simp]
        theorem BotHom.coe_copy {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) (f' : αβ) (h : f' = f) :
        (f.copy f' h) = f'
        theorem BotHom.copy_eq {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) (f' : αβ) (h : f' = f) :
        f.copy f' h = f
        instance BotHom.instInhabited {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] :
        Equations
        • BotHom.instInhabited = { default := { toFun := fun (x : α) => , map_bot' := } }
        def BotHom.id (α : Type u_2) [Bot α] :
        BotHom α α

        id as a BotHom.

        Equations
        @[simp]
        theorem BotHom.coe_id (α : Type u_2) [Bot α] :
        (BotHom.id α) = id
        @[simp]
        theorem BotHom.id_apply {α : Type u_2} [Bot α] (a : α) :
        (BotHom.id α) a = a
        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
        • f.comp g = { toFun := f g, map_bot' := }
        @[simp]
        theorem BotHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [Bot γ] (f : BotHom β γ) (g : BotHom α β) :
        (f.comp g) = f g
        @[simp]
        theorem BotHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [Bot γ] (f : BotHom β γ) (g : BotHom α β) (a : α) :
        (f.comp g) a = f (g a)
        @[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 α β) :
        (f.comp g).comp h = f.comp (g.comp h)
        @[simp]
        theorem BotHom.comp_id {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) :
        f.comp (BotHom.id α) = f
        @[simp]
        theorem BotHom.id_comp {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) :
        (BotHom.id β).comp f = f
        @[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) :
        g₁.comp f = g₂.comp f g₁ = g₂
        @[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) :
        g.comp f₁ = g.comp f₂ f₁ = f₂
        instance BotHom.instLE {α : Type u_2} {β : Type u_3} [Bot α] [LE β] [Bot β] :
        LE (BotHom α β)
        Equations
        • BotHom.instLE = { le := fun (f g : BotHom α β) => f g }
        instance BotHom.instPreorder {α : Type u_2} {β : Type u_3} [Bot α] [Preorder β] [Bot β] :
        Equations
        instance BotHom.instPartialOrder {α : Type u_2} {β : Type u_3} [Bot α] [PartialOrder β] [Bot β] :
        Equations
        instance BotHom.instOrderBot {α : Type u_2} {β : Type u_3} [Bot α] [LE β] [OrderBot β] :
        Equations
        @[simp]
        theorem BotHom.coe_bot {α : Type u_2} {β : Type u_3} [Bot α] [LE β] [OrderBot β] :
        =
        @[simp]
        theorem BotHom.bot_apply {α : Type u_2} {β : Type u_3} [Bot α] [LE β] [OrderBot β] (a : α) :
        instance BotHom.instInf {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeInf β] [OrderBot β] :
        Inf (BotHom α β)
        Equations
        • BotHom.instInf = { inf := fun (f g : BotHom α β) => { toFun := f g, map_bot' := } }
        instance BotHom.instSemilatticeInf {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeInf β] [OrderBot β] :
        Equations
        @[simp]
        theorem BotHom.coe_inf {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeInf β] [OrderBot β] (f : BotHom α β) (g : BotHom α β) :
        (f g) = f g
        @[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
        instance BotHom.instSup {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeSup β] [OrderBot β] :
        Sup (BotHom α β)
        Equations
        • BotHom.instSup = { sup := fun (f g : BotHom α β) => { toFun := f g, map_bot' := } }
        instance BotHom.instSemilatticeSup {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeSup β] [OrderBot β] :
        Equations
        @[simp]
        theorem BotHom.coe_sup {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeSup β] [OrderBot β] (f : BotHom α β) (g : BotHom α β) :
        (f g) = f g
        @[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
        instance BotHom.instLattice {α : Type u_2} {β : Type u_3} [Bot α] [Lattice β] [OrderBot β] :
        Lattice (BotHom α β)
        Equations
        instance BotHom.instDistribLattice {α : Type u_2} {β : Type u_3} [Bot α] [DistribLattice β] [OrderBot β] :
        Equations

        Bounded order homomorphisms #

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

        Reinterpret a BoundedOrderHom as a TopHom.

        Equations
        • f.toTopHom = { toFun := f.toFun, map_top' := }
        def BoundedOrderHom.toBotHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) :
        BotHom α β

        Reinterpret a BoundedOrderHom as a BotHom.

        Equations
        • f.toBotHom = { toFun := f.toFun, map_bot' := }
        instance BoundedOrderHom.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] :
        FunLike (BoundedOrderHom α β) α β
        Equations
        • BoundedOrderHom.instFunLike = { coe := fun (f : BoundedOrderHom α β) => f.toFun, coe_injective' := }
        Equations
        • =
        theorem BoundedOrderHom.ext_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] {f : BoundedOrderHom α β} {g : BoundedOrderHom α β} :
        f = g ∀ (a : α), f a = g a
        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
        def BoundedOrderHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) (f' : αβ) (h : f' = f) :

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

        Equations
        • f.copy f' h = { toOrderHom := f.copy f' h, map_top' := , map_bot' := }
        @[simp]
        theorem BoundedOrderHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) (f' : αβ) (h : f' = f) :
        (f.copy f' h) = f'
        theorem BoundedOrderHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) (f' : αβ) (h : f' = f) :
        f.copy f' h = f

        id as a BoundedOrderHom.

        Equations
        @[simp]
        theorem BoundedOrderHom.coe_id (α : Type u_2) [Preorder α] [BoundedOrder α] :
        @[simp]
        theorem BoundedOrderHom.id_apply {α : Type u_2} [Preorder α] [BoundedOrder α] (a : α) :
        def BoundedOrderHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :

        Composition of BoundedOrderHoms as a BoundedOrderHom.

        Equations
        • f.comp g = { toOrderHom := f.comp g.toOrderHom, map_top' := , map_bot' := }
        @[simp]
        theorem BoundedOrderHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :
        (f.comp g) = f g
        @[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 : α) :
        (f.comp g) a = f (g a)
        @[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 α β) :
        (f.comp g) = (↑f).comp g
        @[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 α β) :
        (f.comp g) = (↑f).comp g
        @[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 α β) :
        (f.comp g) = (↑f).comp g
        @[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 α β) :
        (f.comp g).comp h = f.comp (g.comp h)
        @[simp]
        theorem BoundedOrderHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) :
        f.comp (BoundedOrderHom.id α) = f
        @[simp]
        theorem BoundedOrderHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) :
        (BoundedOrderHom.id β).comp f = f
        @[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) :
        g₁.comp f = g₂.comp f g₁ = g₂
        @[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) :
        g.comp f₁ = g.comp f₂ f₁ = f₂

        Dual homs #

        @[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
        @[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
        def TopHom.dual {α : Type u_2} {β : Type u_3} [LE α] [OrderTop α] [LE β] [OrderTop β] :

        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 := }
        @[simp]
        theorem TopHom.dual_id {α : Type u_2} [LE α] [OrderTop α] :
        TopHom.dual (TopHom.id α) = BotHom.id αᵒᵈ
        @[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 (g.comp f) = (TopHom.dual g).comp (TopHom.dual f)
        @[simp]
        theorem TopHom.symm_dual_id {α : Type u_2} [LE α] [OrderTop α] :
        TopHom.dual.symm (BotHom.id αᵒᵈ) = TopHom.id α
        @[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 (g.comp f) = (TopHom.dual.symm g).comp (TopHom.dual.symm f)
        @[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
        @[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
        def BotHom.dual {α : Type u_2} {β : Type u_3} [LE α] [OrderBot α] [LE β] [OrderBot β] :

        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 := }
        @[simp]
        theorem BotHom.dual_id {α : Type u_2} [LE α] [OrderBot α] :
        BotHom.dual (BotHom.id α) = TopHom.id αᵒᵈ
        @[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 (g.comp f) = (BotHom.dual g).comp (BotHom.dual f)
        @[simp]
        theorem BotHom.symm_dual_id {α : Type u_2} [LE α] [OrderBot α] :
        BotHom.dual.symm (TopHom.id αᵒᵈ) = BotHom.id α
        @[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 (g.comp f) = (BotHom.dual.symm g).comp (BotHom.dual.symm f)
        @[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
        @[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

        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.
        @[simp]
        theorem BoundedOrderHom.dual_id {α : Type u_2} [Preorder α] [BoundedOrder α] :
        BoundedOrderHom.dual (BoundedOrderHom.id α) = BoundedOrderHom.id αᵒᵈ
        @[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 (g.comp f) = (BoundedOrderHom.dual g).comp (BoundedOrderHom.dual f)
        @[simp]
        theorem BoundedOrderHom.symm_dual_id {α : Type u_2} [Preorder α] [BoundedOrder α] :
        BoundedOrderHom.dual.symm (BoundedOrderHom.id αᵒᵈ) = BoundedOrderHom.id α
        @[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 (g.comp f) = (BoundedOrderHom.dual.symm g).comp (BoundedOrderHom.dual.symm f)