Ordered monoid and group homomorphisms

This file defines morphisms between (additive) ordered monoids.

Types of morphisms

• OrderAddMonoidHom: Ordered additive monoid homomorphisms.
• OrderMonoidHom: Ordered monoid homomorphisms.
• OrderAddMonoidIso: Ordered additive monoid isomorphisms.
• OrderMonoidIso: Ordered monoid isomorphisms.

Notation

• →+o: Bundled ordered additive monoid homs. Also use for additive group homs.
• →*o: Bundled ordered monoid homs. Also use for group homs.
• ≃+o: Bundled ordered additive monoid isos. Also use for additive group isos.
• ≃*o: Bundled ordered monoid isos. Also use for group isos.

Implementation notes

There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

There is no OrderGroupHom -- the idea is that OrderMonoidHom is used. The constructor for OrderMonoidHom needs a proof of map_one as well as map_mul; a separate constructor OrderMonoidHom.mk' will construct ordered group homs (i.e. ordered monoid homs between ordered groups) given only a proof that multiplication is preserved,

Implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type OrderMonoidHom. When they can be inferred from the type it is faster to use this method than to use type class inference.

Removed typeclasses

This file used to define typeclasses for order-preserving (additive) monoid homomorphisms: OrderAddMonoidHomClass, OrderMonoidHomClass, and OrderMonoidWithZeroHomClass.

In https://github.com/leanprover-community/mathlib4/pull/10544 we migrated from these typeclasses to assumptions like [FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N], making some definitions and lemmas irrelevant.

Tags

ordered monoid, ordered group

structure OrderAddMonoidHom (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] extends α →+ β : Type (max u_6 u_7)

α →+o β is the type of monotone functions α → β that preserve the OrderedAddCommMonoid structure.

OrderAddMonoidHom is also used for ordered group homomorphisms.

When possible, instead of parametrizing results over (f : α →+o β), you should parametrize over (F : Type*) [FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N] (f : F).

• toFun : α → β
• map_zero' : (↑self.toAddMonoidHom).toFun 0 = 0
• map_add' (x y : α) : (↑self.toAddMonoidHom).toFun (x + y) = (↑self.toAddMonoidHom).toFun x + (↑self.toAddMonoidHom).toFun y
• monotone' : Monotone (↑self.toAddMonoidHom).toFun

  An OrderAddMonoidHom is a monotone function.

def «term_→+o_» : Lean.TrailingParserDescr

Infix notation for OrderAddMonoidHom.

Equations

• «term_→+o_» = Lean.ParserDescr.trailingNode `«term_→+o_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →+o ") (Lean.ParserDescr.cat `term 25))

structure OrderAddMonoidIso (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [Add α] [Add β] extends α ≃+ β : Type (max u_6 u_7)

α ≃+o β is the type of monotone isomorphisms α ≃ β that preserve the OrderedAddCommMonoid structure.

OrderAddMonoidIso is also used for ordered group isomorphisms.

When possible, instead of parametrizing results over (f : α ≃+o β), you should parametrize over (F : Type*) [FunLike F M N] [AddEquivClass F M N] [OrderIsoClass F M N] (f : F).

• toFun : α → β
• invFun : β → α
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_add' (x y : α) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_le_map_iff' {a b : α} : self.toFun a ≤ self.toFun b ↔ a ≤ b

  An OrderAddMonoidIso respects ≤.

def «term_≃+o_» : Lean.TrailingParserDescr

Infix notation for OrderAddMonoidIso.

Equations

• «term_≃+o_» = Lean.ParserDescr.trailingNode `«term_≃+o_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃+o ") (Lean.ParserDescr.cat `term 25))

structure OrderMonoidHom (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] extends α →* β : Type (max u_6 u_7)

α →*o β is the type of functions α → β that preserve the OrderedCommMonoid structure.

OrderMonoidHom is also used for ordered group homomorphisms.

When possible, instead of parametrizing results over (f : α →*o β), you should parametrize over (F : Type*) [FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N] (f : F).

• toFun : α → β
• map_one' : (↑self.toMonoidHom).toFun 1 = 1
• map_mul' (x y : α) : (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
• monotone' : Monotone (↑self.toMonoidHom).toFun

  An OrderMonoidHom is a monotone function.

def «term_→*o_» : Lean.TrailingParserDescr

Infix notation for OrderMonoidHom.

Equations

• «term_→*o_» = Lean.ParserDescr.trailingNode `«term_→*o_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →*o ") (Lean.ParserDescr.cat `term 25))

def OrderMonoidHomClass.toOrderMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] [FunLike F α β] [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) : α →*o β

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

Equations

• ↑f = { toMonoidHom := ↑f, monotone' := ⋯ }

def OrderMonoidHomClass.toOrderAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [OrderHomClass F α β] [AddMonoidHomClass F α β] (f : F) : α →+o β

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

Equations

• ↑f = { toAddMonoidHom := ↑f, monotone' := ⋯ }

instance instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] [FunLike F α β] [OrderHomClass F α β] [MonoidHomClass F α β] : CoeTC F (α →*o β)

Any type satisfying OrderMonoidHomClass can be cast into OrderMonoidHom via OrderMonoidHomClass.toOrderMonoidHom.

Equations

• instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass = { coe := OrderMonoidHomClass.toOrderMonoidHom }

instance instCoeTCOrderAddMonoidHomOfOrderHomClassOfAddMonoidHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [OrderHomClass F α β] [AddMonoidHomClass F α β] : CoeTC F (α →+o β)

Any type satisfying OrderAddMonoidHomClass can be cast into OrderAddMonoidHom via OrderAddMonoidHomClass.toOrderAddMonoidHom.

Equations

• instCoeTCOrderAddMonoidHomOfOrderHomClassOfAddMonoidHomClass = { coe := OrderMonoidHomClass.toOrderAddMonoidHom }

structure OrderMonoidIso (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [Mul α] [Mul β] extends α ≃* β : Type (max u_6 u_7)

α ≃*o β is the type of isomorphisms α ≃ β that preserve the OrderedCommMonoid structure.

OrderMonoidIso is also used for ordered group isomorphisms.

When possible, instead of parametrizing results over (f : α ≃*o β), you should parametrize over (F : Type*) [FunLike F M N] [MulEquivClass F M N] [OrderIsoClass F M N] (f : F).

• toFun : α → β
• invFun : β → α
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_mul' (x y : α) : self.toFun (x * y) = self.toFun x * self.toFun y
• map_le_map_iff' {a b : α} : self.toFun a ≤ self.toFun b ↔ a ≤ b

  An OrderMonoidIso respects ≤.

def «term_≃*o_» : Lean.TrailingParserDescr

Infix notation for OrderMonoidIso.

Equations

• «term_≃*o_» = Lean.ParserDescr.trailingNode `«term_≃*o_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃*o ") (Lean.ParserDescr.cat `term 25))

def OrderMonoidIsoClass.toOrderMonoidIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] [EquivLike F α β] [OrderIsoClass F α β] [MulEquivClass F α β] (f : F) : α ≃*o β

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

Equations

• ↑f = { toMulEquiv := ↑f, map_le_map_iff' := ⋯ }

def OrderMonoidIsoClass.toOrderAddMonoidIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] [EquivLike F α β] [OrderIsoClass F α β] [AddEquivClass F α β] (f : F) : α ≃+o β

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

Equations

• ↑f = { toAddEquiv := ↑f, map_le_map_iff' := ⋯ }

instance instCoeTCOrderMonoidIsoOfOrderIsoClassOfMulEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] [EquivLike F α β] [OrderIsoClass F α β] [MulEquivClass F α β] : CoeTC F (α ≃*o β)

Any type satisfying OrderMonoidIsoClass can be cast into OrderMonoidIso via OrderMonoidIsoClass.toOrderMonoidIso.

Equations

• instCoeTCOrderMonoidIsoOfOrderIsoClassOfMulEquivClass = { coe := OrderMonoidIsoClass.toOrderMonoidIso }

instance instCoeTCOrderAddMonoidIsoOfOrderIsoClassOfAddEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] [EquivLike F α β] [OrderIsoClass F α β] [AddEquivClass F α β] : CoeTC F (α ≃+o β)

Any type satisfying OrderAddMonoidIsoClass can be cast into OrderAddMonoidIso via OrderAddMonoidIsoClass.toOrderAddMonoidIso.

Equations

• instCoeTCOrderAddMonoidIsoOfOrderIsoClassOfAddEquivClass = { coe := OrderMonoidIsoClass.toOrderAddMonoidIso }

theorem map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Preorder α] [Zero α] [Preorder β] [Zero β] [OrderHomClass F α β] [ZeroHomClass F α β] (f : F) {a : α} (ha : 0 ≤ a) : 0 ≤ f a

See also NonnegHomClass.apply_nonneg.

theorem map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Preorder α] [Zero α] [Preorder β] [Zero β] [OrderHomClass F α β] [ZeroHomClass F α β] (f : F) {a : α} (ha : a ≤ 0) : f a ≤ 0

theorem monotone_iff_map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : Monotone ⇑f ↔ ∀ (a : α), 0 ≤ a → 0 ≤ f a

theorem antitone_iff_map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : Antitone ⇑f ↔ ∀ (a : α), 0 ≤ a → f a ≤ 0

theorem monotone_iff_map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : Monotone ⇑f ↔ ∀ (a : α), a ≤ 0 → f a ≤ 0

theorem antitone_iff_map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : Antitone ⇑f ↔ ∀ (a : α), a ≤ 0 → 0 ≤ f a

theorem strictMono_iff_map_pos {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : StrictMono ⇑f ↔ ∀ (a : α), 0 < a → 0 < f a

theorem strictAnti_iff_map_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : StrictAnti ⇑f ↔ ∀ (a : α), 0 < a → f a < 0

theorem strictMono_iff_map_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : StrictMono ⇑f ↔ ∀ (a : α), a < 0 → f a < 0

theorem strictAnti_iff_map_pos {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : StrictAnti ⇑f ↔ ∀ (a : α), a < 0 → 0 < f a

instance OrderMonoidHom.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] : FunLike (α →*o β) α β

Equations

• OrderMonoidHom.instFunLike = { coe := fun (f : α →*o β) => (↑f.toMonoidHom).toFun, coe_injective' := ⋯ }

instance OrderAddMonoidHom.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] : FunLike (α →+o β) α β

Equations

• OrderAddMonoidHom.instFunLike = { coe := fun (f : α →+o β) => (↑f.toAddMonoidHom).toFun, coe_injective' := ⋯ }

instance OrderMonoidHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] : OrderHomClass (α →*o β) α β

instance OrderAddMonoidHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] : OrderHomClass (α →+o β) α β

instance OrderMonoidHom.instMonoidHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] : MonoidHomClass (α →*o β) α β

instance OrderAddMonoidHom.instAddMonoidHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] : AddMonoidHomClass (α →+o β) α β

theorem OrderMonoidHom.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] {f g : α →*o β} (h : ∀ (a : α), f a = g a) : f = g

theorem OrderAddMonoidHom.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] {f g : α →+o β} (h : ∀ (a : α), f a = g a) : f = g

theorem OrderMonoidHom.ext_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] {f g : α →*o β} : f = g ↔ ∀ (a : α), f a = g a

theorem OrderAddMonoidHom.ext_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] {f g : α →+o β} : f = g ↔ ∀ (a : α), f a = g a

theorem OrderMonoidHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) : (↑f.toMonoidHom).toFun = ⇑f

theorem OrderAddMonoidHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) : (↑f.toAddMonoidHom).toFun = ⇑f

@[simp]

theorem OrderMonoidHom.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →* β) (h : Monotone (↑f).toFun) : ⇑{ toMonoidHom := f, monotone' := h } = ⇑f

@[simp]

theorem OrderAddMonoidHom.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (h : Monotone (↑f).toFun) : ⇑{ toAddMonoidHom := f, monotone' := h } = ⇑f

@[simp]

theorem OrderMonoidHom.mk_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) (h : Monotone (↑↑f).toFun) : { toMonoidHom := ↑f, monotone' := h } = f

@[simp]

theorem OrderAddMonoidHom.mk_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) (h : Monotone (↑↑f).toFun) : { toAddMonoidHom := ↑f, monotone' := h } = f

def OrderMonoidHom.toOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) : α →o β

Reinterpret an ordered monoid homomorphism as an order homomorphism.

Equations

• f.toOrderHom = { toFun := (↑f.toMonoidHom).toFun, monotone' := ⋯ }

def OrderAddMonoidHom.toOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) : α →o β

Reinterpret an ordered additive monoid homomorphism as an order homomorphism.

Equations

• f.toOrderHom = { toFun := (↑f.toAddMonoidHom).toFun, monotone' := ⋯ }

@[simp]

theorem OrderMonoidHom.coe_monoidHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) : ⇑↑f = ⇑f

@[simp]

theorem OrderAddMonoidHom.coe_addMonoidHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) : ⇑↑f = ⇑f

@[simp]

theorem OrderMonoidHom.coe_orderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) : ⇑↑f = ⇑f

@[simp]

theorem OrderAddMonoidHom.coe_orderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) : ⇑↑f = ⇑f

theorem OrderMonoidHom.toMonoidHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] : Function.Injective toMonoidHom

theorem OrderAddMonoidHom.toAddMonoidHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] : Function.Injective toAddMonoidHom

theorem OrderMonoidHom.toOrderHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] : Function.Injective toOrderHom

theorem OrderAddMonoidHom.toOrderHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] : Function.Injective toOrderHom

def OrderMonoidHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) (f' : α → β) (h : f' = ⇑f) : α →*o β

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

Equations

• f.copy f' h = { toFun := f', map_one' := ⋯, map_mul' := ⋯, monotone' := ⋯ }

def OrderAddMonoidHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) (f' : α → β) (h : f' = ⇑f) : α →+o β

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

Equations

• f.copy f' h = { toFun := f', map_zero' := ⋯, map_add' := ⋯, monotone' := ⋯ }

@[simp]

theorem OrderMonoidHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

@[simp]

theorem OrderAddMonoidHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem OrderMonoidHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

theorem OrderAddMonoidHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

def OrderMonoidHom.id (α : Type u_2) [Preorder α] [MulOneClass α] : α →*o α

The identity map as an ordered monoid homomorphism.

Equations

• OrderMonoidHom.id α = { toMonoidHom := MonoidHom.id α, monotone' := ⋯ }

def OrderAddMonoidHom.id (α : Type u_2) [Preorder α] [AddZeroClass α] : α →+o α

The identity map as an ordered additive monoid homomorphism.

Equations

• OrderAddMonoidHom.id α = { toAddMonoidHom := AddMonoidHom.id α, monotone' := ⋯ }

@[simp]

theorem OrderMonoidHom.coe_id (α : Type u_2) [Preorder α] [MulOneClass α] : ⇑(OrderMonoidHom.id α) = id

@[simp]

theorem OrderAddMonoidHom.coe_id (α : Type u_2) [Preorder α] [AddZeroClass α] : ⇑(OrderAddMonoidHom.id α) = id

instance OrderMonoidHom.instInhabited (α : Type u_2) [Preorder α] [MulOneClass α] : Inhabited (α →*o α)

Equations

• OrderMonoidHom.instInhabited α = { default := OrderMonoidHom.id α }

instance OrderAddMonoidHom.instInhabited (α : Type u_2) [Preorder α] [AddZeroClass α] : Inhabited (α →+o α)

Equations

• OrderAddMonoidHom.instInhabited α = { default := OrderAddMonoidHom.id α }

def OrderMonoidHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) (g : α →*o β) : α →*o γ

Composition of OrderMonoidHoms as an OrderMonoidHom.

Equations

• f.comp g = { toMonoidHom := f.comp ↑g, monotone' := ⋯ }

def OrderAddMonoidHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) (g : α →+o β) : α →+o γ

Composition of OrderAddMonoidHoms as an OrderAddMonoidHom

Equations

• f.comp g = { toAddMonoidHom := f.comp ↑g, monotone' := ⋯ }

@[simp]

theorem OrderMonoidHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) (g : α →*o β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem OrderAddMonoidHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) (g : α →+o β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem OrderMonoidHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) (g : α →*o β) (a : α) : (f.comp g) a = f (g a)

@[simp]

theorem OrderAddMonoidHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) (g : α →+o β) (a : α) : (f.comp g) a = f (g a)

theorem OrderMonoidHom.coe_comp_monoidHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) (g : α →*o β) : ↑(f.comp g) = (↑f).comp ↑g

theorem OrderAddMonoidHom.coe_comp_addMonoidHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) (g : α →+o β) : ↑(f.comp g) = (↑f).comp ↑g

theorem OrderMonoidHom.coe_comp_orderHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) (g : α →*o β) : ↑(f.comp g) = (↑f).comp ↑g

theorem OrderAddMonoidHom.coe_comp_orderHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) (g : α →+o β) : ↑(f.comp g) = (↑f).comp ↑g

@[simp]

theorem OrderMonoidHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] [MulOneClass δ] (f : γ →*o δ) (g : β →*o γ) (h : α →*o β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem OrderAddMonoidHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] [AddZeroClass δ] (f : γ →+o δ) (g : β →+o γ) (h : α →+o β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem OrderMonoidHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) : f.comp (OrderMonoidHom.id α) = f

@[simp]

theorem OrderAddMonoidHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) : f.comp (OrderAddMonoidHom.id α) = f

@[simp]

theorem OrderMonoidHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) : (OrderMonoidHom.id β).comp f = f

@[simp]

theorem OrderAddMonoidHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) : (OrderAddMonoidHom.id β).comp f = f

@[simp]

theorem OrderMonoidHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] {g₁ g₂ : β →*o γ} {f : α →*o β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem OrderAddMonoidHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] {g₁ g₂ : β →+o γ} {f : α →+o β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem OrderMonoidHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] {g : β →*o γ} {f₁ f₂ : α →*o β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

@[simp]

theorem OrderAddMonoidHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] {g : β →+o γ} {f₁ f₂ : α →+o β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

instance OrderMonoidHom.instOne {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] : One (α →*o β)

1 is the homomorphism sending all elements to 1.

Equations

• OrderMonoidHom.instOne = { one := let __src := 1; { toMonoidHom := __src, monotone' := ⋯ } }

instance OrderAddMonoidHom.instZero {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] : Zero (α →+o β)

0 is the homomorphism sending all elements to 0.

Equations

• OrderAddMonoidHom.instZero = { zero := let __src := 0; { toAddMonoidHom := __src, monotone' := ⋯ } }

@[simp]

theorem OrderMonoidHom.coe_one {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] : ⇑1 = 1

@[simp]

theorem OrderAddMonoidHom.coe_zero {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] : ⇑0 = 0

@[simp]

theorem OrderMonoidHom.one_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (a : α) : 1 a = 1

@[simp]

theorem OrderAddMonoidHom.zero_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (a : α) : 0 a = 0

@[simp]

theorem OrderMonoidHom.one_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →*o β) : comp 1 f = 1

@[simp]

theorem OrderAddMonoidHom.zero_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : α →+o β) : comp 0 f = 0

@[simp]

theorem OrderMonoidHom.comp_one {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) : f.comp 1 = 1

@[simp]

theorem OrderAddMonoidHom.comp_zero {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) : f.comp 0 = 0

instance OrderMonoidHom.instMulOfIsOrderedMonoid {α : Type u_2} {β : Type u_3} [CommMonoid α] [PartialOrder α] [CommMonoid β] [PartialOrder β] [IsOrderedMonoid β] : Mul (α →*o β)

For two ordered monoid morphisms f and g, their product is the ordered monoid morphism sending a to f a * g a.

Equations

• OrderMonoidHom.instMulOfIsOrderedMonoid = { mul := fun (f g : α →*o β) => let __src := ↑f * ↑g; { toMonoidHom := __src, monotone' := ⋯ } }

instance OrderAddMonoidHom.instAddOfIsOrderedAddMonoid {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] : Add (α →+o β)

For two ordered additive monoid morphisms f and g, their product is the ordered additive monoid morphism sending a to f a + g a.

Equations

• OrderAddMonoidHom.instAddOfIsOrderedAddMonoid = { add := fun (f g : α →+o β) => let __src := ↑f + ↑g; { toAddMonoidHom := __src, monotone' := ⋯ } }

@[simp]

theorem OrderMonoidHom.coe_mul {α : Type u_2} {β : Type u_3} [CommMonoid α] [PartialOrder α] [CommMonoid β] [PartialOrder β] [IsOrderedMonoid β] (f g : α →*o β) : ⇑(f * g) = ⇑f * ⇑g

@[simp]

theorem OrderAddMonoidHom.coe_add {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] (f g : α →+o β) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem OrderMonoidHom.mul_apply {α : Type u_2} {β : Type u_3} [CommMonoid α] [PartialOrder α] [CommMonoid β] [PartialOrder β] [IsOrderedMonoid β] (f g : α →*o β) (a : α) : (f * g) a = f a * g a

@[simp]

theorem OrderAddMonoidHom.add_apply {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] (f g : α →+o β) (a : α) : (f + g) a = f a + g a

theorem OrderMonoidHom.mul_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [PartialOrder α] [CommMonoid β] [PartialOrder β] [CommMonoid γ] [PartialOrder γ] [IsOrderedMonoid γ] (g₁ g₂ : β →*o γ) (f : α →*o β) : (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

theorem OrderAddMonoidHom.add_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [AddCommMonoid γ] [PartialOrder γ] [IsOrderedAddMonoid γ] (g₁ g₂ : β →+o γ) (f : α →+o β) : (g₁ + g₂).comp f = g₁.comp f + g₂.comp f

theorem OrderMonoidHom.comp_mul {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [PartialOrder α] [CommMonoid β] [PartialOrder β] [CommMonoid γ] [PartialOrder γ] [IsOrderedMonoid β] [IsOrderedMonoid γ] (g : β →*o γ) (f₁ f₂ : α →*o β) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

theorem OrderAddMonoidHom.comp_add {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [AddCommMonoid γ] [PartialOrder γ] [IsOrderedAddMonoid β] [IsOrderedAddMonoid γ] (g : β →+o γ) (f₁ f₂ : α →+o β) : g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂

@[simp]

theorem OrderMonoidHom.toMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} {x✝ : Preorder α} {x✝¹ : Preorder β} {x✝² : MulOneClass α} {x✝³ : MulOneClass β} (f : α →*o β) : f.toMonoidHom = ↑f

@[simp]

theorem OrderAddMonoidHom.toAddMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} {x✝ : Preorder α} {x✝¹ : Preorder β} {x✝² : AddZeroClass α} {x✝³ : AddZeroClass β} (f : α →+o β) : f.toAddMonoidHom = ↑f

@[simp]

theorem OrderMonoidHom.toOrderHom_eq_coe {α : Type u_2} {β : Type u_3} {x✝ : Preorder α} {x✝¹ : Preorder β} {x✝² : MulOneClass α} {x✝³ : MulOneClass β} (f : α →*o β) : f.toOrderHom = ↑f

@[simp]

theorem OrderAddMonoidHom.toOrderHom_eq_coe {α : Type u_2} {β : Type u_3} {x✝ : Preorder α} {x✝¹ : Preorder β} {x✝² : AddZeroClass α} {x✝³ : AddZeroClass β} (f : α →+o β) : f.toOrderHom = ↑f

def OrderMonoidHom.mk' {α : Type u_2} {β : Type u_3} {x✝ : CommGroup α} {x✝¹ : PartialOrder α} {x✝² : CommGroup β} {x✝³ : PartialOrder β} (f : α → β) (hf : Monotone f) (map_mul : ∀ (a b : α), f (a * b) = f a * f b) : α →*o β

Makes an ordered group homomorphism from a proof that the map preserves multiplication.

Equations

• OrderMonoidHom.mk' f hf map_mul = { toMonoidHom := MonoidHom.mk' f map_mul, monotone' := hf }

def OrderAddMonoidHom.mk' {α : Type u_2} {β : Type u_3} {x✝ : AddCommGroup α} {x✝¹ : PartialOrder α} {x✝² : AddCommGroup β} {x✝³ : PartialOrder β} (f : α → β) (hf : Monotone f) (map_add : ∀ (a b : α), f (a + b) = f a + f b) : α →+o β

Makes an ordered additive group homomorphism from a proof that the map preserves addition.

Equations

• OrderAddMonoidHom.mk' f hf map_mul = { toAddMonoidHom := AddMonoidHom.mk' f map_mul, monotone' := hf }

instance OrderMonoidIso.instEquivLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] : EquivLike (α ≃*o β) α β

Equations

• OrderMonoidIso.instEquivLike = { coe := fun (f : α ≃*o β) => f.toFun, inv := fun (f : α ≃*o β) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance OrderAddMonoidIso.instEquivLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] : EquivLike (α ≃+o β) α β

Equations

• OrderAddMonoidIso.instEquivLike = { coe := fun (f : α ≃+o β) => f.toFun, inv := fun (f : α ≃+o β) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance OrderMonoidIso.instOrderIsoClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] : OrderIsoClass (α ≃*o β) α β

instance OrderAddMonoidIso.instOrderIsoClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] : OrderIsoClass (α ≃+o β) α β

instance OrderMonoidIso.instMulEquivClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] : MulEquivClass (α ≃*o β) α β

instance OrderAddMonoidIso.instAddEquivClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] : AddEquivClass (α ≃+o β) α β

theorem OrderMonoidIso.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] {f g : α ≃*o β} (h : ∀ (a : α), f a = g a) : f = g

theorem OrderAddMonoidIso.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] {f g : α ≃+o β} (h : ∀ (a : α), f a = g a) : f = g

theorem OrderAddMonoidIso.ext_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] {f g : α ≃+o β} : f = g ↔ ∀ (a : α), f a = g a

theorem OrderMonoidIso.ext_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] {f g : α ≃*o β} : f = g ↔ ∀ (a : α), f a = g a

theorem OrderMonoidIso.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : f.toFun = ⇑f

theorem OrderAddMonoidIso.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : f.toFun = ⇑f

@[simp]

theorem OrderMonoidIso.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃* β) (h : ∀ {a b : α}, f.toFun a ≤ f.toFun b ↔ a ≤ b) : ⇑{ toMulEquiv := f, map_le_map_iff' := h } = ⇑f

@[simp]

theorem OrderAddMonoidIso.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+ β) (h : ∀ {a b : α}, f.toFun a ≤ f.toFun b ↔ a ≤ b) : ⇑{ toAddEquiv := f, map_le_map_iff' := h } = ⇑f

@[simp]

theorem OrderMonoidIso.mk_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) (h : ∀ {a b : α}, (↑f).toFun a ≤ (↑f).toFun b ↔ a ≤ b) : { toMulEquiv := ↑f, map_le_map_iff' := h } = f

@[simp]

theorem OrderAddMonoidIso.mk_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) (h : ∀ {a b : α}, (↑f).toFun a ≤ (↑f).toFun b ↔ a ≤ b) : { toAddEquiv := ↑f, map_le_map_iff' := h } = f

def OrderMonoidIso.toOrderIso {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : α ≃o β

Reinterpret an ordered monoid isomorphism as an order isomorphism.

Equations

• f.toOrderIso = { toEquiv := f.toEquiv, map_rel_iff' := ⋯ }

def OrderAddMonoidIso.toOrderIso {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : α ≃o β

Reinterpret an ordered additive monoid isomomorphism as an order isomomorphism.

Equations

• f.toOrderIso = { toEquiv := f.toEquiv, map_rel_iff' := ⋯ }

@[simp]

theorem OrderMonoidIso.coe_mulEquiv {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : ⇑↑f = ⇑f

@[simp]

theorem OrderAddMonoidIso.coe_addEquiv {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : ⇑↑f = ⇑f

@[simp]

theorem OrderMonoidIso.coe_orderIso {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : ⇑↑f = ⇑f

@[simp]

theorem OrderAddMonoidIso.coe_orderIso {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : ⇑↑f = ⇑f

theorem OrderMonoidIso.toMulEquiv_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] : Function.Injective toMulEquiv

theorem OrderAddMonoidIso.toAddEquiv_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] : Function.Injective toAddEquiv

theorem OrderMonoidIso.toOrderIso_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] : Function.Injective toOrderIso

theorem OrderAddMonoidIso.toOrderIso_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] : Function.Injective toOrderIso

def OrderMonoidIso.refl (α : Type u_2) [Preorder α] [Mul α] : α ≃*o α

The identity map as an ordered monoid isomorphism.

Equations

• OrderMonoidIso.refl α = { toMulEquiv := MulEquiv.refl α, map_le_map_iff' := ⋯ }

def OrderAddMonoidIso.refl (α : Type u_2) [Preorder α] [Add α] : α ≃+o α

The identity map as an ordered additive monoid isomorphism.

Equations

• OrderAddMonoidIso.refl α = { toAddEquiv := AddEquiv.refl α, map_le_map_iff' := ⋯ }

@[simp]

theorem OrderMonoidIso.coe_refl (α : Type u_2) [Preorder α] [Mul α] : ⇑(OrderMonoidIso.refl α) = id

@[simp]

theorem OrderAddMonoidIso.coe_refl (α : Type u_2) [Preorder α] [Add α] : ⇑(OrderAddMonoidIso.refl α) = id

instance OrderMonoidIso.instInhabited (α : Type u_2) [Preorder α] [Mul α] : Inhabited (α ≃*o α)

Equations

• OrderMonoidIso.instInhabited α = { default := OrderMonoidIso.refl α }

instance OrderAddMonoidIso.instInhabited (α : Type u_2) [Preorder α] [Add α] : Inhabited (α ≃+o α)

Equations

• OrderAddMonoidIso.instInhabited α = { default := OrderAddMonoidIso.refl α }

def OrderMonoidIso.trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Mul α] [Mul β] [Mul γ] (f : α ≃*o β) (g : β ≃*o γ) : α ≃*o γ

Transitivity of multiplication-preserving order isomorphisms

Equations

• f.trans g = { toMulEquiv := (↑f).trans ↑g, map_le_map_iff' := ⋯ }

def OrderAddMonoidIso.trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Add α] [Add β] [Add γ] (f : α ≃+o β) (g : β ≃+o γ) : α ≃+o γ

Transitivity of addition-preserving order isomorphisms

Equations

• f.trans g = { toAddEquiv := (↑f).trans ↑g, map_le_map_iff' := ⋯ }

@[simp]

theorem OrderMonoidIso.coe_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Mul α] [Mul β] [Mul γ] (f : α ≃*o β) (g : β ≃*o γ) : ⇑(f.trans g) = ⇑g ∘ ⇑f

@[simp]

theorem OrderAddMonoidIso.coe_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Add α] [Add β] [Add γ] (f : α ≃+o β) (g : β ≃+o γ) : ⇑(f.trans g) = ⇑g ∘ ⇑f

@[simp]

theorem OrderMonoidIso.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Mul α] [Mul β] [Mul γ] (f : α ≃*o β) (g : β ≃*o γ) (a : α) : (f.trans g) a = g (f a)

@[simp]

theorem OrderAddMonoidIso.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Add α] [Add β] [Add γ] (f : α ≃+o β) (g : β ≃+o γ) (a : α) : (f.trans g) a = g (f a)

theorem OrderMonoidIso.coe_trans_mulEquiv {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Mul α] [Mul β] [Mul γ] (f : α ≃*o β) (g : β ≃*o γ) : ↑(f.trans g) = (↑f).trans ↑g

theorem OrderAddMonoidIso.coe_trans_addEquiv {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Add α] [Add β] [Add γ] (f : α ≃+o β) (g : β ≃+o γ) : ↑(f.trans g) = (↑f).trans ↑g

theorem OrderMonoidIso.coe_trans_orderIso {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Mul α] [Mul β] [Mul γ] (f : α ≃*o β) (g : β ≃*o γ) : ↑(f.trans g) = (↑f).trans ↑g

theorem OrderAddMonoidIso.coe_trans_orderIso {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Add α] [Add β] [Add γ] (f : α ≃+o β) (g : β ≃+o γ) : ↑(f.trans g) = (↑f).trans ↑g

@[simp]

theorem OrderMonoidIso.trans_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [Mul α] [Mul β] [Mul γ] [Mul δ] (f : α ≃*o β) (g : β ≃*o γ) (h : γ ≃*o δ) : (f.trans g).trans h = f.trans (g.trans h)

@[simp]

theorem OrderAddMonoidIso.trans_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [Add α] [Add β] [Add γ] [Add δ] (f : α ≃+o β) (g : β ≃+o γ) (h : γ ≃+o δ) : (f.trans g).trans h = f.trans (g.trans h)

@[simp]

theorem OrderMonoidIso.trans_refl {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : f.trans (OrderMonoidIso.refl β) = f

@[simp]

theorem OrderAddMonoidIso.trans_refl {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : f.trans (OrderAddMonoidIso.refl β) = f

@[simp]

theorem OrderMonoidIso.refl_trans {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : (OrderMonoidIso.refl α).trans f = f

@[simp]

theorem OrderAddMonoidIso.refl_trans {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : (OrderAddMonoidIso.refl α).trans f = f

@[simp]

theorem OrderMonoidIso.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Mul α] [Mul β] [Mul γ] {g₁ g₂ : α ≃*o β} {f : β ≃*o γ} (hf : Function.Injective ⇑f) : g₁.trans f = g₂.trans f ↔ g₁ = g₂

@[simp]

theorem OrderAddMonoidIso.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Add α] [Add β] [Add γ] {g₁ g₂ : α ≃+o β} {f : β ≃+o γ} (hf : Function.Injective ⇑f) : g₁.trans f = g₂.trans f ↔ g₁ = g₂

@[simp]

theorem OrderMonoidIso.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Mul α] [Mul β] [Mul γ] {g : α ≃*o β} {f₁ f₂ : β ≃*o γ} (hg : Function.Surjective ⇑g) : g.trans f₁ = g.trans f₂ ↔ f₁ = f₂

@[simp]

theorem OrderAddMonoidIso.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Add α] [Add β] [Add γ] {g : α ≃+o β} {f₁ f₂ : β ≃+o γ} (hg : Function.Surjective ⇑g) : g.trans f₁ = g.trans f₂ ↔ f₁ = f₂

@[simp]

theorem OrderMonoidIso.toMulEquiv_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : f.toMulEquiv = ↑f

@[simp]

theorem OrderAddMonoidIso.toAddEquiv_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : f.toAddEquiv = ↑f

@[simp]

theorem OrderMonoidIso.toOrderIso_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : f.toOrderIso = ↑f

@[simp]

theorem OrderAddMonoidIso.toOrderIso_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : f.toOrderIso = ↑f

def OrderMonoidIso.symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : β ≃*o α

The inverse of an isomorphism is an isomorphism.

Equations

• f.symm = { toMulEquiv := f.symm, map_le_map_iff' := ⋯ }

def OrderAddMonoidIso.symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : β ≃+o α

The inverse of an order isomorphism is an order isomorphism.

Equations

• f.symm = { toAddEquiv := f.symm, map_le_map_iff' := ⋯ }

def OrderMonoidIso.Simps.apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (h : α ≃*o β) : α → β

See Note [custom simps projection].

Equations

• OrderMonoidIso.Simps.apply h = ⇑h

def OrderAddMonoidIso.Simps.apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (h : α ≃+o β) : α → β

See Note [custom simps projection].

Equations

• OrderAddMonoidIso.Simps.apply h = ⇑h

def OrderMonoidIso.Simps.symm_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (h : α ≃*o β) : β → α

See Note [custom simps projection]

Equations

• OrderMonoidIso.Simps.symm_apply h = ⇑h.symm

def OrderAddMonoidIso.Simps.symm_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (h : α ≃+o β) : β → α

See Note [custom simps projection].

Equations

• OrderAddMonoidIso.Simps.symm_apply h = ⇑h.symm

theorem OrderMonoidIso.invFun_eq_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] {f : α ≃*o β} : f.invFun = ⇑f.symm

theorem OrderAddMonoidIso.invFun_eq_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] {f : α ≃+o β} : f.invFun = ⇑f.symm

@[simp]

theorem OrderMonoidIso.coe_toEquiv_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : ⇑(↑f).symm = ⇑f.symm

simp-normal form of invFun_eq_symm.

@[simp]

theorem OrderAddMonoidIso.coe_toEquiv_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : ⇑(↑f).symm = ⇑f.symm

@[simp]

theorem OrderMonoidIso.equivLike_inv_eq_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : EquivLike.inv f = ⇑f.symm

@[simp]

theorem OrderAddMonoidIso.equivLike_neg_eq_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : EquivLike.inv f = ⇑f.symm

@[simp]

theorem OrderMonoidIso.toEquiv_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : ↑f.symm = (↑f).symm

@[simp]

theorem OrderAddMonoidIso.toEquiv_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : ↑f.symm = (↑f).symm

@[simp]

theorem OrderMonoidIso.symm_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : f.symm.symm = f

@[simp]

theorem OrderAddMonoidIso.symm_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : f.symm.symm = f

theorem OrderMonoidIso.symm_bijective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] : Function.Bijective symm

theorem OrderAddMonoidIso.symm_bijective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] : Function.Bijective symm

@[simp]

theorem OrderMonoidIso.refl_symm {α : Type u_2} [Preorder α] [Mul α] : (OrderMonoidIso.refl α).symm = OrderMonoidIso.refl α

@[simp]

theorem OrderAddMonoidIso.refl_symm {α : Type u_2} [Preorder α] [Add α] : (OrderAddMonoidIso.refl α).symm = OrderAddMonoidIso.refl α

@[simp]

theorem OrderMonoidIso.apply_symm_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) (y : β) : e (e.symm y) = y

e.symm is a right inverse of e, written as e (e.symm y) = y.

@[simp]

theorem OrderAddMonoidIso.apply_symm_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) (y : β) : e (e.symm y) = y

e.symm is a right inverse of e, written as e (e.symm y) = y.

@[simp]

theorem OrderMonoidIso.symm_apply_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) (x : α) : e.symm (e x) = x

e.symm is a left inverse of e, written as e.symm (e y) = y.

@[simp]

theorem OrderAddMonoidIso.symm_apply_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) (x : α) : e.symm (e x) = x

e.symm is a left inverse of e, written as e.symm (e y) = y.

@[simp]

theorem OrderMonoidIso.symm_comp_self {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) : ⇑e.symm ∘ ⇑e = id

@[simp]

theorem OrderAddMonoidIso.symm_comp_self {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) : ⇑e.symm ∘ ⇑e = id

@[simp]

theorem OrderMonoidIso.self_comp_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) : ⇑e ∘ ⇑e.symm = id

@[simp]

theorem OrderAddMonoidIso.self_comp_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) : ⇑e ∘ ⇑e.symm = id

theorem OrderMonoidIso.apply_eq_iff_symm_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) {x : α} {y : β} : e x = y ↔ x = e.symm y

theorem OrderAddMonoidIso.apply_eq_iff_symm_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) {x : α} {y : β} : e x = y ↔ x = e.symm y

theorem OrderMonoidIso.symm_apply_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) {x : β} {y : α} : e.symm x = y ↔ x = e y

theorem OrderAddMonoidIso.symm_apply_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) {x : β} {y : α} : e.symm x = y ↔ x = e y

theorem OrderMonoidIso.eq_symm_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) {x : β} {y : α} : y = e.symm x ↔ e y = x

theorem OrderAddMonoidIso.eq_symm_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) {x : β} {y : α} : y = e.symm x ↔ e y = x

theorem OrderMonoidIso.eq_comp_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) (f : β → α) (g : α → α) : f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g

theorem OrderAddMonoidIso.eq_comp_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) (f : β → α) (g : α → α) : f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g

theorem OrderMonoidIso.comp_symm_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) (f : β → α) (g : α → α) : g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e

theorem OrderAddMonoidIso.comp_symm_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) (f : β → α) (g : α → α) : g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e

theorem OrderMonoidIso.eq_symm_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) (f : α → α) (g : α → β) : f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g

theorem OrderAddMonoidIso.eq_symm_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) (f : α → α) (g : α → β) : f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g

theorem OrderMonoidIso.symm_comp_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) (f : α → α) (g : α → β) : ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f

theorem OrderAddMonoidIso.symm_comp_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) (f : α → α) (g : α → β) : ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f

theorem OrderMonoidIso.strictMono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : StrictMono ⇑f

theorem OrderAddMonoidIso.strictMono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : StrictMono ⇑f

theorem OrderMonoidIso.strictMono_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (f : α ≃*o β) : StrictMono ⇑f.symm

theorem OrderAddMonoidIso.strictMono_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (f : α ≃+o β) : StrictMono ⇑f.symm

def OrderMonoidIso.mk' {α : Type u_2} {β : Type u_3} {x✝ : CommGroup α} {x✝¹ : PartialOrder α} {x✝² : CommGroup β} {x✝³ : PartialOrder β} (f : α ≃ β) (hf : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b) (map_mul : ∀ (a b : α), f (a * b) = f a * f b) : α ≃*o β

Makes an ordered group isomorphism from a proof that the map preserves multiplication.

Equations

• OrderMonoidIso.mk' f hf map_mul = { toMulEquiv := MulEquiv.mk' f map_mul, map_le_map_iff' := ⋯ }

def OrderAddMonoidIso.mk' {α : Type u_2} {β : Type u_3} {x✝ : AddCommGroup α} {x✝¹ : PartialOrder α} {x✝² : AddCommGroup β} {x✝³ : PartialOrder β} (f : α ≃ β) (hf : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b) (map_add : ∀ (a b : α), f (a + b) = f a + f b) : α ≃+o β

Makes an ordered additive group isomorphism from a proof that the map preserves addition.

Equations

• OrderAddMonoidIso.mk' f hf map_mul = { toAddEquiv := AddEquiv.mk' f map_mul, map_le_map_iff' := ⋯ }