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