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.
• OrderMonoidWithZeroHom: Ordered monoid with zero homomorphisms.

Typeclasses

• OrderAddMonoidHomClass
• OrderMonoidHomClass
• OrderMonoidWithZeroHomClass

Notation

• →+o→+o: Bundled ordered additive monoid homs. Also use for additive groups homs.
• →*o→*o: Bundled ordered monoid homs. Also use for groups homs.
• →*₀o→*₀o: Bundled ordered monoid with zero homs. Also use for groups with zero homs.

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.

Tags

ordered monoid, ordered group, monoid with zero

ink

structure OrderAddMonoidHom (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] extends AddMonoidHom : Type (maxu_1u_2)

• An OrderAddMonoidHom is a monotone function.

  monotone' : Monotone (↑toAddMonoidHom).toFun

α →+o β→+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 β)→+o β), you should parametrize over (F : Type _) [OrderAddMonoidHomClass F α β] (f : F).

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

ink

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))

ink

class OrderAddMonoidHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] extends AddMonoidHomClass : Type (max(maxu_1u_2)u_3)

• An OrderAddMonoidHom is a monotone function.

  monotone : ∀ (f : F), Monotone ↑f

OrderAddMonoidHomClass F α β states that F is a type of ordered monoid homomorphisms.

You should also extend this typeclass when you extend OrderAddMonoidHom.

ink

structure OrderMonoidHom (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] extends MonoidHom : Type (maxu_1u_2)

• An OrderMonoidHom is a monotone function.

  monotone' : Monotone (↑toMonoidHom).toFun

α →*o β→*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 β)→*o β), you should parametrize over (F : Type _) [OrderMonoidHomClass F α β] (f : F).

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

ink

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))

ink

class OrderMonoidHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] extends MonoidHomClass : Type (max(maxu_1u_2)u_3)

• An OrderMonoidHom is a monotone function.

  monotone : ∀ (f : F), Monotone ↑f

OrderMonoidHomClass F α β states that F is a type of ordered monoid homomorphisms.

You should also extend this typeclass when you extend OrderMonoidHom.

ink

def OrderAddMonoidHomClass.toOrderAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : Preorder α} → {x_1 : Preorder β} → {x_2 : AddZeroClass α} → {x_3 : AddZeroClass β} → [inst : OrderAddMonoidHomClass F α β] → F → α →+o β

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

Equations

• One or more equations did not get rendered due to their size.

ink

def OrderMonoidHomClass.toOrderMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : Preorder α} → {x_1 : Preorder β} → {x_2 : MulOneClass α} → {x_3 : MulOneClass β} → [inst : OrderMonoidHomClass F α β] → F → α →*o β

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

Equations

• One or more equations did not get rendered due to their size.

ink

instance OrderAddMonoidHomClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : Preorder α} → {x_1 : Preorder β} → {x_2 : AddZeroClass α} → {x_3 : AddZeroClass β} → [inst : OrderAddMonoidHomClass F α β] → OrderHomClass F α β

Equations

• OrderAddMonoidHomClass.toOrderHomClass = let src := inst; RelHomClass.mk (_ : ∀ (f : F), Monotone ↑f)

ink

instance OrderMonoidHomClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : Preorder α} → {x_1 : Preorder β} → {x_2 : MulOneClass α} → {x_3 : MulOneClass β} → [inst : OrderMonoidHomClass F α β] → OrderHomClass F α β

Equations

• OrderMonoidHomClass.toOrderHomClass = let src := inst; RelHomClass.mk (_ : ∀ (f : F), Monotone ↑f)

ink

instance instCoeTCOrderAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : Preorder α} → {x_1 : Preorder β} → {x_2 : AddZeroClass α} → {x_3 : AddZeroClass β} → [inst : OrderAddMonoidHomClass F α β] → CoeTC F (α →+o β)

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

Equations

• instCoeTCOrderAddMonoidHom = { coe := OrderAddMonoidHomClass.toOrderAddMonoidHom }

ink

instance instCoeTCOrderMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : Preorder α} → {x_1 : Preorder β} → {x_2 : MulOneClass α} → {x_3 : MulOneClass β} → [inst : OrderMonoidHomClass F α β] → CoeTC F (α →*o β)

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

Equations

• instCoeTCOrderMonoidHom = { coe := OrderMonoidHomClass.toOrderMonoidHom }

ink

structure OrderMonoidWithZeroHom (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] extends MonoidWithZeroHom : Type (maxu_1u_2)

• An OrderMonoidWithZeroHom is a monotone function.

  monotone' : Monotone (↑toMonoidWithZeroHom).toFun

OrderMonoidWithZeroHom α β is the type of functions α → β→ β that preserve the MonoidWithZero structure.

OrderMonoidWithZeroHom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : α →+ β)→+ β), you should parametrize over (F : Type _) [OrderMonoidWithZeroHomClass F α β] (f : F).

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

ink

def «term_→*₀o_» : Lean.TrailingParserDescr

Infix notation for OrderMonoidWithZeroHom.

Equations

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

ink

class OrderMonoidWithZeroHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] extends MonoidWithZeroHomClass : Type (max(maxu_1u_2)u_3)

• An OrderMonoidWithZeroHom is a monotone function.

  monotone : ∀ (f : F), Monotone ↑f

OrderMonoidWithZeroHomClass F α β states that F is a type of ordered monoid with zero homomorphisms.

You should also extend this typeclass when you extend OrderMonoidWithZeroHom.

ink

def OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : OrderMonoidWithZeroHomClass F α β] (f : F) : α →*₀o β

Turn an element of a type F satisfying OrderMonoidWithZeroHomClass F α β into an actual OrderMonoidWithZeroHom. This is declared as the default coercion from F to α →+*₀o β→+*₀o β.

Equations

• One or more equations did not get rendered due to their size.

ink

instance OrderMonoidWithZeroHomClass.toOrderMonoidHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : Preorder α} → {x_1 : Preorder β} → {x_2 : MulZeroOneClass α} → {x_3 : MulZeroOneClass β} → [inst : OrderMonoidWithZeroHomClass F α β] → OrderMonoidHomClass F α β

Equations

• OrderMonoidWithZeroHomClass.toOrderMonoidHomClass = let src := inst; OrderMonoidHomClass.mk (_ : ∀ (f : F), Monotone ↑f)

ink

instance instCoeTCOrderMonoidWithZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : OrderMonoidWithZeroHomClass F α β] : CoeTC F (α →*₀o β)

Equations

• instCoeTCOrderMonoidWithZeroHom = { coe := OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom }

ink

theorem map_nonneg {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] [inst : OrderAddMonoidHomClass F α β] (f : F) {a : α} (ha : 0 ≤ a) : 0 ≤ ↑f a

ink

theorem map_nonpos {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] [inst : OrderAddMonoidHomClass F α β] (f : F) {a : α} (ha : a ≤ 0) : ↑f a ≤ 0

ink

theorem monotone_iff_map_nonneg {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) : Monotone ↑f ↔ ∀ (a : α), 0 ≤ a → 0 ≤ ↑f a

ink

theorem antitone_iff_map_nonpos {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) : Antitone ↑f ↔ ∀ (a : α), 0 ≤ a → ↑f a ≤ 0

ink

theorem monotone_iff_map_nonpos {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) : Monotone ↑f ↔ ∀ (a : α), a ≤ 0 → ↑f a ≤ 0

ink

theorem antitone_iff_map_nonneg {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) : Antitone ↑f ↔ ∀ (a : α), a ≤ 0 → 0 ≤ ↑f a

ink

theorem strictMono_iff_map_pos {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) [inst : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1] : StrictMono ↑f ↔ ∀ (a : α), 0 < a → 0 < ↑f a

ink

theorem strictAnti_iff_map_neg {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) [inst : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1] : StrictAnti ↑f ↔ ∀ (a : α), 0 < a → ↑f a < 0

ink

theorem strictMono_iff_map_neg {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) [inst : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1] : StrictMono ↑f ↔ ∀ (a : α), a < 0 → ↑f a < 0

ink

theorem strictAnti_iff_map_pos {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) [inst : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1] : StrictAnti ↑f ↔ ∀ (a : α), a < 0 → 0 < ↑f a

ink

def OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom.proof_2 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) (x : α) (y : α) : ZeroHom.toFun (↑f.toAddMonoidHom) (x + y) = ZeroHom.toFun (↑f.toAddMonoidHom) x + ZeroHom.toFun (↑f.toAddMonoidHom) y

Equations

• One or more equations did not get rendered due to their size.

ink

def OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom.proof_3 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) : ZeroHom.toFun (↑f.toAddMonoidHom) 0 = 0

Equations

• (_ : ZeroHom.toFun (↑f.toAddMonoidHom) 0 = 0) = (_ : ZeroHom.toFun (↑f.toAddMonoidHom) 0 = 0)

ink

instance OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] : OrderAddMonoidHomClass (α →+o β) α β

Equations

• OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom = OrderAddMonoidHomClass.mk (_ : ∀ (f : α →+o β), Monotone (↑f.toAddMonoidHom).toFun)

ink

def OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom.proof_4 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) : Monotone (↑f.toAddMonoidHom).toFun

Equations

• (_ : Monotone (↑f.toAddMonoidHom).toFun) = (_ : Monotone (↑f.toAddMonoidHom).toFun)

ink

def OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom.proof_1 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) (g : α →+o β) (h : (fun f => (↑f.toAddMonoidHom).toFun) f = (fun f => (↑f.toAddMonoidHom).toFun) g) : f = g

Equations

• (_ : f = g) = (_ : f = g)

ink

instance OrderMonoidHom.instOrderMonoidHomClassOrderMonoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] : OrderMonoidHomClass (α →*o β) α β

Equations

• OrderMonoidHom.instOrderMonoidHomClassOrderMonoidHom = OrderMonoidHomClass.mk (_ : ∀ (f : α →*o β), Monotone (↑f.toMonoidHom).toFun)

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Reinterpret an ordered additive monoid homomorphism as an order homomorphism.

Equations

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

ink

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

Reinterpret an ordered monoid homomorphism as an order homomorphism.

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

def OrderAddMonoidHom.copy.proof_1 {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) (f' : α → β) (h : f' = ↑f) : ZeroHom.toFun (↑(AddMonoidHom.copy f.toAddMonoidHom f' h)) 0 = 0

Equations

• (_ : ZeroHom.toFun (↑(AddMonoidHom.copy f.toAddMonoidHom f' h)) 0 = 0) = (_ : ZeroHom.toFun (↑(AddMonoidHom.copy f.toAddMonoidHom f' h)) 0 = 0)

ink

def OrderAddMonoidHom.copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : 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

• One or more equations did not get rendered due to their size.

ink

def OrderAddMonoidHom.copy.proof_2 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) (f' : α → β) (h : f' = ↑f) : Monotone f'

Equations

• (_ : Monotone f') = (_ : Monotone f')

ink

def OrderMonoidHom.copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : 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

• One or more equations did not get rendered due to their size.

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

The identity map as an ordered additive monoid homomorphism.

Equations

• One or more equations did not get rendered due to their size.

ink

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

The identity map as an ordered monoid homomorphism.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem OrderAddMonoidHom.coe_id (α : Type u_1) [inst : Preorder α] [inst : AddZeroClass α] : ↑(OrderAddMonoidHom.id α) = id

ink

@[simp]

theorem OrderMonoidHom.coe_id (α : Type u_1) [inst : Preorder α] [inst : MulOneClass α] : ↑(OrderMonoidHom.id α) = id

ink

instance OrderAddMonoidHom.instInhabitedOrderAddMonoidHom (α : Type u_1) [inst : Preorder α] [inst : AddZeroClass α] : Inhabited (α →+o α)

Equations

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

ink

instance OrderMonoidHom.instInhabitedOrderMonoidHom (α : Type u_1) [inst : Preorder α] [inst : MulOneClass α] : Inhabited (α →*o α)

Equations

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

ink

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

Composition of OrderAddMonoidHoms as an OrderAddMonoidHom

Equations

• One or more equations did not get rendered due to their size.

ink

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

Composition of OrderMonoidHoms as an OrderMonoidHom.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

def OrderAddMonoidHom.instZeroOrderAddMonoidHom.proof_1 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass β] : Monotone fun x => AddZeroClass.toZero.1

Equations

• (_ : Monotone fun x => AddZeroClass.toZero.1) = (_ : Monotone fun x => AddZeroClass.toZero.1)

ink

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

0 is the homomorphism sending all elements to 0.

Equations

• One or more equations did not get rendered due to their size.

ink

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

1 is the homomorphism sending all elements to 1.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem OrderAddMonoidHom.coe_zero {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] : ↑0 = 0

ink

@[simp]

theorem OrderMonoidHom.coe_one {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] : ↑1 = 1

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

def OrderAddMonoidHom.instAddOrderAddMonoidHomToPreorderToPartialOrderToPreorderToPartialOrderToAddZeroClassToAddMonoidToAddCommMonoidToAddZeroClassToAddMonoidToAddCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] (f : α →+o β) (g : α →+o β) (x : α) (y : α) : ZeroHom.toFun (↑(↑f + ↑g)) (x + y) = ZeroHom.toFun (↑(↑f + ↑g)) x + ZeroHom.toFun (↑(↑f + ↑g)) y

Equations

• One or more equations did not get rendered due to their size.

ink

instance OrderAddMonoidHom.instAddOrderAddMonoidHomToPreorderToPartialOrderToPreorderToPartialOrderToAddZeroClassToAddMonoidToAddCommMonoidToAddZeroClassToAddMonoidToAddCommMonoid {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] : 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

• One or more equations did not get rendered due to their size.

ink

def OrderAddMonoidHom.instAddOrderAddMonoidHomToPreorderToPartialOrderToPreorderToPartialOrderToAddZeroClassToAddMonoidToAddCommMonoidToAddZeroClassToAddMonoidToAddCommMonoid.proof_2 {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] (f : α →+o β) (g : α →+o β) : Monotone fun x => ZeroHom.toFun (↑f.toAddMonoidHom) x + ↑↑g x

Equations

• (_ : Monotone fun x => ZeroHom.toFun (↑f.toAddMonoidHom) x + ↑↑g x) = (_ : Monotone fun x => ZeroHom.toFun (↑f.toAddMonoidHom) x + ↑↑g x)

ink

instance OrderMonoidHom.instMulOrderMonoidHomToPreorderToPartialOrderToPreorderToPartialOrderToMulOneClassToMonoidToCommMonoidToMulOneClassToMonoidToCommMonoid {α : Type u_1} {β : Type u_2} [inst : OrderedCommMonoid α] [inst : OrderedCommMonoid β] : 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

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem OrderAddMonoidHom.coe_add {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] (f : α →+o β) (g : α →+o β) : ↑(f + g) = ↑f + ↑g

ink

@[simp]

theorem OrderMonoidHom.coe_mul {α : Type u_1} {β : Type u_2} [inst : OrderedCommMonoid α] [inst : OrderedCommMonoid β] (f : α →*o β) (g : α →*o β) : ↑(f * g) = ↑f * ↑g

ink

@[simp]

theorem OrderAddMonoidHom.add_apply {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] (f : α →+o β) (g : α →+o β) (a : α) : ↑(f + g) a = ↑f a + ↑g a

ink

@[simp]

theorem OrderMonoidHom.mul_apply {α : Type u_1} {β : Type u_2} [inst : OrderedCommMonoid α] [inst : OrderedCommMonoid β] (f : α →*o β) (g : α →*o β) (a : α) : ↑(f * g) a = ↑f a * ↑g a

ink

theorem OrderAddMonoidHom.add_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] [inst : OrderedAddCommMonoid γ] (g₁ : β →+o γ) (g₂ : β →+o γ) (f : α →+o β) : OrderAddMonoidHom.comp (g₁ + g₂) f = OrderAddMonoidHom.comp g₁ f + OrderAddMonoidHom.comp g₂ f

ink

theorem OrderMonoidHom.mul_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : OrderedCommMonoid α] [inst : OrderedCommMonoid β] [inst : OrderedCommMonoid γ] (g₁ : β →*o γ) (g₂ : β →*o γ) (f : α →*o β) : OrderMonoidHom.comp (g₁ * g₂) f = OrderMonoidHom.comp g₁ f * OrderMonoidHom.comp g₂ f

ink

theorem OrderAddMonoidHom.comp_add {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] [inst : OrderedAddCommMonoid γ] (g : β →+o γ) (f₁ : α →+o β) (f₂ : α →+o β) : OrderAddMonoidHom.comp g (f₁ + f₂) = OrderAddMonoidHom.comp g f₁ + OrderAddMonoidHom.comp g f₂

ink

theorem OrderMonoidHom.comp_mul {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : OrderedCommMonoid α] [inst : OrderedCommMonoid β] [inst : OrderedCommMonoid γ] (g : β →*o γ) (f₁ : α →*o β) (f₂ : α →*o β) : OrderMonoidHom.comp g (f₁ * f₂) = OrderMonoidHom.comp g f₁ * OrderMonoidHom.comp g f₂

ink

@[simp]

theorem OrderAddMonoidHom.toAddMonoidHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : OrderedAddCommMonoid α} {hβ : OrderedAddCommMonoid β} (f : α →+o β) : f.toAddMonoidHom = ↑f

ink

@[simp]

theorem OrderMonoidHom.toMonoidHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : OrderedCommMonoid α} {hβ : OrderedCommMonoid β} (f : α →*o β) : f.toMonoidHom = ↑f

ink

@[simp]

theorem OrderAddMonoidHom.toOrderHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : OrderedAddCommMonoid α} {hβ : OrderedAddCommMonoid β} (f : α →+o β) : OrderAddMonoidHom.toOrderHom f = ↑f

ink

@[simp]

theorem OrderMonoidHom.toOrderHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : OrderedCommMonoid α} {hβ : OrderedCommMonoid β} (f : α →*o β) : OrderMonoidHom.toOrderHom f = ↑f

ink

def OrderAddMonoidHom.mk' {α : Type u_1} {β : Type u_2} {hα : OrderedAddCommGroup α} {hβ : OrderedAddCommGroup β} (f : α → β) (hf : Monotone f) (map_mul : ∀ (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

• One or more equations did not get rendered due to their size.

ink

def OrderAddMonoidHom.mk'.proof_1 {α : Type u_2} {β : Type u_1} {hα : OrderedAddCommGroup α} {hβ : OrderedAddCommGroup β} (f : α → β) (map_mul : ∀ (a b : α), f (a + b) = f a + f b) (x : α) (y : α) : ZeroHom.toFun (↑(AddMonoidHom.mk' f map_mul)) (x + y) = ZeroHom.toFun (↑(AddMonoidHom.mk' f map_mul)) x + ZeroHom.toFun (↑(AddMonoidHom.mk' f map_mul)) y

Equations

• One or more equations did not get rendered due to their size.

ink

def OrderMonoidHom.mk' {α : Type u_1} {β : Type u_2} {hα : OrderedCommGroup α} {hβ : OrderedCommGroup β} (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

• One or more equations did not get rendered due to their size.

ink

instance OrderMonoidWithZeroHom.instOrderMonoidWithZeroHomClassOrderMonoidWithZeroHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] : OrderMonoidWithZeroHomClass (α →*₀o β) α β

Equations

• OrderMonoidWithZeroHom.instOrderMonoidWithZeroHomClassOrderMonoidWithZeroHom = OrderMonoidWithZeroHomClass.mk (_ : ∀ (f : α →*₀o β), Monotone (↑f.toMonoidWithZeroHom).toFun)

ink

theorem OrderMonoidWithZeroHom.ext {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] {f : α →*₀o β} {g : α →*₀o β} (h : ∀ (a : α), ↑f a = ↑g a) : f = g

ink

theorem OrderMonoidWithZeroHom.toFun_eq_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) : (↑f.toMonoidWithZeroHom).toFun = ↑f

ink

@[simp]

theorem OrderMonoidWithZeroHom.coe_mk {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀ β) (h : Monotone (↑f).toFun) : ↑{ toMonoidWithZeroHom := f, monotone' := h } = ↑f

ink

@[simp]

theorem OrderMonoidWithZeroHom.mk_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) (h : Monotone (↑↑f).toFun) : { toMonoidWithZeroHom := ↑f, monotone' := h } = f

ink

def OrderMonoidWithZeroHom.toOrderMonoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) : α →*o β

Reinterpret an ordered monoid with zero homomorphism as an order monoid homomorphism.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem OrderMonoidWithZeroHom.coe_monoidWithZeroHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) : ↑↑f = ↑f

ink

@[simp]

theorem OrderMonoidWithZeroHom.coe_orderMonoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) : ↑↑f = ↑f

ink

theorem OrderMonoidWithZeroHom.toOrderMonoidHom_injective {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] : Function.Injective OrderMonoidWithZeroHom.toOrderMonoidHom

ink

theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] : Function.Injective OrderMonoidWithZeroHom.toMonoidWithZeroHom

ink

def OrderMonoidWithZeroHom.copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) (f' : α → β) (h : f' = ↑f) : α →*o β

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem OrderMonoidWithZeroHom.coe_copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) (f' : α → β) (h : f' = ↑f) : ↑(OrderMonoidWithZeroHom.copy f f' h) = f'

ink

theorem OrderMonoidWithZeroHom.copy_eq {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) (f' : α → β) (h : f' = ↑f) : OrderMonoidWithZeroHom.copy f f' h = ↑f

ink

def OrderMonoidWithZeroHom.id (α : Type u_1) [inst : Preorder α] [inst : MulZeroOneClass α] : α →*₀o α

The identity map as an ordered monoid with zero homomorphism.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem OrderMonoidWithZeroHom.coe_id (α : Type u_1) [inst : Preorder α] [inst : MulZeroOneClass α] : ↑(OrderMonoidWithZeroHom.id α) = id

ink

instance OrderMonoidWithZeroHom.instInhabitedOrderMonoidWithZeroHom (α : Type u_1) [inst : Preorder α] [inst : MulZeroOneClass α] : Inhabited (α →*₀o α)

Equations

• OrderMonoidWithZeroHom.instInhabitedOrderMonoidWithZeroHom α = { default := OrderMonoidWithZeroHom.id α }

ink

def OrderMonoidWithZeroHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) : α →*₀o γ

Composition of OrderMonoidWithZeroHoms as an OrderMonoidWithZeroHom.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem OrderMonoidWithZeroHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) : ↑(OrderMonoidWithZeroHom.comp f g) = ↑f ∘ ↑g

ink

@[simp]

theorem OrderMonoidWithZeroHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) (a : α) : ↑(OrderMonoidWithZeroHom.comp f g) a = ↑f (↑g a)

ink

theorem OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) : ↑(OrderMonoidWithZeroHom.comp f g) = MonoidWithZeroHom.comp ↑f ↑g

ink

theorem OrderMonoidWithZeroHom.coe_comp_orderMonoidHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) : ↑(OrderMonoidWithZeroHom.comp f g) = OrderMonoidHom.comp ↑f ↑g

ink

@[simp]

theorem OrderMonoidWithZeroHom.comp_assoc {α : Type u_4} {β : Type u_3} {γ : Type u_1} {δ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : Preorder δ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] [inst : MulZeroOneClass δ] (f : γ →*₀o δ) (g : β →*₀o γ) (h : α →*₀o β) : OrderMonoidWithZeroHom.comp (OrderMonoidWithZeroHom.comp f g) h = OrderMonoidWithZeroHom.comp f (OrderMonoidWithZeroHom.comp g h)

ink

@[simp]

theorem OrderMonoidWithZeroHom.comp_id {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) : OrderMonoidWithZeroHom.comp f (OrderMonoidWithZeroHom.id α) = f

ink

@[simp]

theorem OrderMonoidWithZeroHom.id_comp {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) : OrderMonoidWithZeroHom.comp (OrderMonoidWithZeroHom.id β) f = f

ink

theorem OrderMonoidWithZeroHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] {g₁ : β →*₀o γ} {g₂ : β →*₀o γ} {f : α →*₀o β} (hf : Function.Surjective ↑f) : OrderMonoidWithZeroHom.comp g₁ f = OrderMonoidWithZeroHom.comp g₂ f ↔ g₁ = g₂

ink

theorem OrderMonoidWithZeroHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] {g : β →*₀o γ} {f₁ : α →*₀o β} {f₂ : α →*₀o β} (hg : Function.Injective ↑g) : OrderMonoidWithZeroHom.comp g f₁ = OrderMonoidWithZeroHom.comp g f₂ ↔ f₁ = f₂

ink

instance OrderMonoidWithZeroHom.instMulOrderMonoidWithZeroHomToPreorderToPartialOrderToOrderedCommMonoidToLinearOrderedCommMonoidToPreorderToPartialOrderToOrderedCommMonoidToLinearOrderedCommMonoidToMulZeroOneClassToMonoidWithZeroToCommMonoidWithZeroToMulZeroOneClassToMonoidWithZeroToCommMonoidWithZero {α : Type u_1} {β : Type u_2} [inst : LinearOrderedCommMonoidWithZero α] [inst : LinearOrderedCommMonoidWithZero β] : 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

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem OrderMonoidWithZeroHom.coe_mul {α : Type u_1} {β : Type u_2} [inst : LinearOrderedCommMonoidWithZero α] [inst : LinearOrderedCommMonoidWithZero β] (f : α →*₀o β) (g : α →*₀o β) : ↑(f * g) = ↑f * ↑g

ink

@[simp]

theorem OrderMonoidWithZeroHom.mul_apply {α : Type u_1} {β : Type u_2} [inst : LinearOrderedCommMonoidWithZero α] [inst : LinearOrderedCommMonoidWithZero β] (f : α →*₀o β) (g : α →*₀o β) (a : α) : ↑(f * g) a = ↑f a * ↑g a

ink

theorem OrderMonoidWithZeroHom.mul_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : LinearOrderedCommMonoidWithZero α] [inst : LinearOrderedCommMonoidWithZero β] [inst : LinearOrderedCommMonoidWithZero γ] (g₁ : β →*₀o γ) (g₂ : β →*₀o γ) (f : α →*₀o β) : OrderMonoidWithZeroHom.comp (g₁ * g₂) f = OrderMonoidWithZeroHom.comp g₁ f * OrderMonoidWithZeroHom.comp g₂ f

ink

theorem OrderMonoidWithZeroHom.comp_mul {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : LinearOrderedCommMonoidWithZero α] [inst : LinearOrderedCommMonoidWithZero β] [inst : LinearOrderedCommMonoidWithZero γ] (g : β →*₀o γ) (f₁ : α →*₀o β) (f₂ : α →*₀o β) : OrderMonoidWithZeroHom.comp g (f₁ * f₂) = OrderMonoidWithZeroHom.comp g f₁ * OrderMonoidWithZeroHom.comp g f₂

ink

@[simp]

theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} (f : α →*₀o β) : f.toMonoidWithZeroHom = ↑f

ink

@[simp]

theorem OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} (f : α →*₀o β) : OrderMonoidWithZeroHom.toOrderMonoidHom f = ↑f