The range of a MonoidWithZeroHom

Given a MonoidWithZeroHom f : A → B whose codomain B is a LinearOrderedCommGroupWithZero, we provide some order properties of the MonoidWithZeroHom.ValueGroup₀ as defined in Mathlib.Algebra.GroupWithZero.Range.

def MonoidWithZeroHom.ValueGroup₀.orderMonoidWithZeroHom {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] (f : A →*₀ B) : ValueGroup₀ f →*₀o WithZero Bˣ

The inclusion of ValueGroup₀ f into WithZero Bˣ as a homomorphism of monoids with zero.

Equations

• MonoidWithZeroHom.ValueGroup₀.orderMonoidWithZeroHom f = { toMonoidWithZeroHom := WithZero.map' (MonoidWithZeroHom.valueGroup f).subtype, monotone' := ⋯ }

theorem MonoidWithZeroHom.ValueGroup₀.monoidWithZeroHom_strictMono {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} : StrictMono ⇑(orderMonoidWithZeroHom f)

theorem MonoidWithZeroHom.ValueGroup₀.embedding_strictMono {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} : StrictMono ⇑embedding

instance MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} : IsOrderedMonoid (ValueGroup₀ f)

@[implicit_reducible]

instance MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} : LinearOrderedCommGroupWithZero (ValueGroup₀ f)

Equations

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

theorem MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} (a : (ValueGroup₀ f)ˣ) : 0 < embedding ↑a

theorem MonoidWithZeroHom.ValueGroup₀.embedding_unit_ne_zero {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} (a : (ValueGroup₀ f)ˣ) : embedding ↑a ≠ 0