Documentation

🔶 coverage

structure OrderMonoidWithZeroHom (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] extends α →*₀ β :

Type (max u_6 u_7)

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 parameterize over (F : Type*) [FunLike F M N] [MonoidWithZeroHomClass F M N] [OrderHomClass F M N] (f : F).

toFun : α → β
map_zero' : (↑self.toMonoidWithZeroHom).toFun 0 = 0
map_one' : (↑self.toMonoidWithZeroHom).toFun 1 = 1
map_mul' (x y : α) : (↑self.toMonoidWithZeroHom).toFun (x * y) = (↑self.toMonoidWithZeroHom).toFun x * (↑self.toMonoidWithZeroHom).toFun y
monotone' : Monotone (↑self.toMonoidWithZeroHom).toFun
An OrderMonoidWithZeroHom is a monotone function.

Instances For

def «term_→*₀o_» :

Lean.TrailingParserDescr

Infix notation for OrderMonoidWithZeroHom.

Instances For

def OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] [OrderHomClass F α β] [MonoidWithZeroHomClass F α β] (f : F) :

α →*₀o β

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

Instances For

@[implicit_reducible]

instance instCoeTCOrderMonoidWithZeroHomOfOrderHomClassOfMonoidWithZeroHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] [OrderHomClass F α β] [MonoidWithZeroHomClass F α β] :

CoeTC F (α →*₀o β)

@[implicit_reducible]

instance OrderMonoidWithZeroHom.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] :

FunLike (α →*₀o β) α β

instance OrderMonoidWithZeroHom.instMonoidWithZeroHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] :

MonoidWithZeroHomClass (α →*₀o β) α β

instance OrderMonoidWithZeroHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] :

OrderHomClass (α →*₀o β) α β

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

f = g

theorem OrderMonoidWithZeroHom.ext_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] {f g : α →*₀o β} :

f = g ↔ ∀ (a : α), f a = g a

theorem OrderMonoidWithZeroHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) :

(↑f.toMonoidWithZeroHom).toFun = ⇑f

@[simp]

theorem OrderMonoidWithZeroHom.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (h : Monotone (↑f).toFun) :

⇑{ toMonoidWithZeroHom := f, monotone' := h } = ⇑f

@[simp]

theorem OrderMonoidWithZeroHom.mk_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) (h : Monotone (↑↑f).toFun) :

{ toMonoidWithZeroHom := ↑f, monotone' := h } = f

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

α →*o β

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

Instances For

@[simp]

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

⇑↑f = ⇑f

@[simp]

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

⇑↑f = ⇑f

theorem OrderMonoidWithZeroHom.toOrderMonoidHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] :

Function.Injective toOrderMonoidHom

theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] :

Function.Injective toMonoidWithZeroHom

def OrderMonoidWithZeroHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [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.

Instances For

@[simp]

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

⇑(f.copy f' h) = f'

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

f.copy f' h = ↑f

def OrderMonoidWithZeroHom.id (α : Type u_2) [Preorder α] [MulZeroOneClass α] :

α →*₀o α

The identity map as an ordered monoid with zero homomorphism.

Instances For

@[simp]

theorem OrderMonoidWithZeroHom.coe_id (α : Type u_2) [Preorder α] [MulZeroOneClass α] :

⇑(OrderMonoidWithZeroHom.id α) = id

@[implicit_reducible]

instance OrderMonoidWithZeroHom.instInhabited (α : Type u_2) [Preorder α] [MulZeroOneClass α] :

Inhabited (α →*₀o α)

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

α →*₀o γ

Composition of OrderMonoidWithZeroHoms as an OrderMonoidWithZeroHom.

Instances For

@[simp]

theorem OrderMonoidWithZeroHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) :

⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

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

(f.comp g) a = f (g a)

theorem OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) :

↑(f.comp g) = (↑f).comp ↑g

theorem OrderMonoidWithZeroHom.coe_comp_orderMonoidHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) :

↑(f.comp g) = (↑f).comp ↑g

@[simp]

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

(f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem OrderMonoidWithZeroHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) :

f.comp (OrderMonoidWithZeroHom.id α) = f

@[simp]

theorem OrderMonoidWithZeroHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) :

(OrderMonoidWithZeroHom.id β).comp f = f

@[simp]

theorem OrderMonoidWithZeroHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] {g₁ g₂ : β →*₀o γ} {f : α →*₀o β} (hf : Function.Surjective ⇑f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem OrderMonoidWithZeroHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] {g : β →*₀o γ} {f₁ f₂ : α →*₀o β} (hg : Function.Injective ⇑g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

@[implicit_reducible]

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

@[simp]

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

⇑(f * g) = ⇑f * ⇑g

@[simp]

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

(f * g) a = f a * g a

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

(g₁ * g₂).comp f = g₁.comp f * g₂.comp f

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

g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

@[simp]

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

f.toMonoidWithZeroHom = ↑f

@[simp]

theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_mk {α : Type u_2} {β : Type u_3} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} (f : α →*₀ β) (hf : Monotone ⇑f) :

↑{ toMonoidWithZeroHom := f, monotone' := hf } = f

@[simp]

theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} {hγ : Preorder γ} {hγ' : MulZeroOneClass γ} (f : β →*₀o γ) (g : α →*₀o β) :

↑(f.comp g) = (↑f).comp ↑g

@[simp]

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

f.toOrderMonoidHom = ↑f

@[simp]

theorem OrderMonoidWithZeroHom.toOrderMonoidHom_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} {hγ : Preorder γ} {hγ' : MulZeroOneClass γ} (f : β →*₀o γ) (g : α →*₀o β) :

↑(f.comp g) = (↑f).comp ↑g

def OrderMonoidIso.unitsWithZero {α : Type u_6} [Group α] [Preorder α] :

(WithZero α)ˣ ≃*o α

Any ordered group is isomorphic to the units of itself adjoined with 0.

Instances For

@[simp]

theorem OrderMonoidIso.val_unitsWithZero_symm_apply {α : Type u_6} [Group α] [Preorder α] (a : α) :

↑(unitsWithZero.symm a) = ↑a

@[simp]

theorem OrderMonoidIso.unitsWithZero_apply {α : Type u_6} [Group α] [Preorder α] (a : (WithZero α)ˣ) :

unitsWithZero a = WithZero.unzero ⋯

@[simp]

theorem OrderMonoidIso.val_inv_unitsWithZero_symm_apply {α : Type u_6} [Group α] [Preorder α] (a : α) :

↑(unitsWithZero.symm a)⁻¹ = (↑a)⁻¹

def OrderMonoidIso.withZero {G : Type u_6} {H : Type u_7} [Group G] [PartialOrder G] [Group H] [PartialOrder H] :

(G ≃*o H) ≃ (WithZero G ≃*o WithZero H)

A version of Equiv.optionCongr for WithZero on OrderMonoidIso.

Instances For

@[simp]

theorem OrderMonoidIso.withZero_apply_symm_apply {G : Type u_6} {H : Type u_7} [Group G] [PartialOrder G] [Group H] [PartialOrder H] (e : G ≃*o H) (a : WithZero H) :

(withZero e).symm a = (WithZero.map' ↑(↑e).symm) a

@[simp]

theorem OrderMonoidIso.withZero_symm_apply_symm_apply {G : Type u_6} {H : Type u_7} [Group G] [PartialOrder G] [Group H] [PartialOrder H] (e : WithZero G ≃*o WithZero H) (x : H) :

(withZero.symm e).symm x = WithZero.unzero ⋯

@[simp]

theorem OrderMonoidIso.withZero_symm_apply_apply {G : Type u_6} {H : Type u_7} [Group G] [PartialOrder G] [Group H] [PartialOrder H] (e : WithZero G ≃*o WithZero H) (x : G) :

(withZero.symm e) x = WithZero.unzero ⋯

@[simp]

theorem OrderMonoidIso.withZero_apply_apply {G : Type u_6} {H : Type u_7} [Group G] [PartialOrder G] [Group H] [PartialOrder H] (e : G ≃*o H) (a : WithZero G) :

(withZero e) a = (WithZero.map' ↑↑e) a

def OrderMonoidIso.withZeroUnits {α : Type u_6} [LinearOrderedCommGroupWithZero α] [DecidablePred fun (a : α) => a = 0] :

WithZero αˣ ≃*o α

Any linearly ordered group with zero is isomorphic to adjoining 0 to the units of itself.

Instances For

@[simp]

theorem OrderMonoidIso.withZeroUnits_symm_apply {α : Type u_6} [LinearOrderedCommGroupWithZero α] [DecidablePred fun (a : α) => a = 0] (a : α) :

withZeroUnits.symm a = if h : a = 0 then 0 else ↑(Units.mk0 a h)