Documentation

Mathlib.Algebra.Order.Hom.Ring

Ordered ring homomorphisms #

Homomorphisms between ordered (semi)rings that respect the ordering.

Main definitions #

Notation #

Implementation notes #

This file used to define typeclasses for order-preserving ring homomorphisms and isomorphisms. In https://github.com/leanprover-community/mathlib4/pull/10544, we migrated from assumptions like [FunLike F R S] [OrderRingHomClass F R S] to assumptions like [FunLike F R S] [OrderHomClass F R S] [RingHomClass F R S], making some typeclasses and instances irrelevant.

Tags #

ordered ring homomorphism, order homomorphism

structure OrderRingHom (α : Type u_6) (β : Type u_7) [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] extends α →+* β :
Type (max u_6 u_7)

OrderRingHom α β, denoted α →+*o β, is the type of monotone semiring homomorphisms from α to β.

When possible, instead of parametrizing results over (f : OrderRingHom α β), you should parametrize over (F : Type*) [OrderRingHomClass F α β] (f : F).

When you extend this structure, make sure to extend OrderRingHomClass.

Instances For

    OrderRingHom α β, denoted α →+*o β, is the type of monotone semiring homomorphisms from α to β.

    When possible, instead of parametrizing results over (f : OrderRingHom α β), you should parametrize over (F : Type*) [OrderRingHomClass F α β] (f : F).

    When you extend this structure, make sure to extend OrderRingHomClass.

    Equations
      Instances For
        structure OrderRingIso (α : Type u_6) (β : Type u_7) [Mul α] [Mul β] [Add α] [Add β] [LE α] [LE β] extends α ≃+* β :
        Type (max u_6 u_7)

        OrderRingIso α β, denoted as α ≃+*o β, is the type of order-preserving semiring isomorphisms between α and β.

        When possible, instead of parametrizing results over (f : OrderRingIso α β), you should parametrize over (F : Type*) [OrderRingIsoClass F α β] (f : F).

        When you extend this structure, make sure to extend OrderRingIsoClass.

        Instances For

          OrderRingIso α β, denoted as α ≃+*o β, is the type of order-preserving semiring isomorphisms between α and β.

          When possible, instead of parametrizing results over (f : OrderRingIso α β), you should parametrize over (F : Type*) [OrderRingIsoClass F α β] (f : F).

          When you extend this structure, make sure to extend OrderRingIsoClass.

          Equations
            Instances For
              def OrderRingHomClass.toOrderRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderHomClass F α β] [RingHomClass F α β] (f : F) :
              α →+*o β

              Turn an element of a type F satisfying OrderHomClass F α β and RingHomClass F α β into an actual OrderRingHom. This is declared as the default coercion from F to α →+*o β.

              Equations
                Instances For
                  instance instCoeTCOrderRingHomOfOrderHomClassOfRingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderHomClass F α β] [RingHomClass F α β] :
                  CoeTC F (α →+*o β)

                  Any type satisfying OrderRingHomClass can be cast into OrderRingHom via OrderRingHomClass.toOrderRingHom.

                  Equations
                    def OrderRingIsoClass.toOrderRingIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [OrderIsoClass F α β] [RingEquivClass F α β] (f : F) :
                    α ≃+*o β

                    Turn an element of a type F satisfying OrderIsoClass F α β and RingEquivClass F α β into an actual OrderRingIso. This is declared as the default coercion from F to α ≃+*o β.

                    Equations
                      Instances For
                        instance instCoeTCOrderRingIsoOfOrderIsoClassOfRingEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [OrderIsoClass F α β] [RingEquivClass F α β] :
                        CoeTC F (α ≃+*o β)

                        Any type satisfying OrderRingIsoClass can be cast into OrderRingIso via OrderRingIsoClass.toOrderRingIso.

                        Equations

                          Ordered ring homomorphisms #

                          def OrderRingHom.toOrderAddMonoidHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                          α →+o β

                          Reinterpret an ordered ring homomorphism as an ordered additive monoid homomorphism.

                          Equations
                            Instances For
                              def OrderRingHom.toOrderMonoidWithZeroHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                              α →*₀o β

                              Reinterpret an ordered ring homomorphism as an order homomorphism.

                              Equations
                                Instances For
                                  instance OrderRingHom.instFunLike {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :
                                  FunLike (α →+*o β) α β
                                  Equations
                                    instance OrderRingHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :
                                    OrderHomClass (α →+*o β) α β
                                    instance OrderRingHom.instRingHomClass {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :
                                    RingHomClass (α →+*o β) α β
                                    theorem OrderRingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                                    (↑f.toRingHom).toFun = f
                                    theorem OrderRingHom.ext {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] {f g : α →+*o β} (h : ∀ (a : α), f a = g a) :
                                    f = g
                                    theorem OrderRingHom.ext_iff {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] {f g : α →+*o β} :
                                    f = g ∀ (a : α), f a = g a
                                    @[simp]
                                    theorem OrderRingHom.toRingHom_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                                    f.toRingHom = f
                                    @[simp]
                                    @[simp]
                                    theorem OrderRingHom.coe_coe_ringHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                                    f = f
                                    @[simp]
                                    theorem OrderRingHom.coe_coe_orderAddMonoidHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                                    f = f
                                    @[simp]
                                    theorem OrderRingHom.coe_coe_orderMonoidWithZeroHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                                    f = f
                                    theorem OrderRingHom.coe_ringHom_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (a : α) :
                                    f a = f a
                                    theorem OrderRingHom.coe_orderAddMonoidHom_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (a : α) :
                                    f a = f a
                                    theorem OrderRingHom.coe_orderMonoidWithZeroHom_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (a : α) :
                                    f a = f a
                                    def OrderRingHom.copy {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (f' : αβ) (h : f' = f) :
                                    α →+*o β

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

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem OrderRingHom.coe_copy {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (f' : αβ) (h : f' = f) :
                                        (f.copy f' h) = f'
                                        theorem OrderRingHom.copy_eq {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (f' : αβ) (h : f' = f) :
                                        f.copy f' h = f
                                        def OrderRingHom.id (α : Type u_2) [NonAssocSemiring α] [Preorder α] :
                                        α →+*o α

                                        The identity as an ordered ring homomorphism.

                                        Equations
                                          Instances For
                                            Equations
                                              @[simp]
                                              theorem OrderRingHom.coe_id (α : Type u_2) [NonAssocSemiring α] [Preorder α] :
                                              @[simp]
                                              theorem OrderRingHom.id_apply {α : Type u_2} [NonAssocSemiring α] [Preorder α] (a : α) :
                                              def OrderRingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] (f : β →+*o γ) (g : α →+*o β) :
                                              α →+*o γ

                                              Composition of two OrderRingHoms as an OrderRingHom.

                                              Equations
                                                Instances For
                                                  @[simp]
                                                  theorem OrderRingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] (f : β →+*o γ) (g : α →+*o β) :
                                                  (f.comp g) = f g
                                                  @[simp]
                                                  theorem OrderRingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] (f : β →+*o γ) (g : α →+*o β) (a : α) :
                                                  (f.comp g) a = f (g a)
                                                  theorem OrderRingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] [NonAssocSemiring δ] [Preorder δ] (f : γ →+*o δ) (g : β →+*o γ) (h : α →+*o β) :
                                                  (f.comp g).comp h = f.comp (g.comp h)
                                                  @[simp]
                                                  theorem OrderRingHom.comp_id {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                                                  @[simp]
                                                  theorem OrderRingHom.id_comp {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                                                  @[simp]
                                                  theorem OrderRingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] {f₁ f₂ : β →+*o γ} {g : α →+*o β} (hg : Function.Surjective g) :
                                                  f₁.comp g = f₂.comp g f₁ = f₂
                                                  @[simp]
                                                  theorem OrderRingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] {f : β →+*o γ} {g₁ g₂ : α →+*o β} (hf : Function.Injective f) :
                                                  f.comp g₁ = f.comp g₂ g₁ = g₂
                                                  instance OrderRingHom.instPreorder {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :
                                                  Equations
                                                    Equations

                                                      Ordered ring isomorphisms #

                                                      def OrderRingIso.toOrderIso {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                                                      α ≃o β

                                                      Reinterpret an ordered ring isomorphism as an order isomorphism.

                                                      Equations
                                                        Instances For
                                                          instance OrderRingIso.instEquivLike {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
                                                          EquivLike (α ≃+*o β) α β
                                                          Equations
                                                            instance OrderRingIso.instOrderIsoClass {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
                                                            OrderIsoClass (α ≃+*o β) α β
                                                            instance OrderRingIso.instRingEquivClass {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
                                                            RingEquivClass (α ≃+*o β) α β
                                                            theorem OrderRingIso.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                                                            f.toFun = f
                                                            theorem OrderRingIso.ext {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] {f g : α ≃+*o β} (h : ∀ (a : α), f a = g a) :
                                                            f = g
                                                            theorem OrderRingIso.ext_iff {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] {f g : α ≃+*o β} :
                                                            f = g ∀ (a : α), f a = g a
                                                            @[simp]
                                                            theorem OrderRingIso.coe_mk {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+* β) (h : ∀ {a b : α}, e.toFun a e.toFun b a b) :
                                                            { toRingEquiv := e, map_le_map_iff' := h } = e
                                                            @[simp]
                                                            theorem OrderRingIso.mk_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) (h : ∀ {a b : α}, (↑e).toFun a (↑e).toFun b a b) :
                                                            { toRingEquiv := e, map_le_map_iff' := h } = e
                                                            @[simp]
                                                            theorem OrderRingIso.toRingEquiv_eq_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                                                            f.toRingEquiv = f
                                                            @[simp]
                                                            theorem OrderRingIso.toOrderIso_eq_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                                                            f = f
                                                            @[simp]
                                                            theorem OrderRingIso.coe_toRingEquiv {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                                                            f = f
                                                            @[simp]
                                                            theorem OrderRingIso.coe_toOrderIso {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                                                            f = f
                                                            def OrderRingIso.refl (α : Type u_2) [Mul α] [Add α] [LE α] :
                                                            α ≃+*o α

                                                            The identity map as an ordered ring isomorphism.

                                                            Equations
                                                              Instances For
                                                                instance OrderRingIso.instInhabited (α : Type u_2) [Mul α] [Add α] [LE α] :
                                                                Equations
                                                                  @[simp]
                                                                  theorem OrderRingIso.refl_apply (α : Type u_2) [Mul α] [Add α] [LE α] (x : α) :
                                                                  @[simp]
                                                                  theorem OrderRingIso.coe_ringEquiv_refl (α : Type u_2) [Mul α] [Add α] [LE α] :
                                                                  @[simp]
                                                                  theorem OrderRingIso.coe_orderIso_refl (α : Type u_2) [Mul α] [Add α] [LE α] :
                                                                  def OrderRingIso.symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
                                                                  β ≃+*o α

                                                                  The inverse of an ordered ring isomorphism as an ordered ring isomorphism.

                                                                  Equations
                                                                    Instances For
                                                                      def OrderRingIso.Simps.symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
                                                                      βα

                                                                      See Note [custom simps projection]

                                                                      Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem OrderRingIso.symm_symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
                                                                          e.symm.symm = e
                                                                          theorem OrderRingIso.symm_bijective {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
                                                                          def OrderRingIso.trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
                                                                          α ≃+*o γ

                                                                          Composition of OrderRingIsos as an OrderRingIso.

                                                                          Equations
                                                                            Instances For
                                                                              theorem OrderRingIso.trans_toRingEquiv {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) :

                                                                              This lemma used to be generated by [simps] on trans, but the lhs of this simplifies under simp. Removed [simps] attribute and added aux version below.

                                                                              @[simp]
                                                                              theorem OrderRingIso.trans_toRingEquiv_aux {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
                                                                              (f.trans g) = f.trans g.toRingEquiv

                                                                              simp-normal form of trans_toRingEquiv.

                                                                              @[simp]
                                                                              theorem OrderRingIso.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) (a : α) :
                                                                              (f.trans g) a = g (f a)
                                                                              @[simp]
                                                                              theorem OrderRingIso.self_trans_symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
                                                                              @[simp]
                                                                              theorem OrderRingIso.symm_trans_self {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
                                                                              def OrderRingIso.toOrderRingHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α ≃+*o β) :
                                                                              α →+*o β

                                                                              Reinterpret an ordered ring isomorphism as an ordered ring homomorphism.

                                                                              Equations
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem OrderRingIso.toOrderRingHom_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α ≃+*o β) :
                                                                                  @[simp]
                                                                                  theorem OrderRingIso.coe_toOrderRingHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α ≃+*o β) :
                                                                                  f = f