Documentation

Mathlib.Order.Hom.WithTopBot

Adjoining and to order maps and lattice homomorphisms #

This file defines ways to adjoin or or both to order maps (homomorphisms, embeddings and isomorphisms) and lattice homomorphisms, and properties about the results.

Some definitions cause a possibly unbounded lattice homomorphism to become bounded, so they change the type of the homomorphism.

Taking the dual then adding is the same as adding then taking the dual. This is the order iso form of WithTop.ofDual, as proven by coe_toDualBotEquiv.

Equations
    Instances For

      Embedding into WithTop α.

      Equations
        Instances For
          @[simp]
          theorem Function.Embedding.coeWithTop_apply {α : Type u_1} (a✝ : α) :
          coeWithTop a✝ = a✝
          def WithTop.coeOrderHom {α : Type u_4} [Preorder α] :

          The coercion α → WithTop α bundled as monotone map.

          Equations
            Instances For
              @[simp]
              theorem WithTop.coeOrderHom_apply {α : Type u_4} [Preorder α] (a✝ : α) :
              coeOrderHom a✝ = a✝

              Taking the dual then adding is the same as adding then taking the dual. This is the order iso form of WithBot.ofDual, as proven by coe_toDualTopEquiv.

              Equations
                Instances For

                  Embedding into WithBot α.

                  Equations
                    Instances For
                      @[simp]
                      theorem Function.Embedding.coeWithBot_apply {α : Type u_1} (a✝ : α) :
                      coeWithBot a✝ = a✝
                      def WithBot.coeOrderHom {α : Type u_4} [Preorder α] :

                      The coercion α → WithBot α bundled as monotone map.

                      Equations
                        Instances For
                          @[simp]
                          theorem WithBot.coeOrderHom_apply {α : Type u_4} [Preorder α] (a✝ : α) :
                          coeOrderHom a✝ = a✝
                          def OrderHom.withBotMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) :

                          Lift an order homomorphism f : α →o β to an order homomorphism WithBot α →o WithBot β.

                          Equations
                            Instances For
                              @[simp]
                              theorem OrderHom.withBotMap_coe {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) :
                              def OrderHom.withTopMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) :

                              Lift an order homomorphism f : α →o β to an order homomorphism WithTop α →o WithTop β.

                              Equations
                                Instances For
                                  @[simp]
                                  theorem OrderHom.withTopMap_coe {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) :
                                  def OrderEmbedding.withBotMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) :

                                  A version of WithBot.map for order embeddings.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem OrderEmbedding.withBotMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) :
                                      def OrderEmbedding.withTopMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) :

                                      A version of WithTop.map for order embeddings.

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem OrderEmbedding.withTopMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) :

                                          Coercion α → WithBot α as an OrderEmbedding.

                                          Equations
                                            Instances For

                                              Coercion α → WithTop α as an OrderEmbedding.

                                              Equations
                                                Instances For
                                                  def OrderIso.withTopCongr {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :

                                                  A version of Equiv.optionCongr for WithTop.

                                                  Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem OrderIso.withTopCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) (a✝ : Option α) :
                                                      e.withTopCongr a✝ = Option.map (⇑e) a✝
                                                      @[simp]
                                                      theorem OrderIso.withTopCongr_symm {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
                                                      @[simp]
                                                      theorem OrderIso.withTopCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PartialOrder α] [PartialOrder β] [PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
                                                      def OrderIso.withBotCongr {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :

                                                      A version of Equiv.optionCongr for WithBot.

                                                      Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem OrderIso.withBotCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) (a✝ : Option α) :
                                                          e.withBotCongr a✝ = Option.map (⇑e) a✝
                                                          @[simp]
                                                          theorem OrderIso.withBotCongr_symm {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
                                                          @[simp]
                                                          theorem OrderIso.withBotCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PartialOrder α] [PartialOrder β] [PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
                                                          def SupHom.withTop {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) :

                                                          Adjoins a to the domain and codomain of a SupHom.

                                                          Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem SupHom.withTop_toFun {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) (a✝ : WithTop α) :
                                                              f.withTop a✝ = WithTop.map (⇑f) a✝
                                                              @[simp]
                                                              @[simp]
                                                              theorem SupHom.withTop_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [SemilatticeSup β] [SemilatticeSup γ] (f : SupHom β γ) (g : SupHom α β) :
                                                              def SupHom.withBot {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) :

                                                              Adjoins a to the domain and codomain of a SupHom.

                                                              Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem SupHom.withBot_toSupHom_toFun {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) (a✝ : Option α) :
                                                                  f.withBot.toSupHom a✝ = Option.map (⇑f) a✝
                                                                  @[simp]
                                                                  theorem SupHom.withBot_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [SemilatticeSup β] [SemilatticeSup γ] (f : SupHom β γ) (g : SupHom α β) :
                                                                  def SupHom.withTop' {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] [OrderTop β] (f : SupHom α β) :
                                                                  SupHom (WithTop α) β

                                                                  Adjoins a to the codomain of a SupHom.

                                                                  Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem SupHom.withTop'_toFun {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] [OrderTop β] (f : SupHom α β) (a : WithTop α) :
                                                                      def SupHom.withBot' {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] [OrderBot β] (f : SupHom α β) :

                                                                      Adjoins a to the domain of a SupHom.

                                                                      Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem SupHom.withBot'_toSupHom_toFun {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] [OrderBot β] (f : SupHom α β) (a : WithBot α) :
                                                                          def InfHom.withTop {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) :

                                                                          Adjoins a to the domain and codomain of an InfHom.

                                                                          Equations
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem InfHom.withTop_toInfHom_toFun {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) (a✝ : Option α) :
                                                                              f.withTop.toInfHom a✝ = Option.map (⇑f) a✝
                                                                              @[simp]
                                                                              theorem InfHom.withTop_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeInf α] [SemilatticeInf β] [SemilatticeInf γ] (f : InfHom β γ) (g : InfHom α β) :
                                                                              def InfHom.withBot {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) :

                                                                              Adjoins a to the domain and codomain of an InfHom.

                                                                              Equations
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem InfHom.withBot_toFun {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) (a✝ : Option α) :
                                                                                  f.withBot a✝ = Option.map (⇑f) a✝
                                                                                  @[simp]
                                                                                  @[simp]
                                                                                  theorem InfHom.withBot_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeInf α] [SemilatticeInf β] [SemilatticeInf γ] (f : InfHom β γ) (g : InfHom α β) :
                                                                                  def InfHom.withTop' {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] [OrderTop β] (f : InfHom α β) :

                                                                                  Adjoins a to the codomain of an InfHom.

                                                                                  Equations
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem InfHom.withTop'_toInfHom_toFun {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] [OrderTop β] (f : InfHom α β) (a : WithTop α) :
                                                                                      def InfHom.withBot' {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] [OrderBot β] (f : InfHom α β) :
                                                                                      InfHom (WithBot α) β

                                                                                      Adjoins a to the codomain of an InfHom.

                                                                                      Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem InfHom.withBot'_toFun {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] [OrderBot β] (f : InfHom α β) (a : WithBot α) :
                                                                                          def LatticeHom.withTop {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) :

                                                                                          Adjoins a to the domain and codomain of a LatticeHom.

                                                                                          Equations
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem LatticeHom.withTop_toSupHom {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                                              @[simp]
                                                                                              theorem LatticeHom.coe_withTop {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                                              theorem LatticeHom.withTop_apply {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithTop α) :
                                                                                              f.withTop a = WithTop.map (⇑f) a
                                                                                              @[simp]
                                                                                              theorem LatticeHom.withTop_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :
                                                                                              def LatticeHom.withBot {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) :

                                                                                              Adjoins a to the domain and codomain of a LatticeHom.

                                                                                              Equations
                                                                                                Instances For
                                                                                                  @[simp]
                                                                                                  theorem LatticeHom.withBot_toSupHom_toFun {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithBot α) :
                                                                                                  @[simp]
                                                                                                  theorem LatticeHom.coe_withBot {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                                                  f.withBot = Option.map f
                                                                                                  theorem LatticeHom.withBot_apply {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithBot α) :
                                                                                                  f.withBot a = WithBot.map (⇑f) a
                                                                                                  @[simp]
                                                                                                  theorem LatticeHom.withBot_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :
                                                                                                  def LatticeHom.withTopWithBot {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) :

                                                                                                  Adjoins a and to the domain and codomain of a LatticeHom.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem LatticeHom.coe_withTopWithBot {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                                                      theorem LatticeHom.withTopWithBot_apply {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithTop (WithBot α)) :
                                                                                                      @[simp]
                                                                                                      theorem LatticeHom.withTopWithBot_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :
                                                                                                      def LatticeHom.withTop' {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [OrderTop β] (f : LatticeHom α β) :

                                                                                                      Adjoins a to the codomain of a LatticeHom.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          @[simp]
                                                                                                          theorem LatticeHom.withTop'_toSupHom {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [OrderTop β] (f : LatticeHom α β) :
                                                                                                          def LatticeHom.withBot' {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [OrderBot β] (f : LatticeHom α β) :

                                                                                                          Adjoins a to the domain and codomain of a LatticeHom.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              @[simp]
                                                                                                              theorem LatticeHom.withBot'_toSupHom {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [OrderBot β] (f : LatticeHom α β) :
                                                                                                              def LatticeHom.withTopWithBot' {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [BoundedOrder β] (f : LatticeHom α β) :

                                                                                                              Adjoins a and to the codomain of a LatticeHom.

                                                                                                              Equations
                                                                                                                Instances For