The range of a MonoidWithZeroHom

Given a MonoidWithZeroHom f : A → B whose codomain B is a MonoidWithZero, we define the type MonoidWithZeroHom.valueMonoid as the submonoid of Bˣ generated by the invertible elements in the range of f. For example, if A = ℕ, f is the natural cast to B where B is

• ℝ≥0, then MonoidWithZero.valueMonoid are the positive natural numbers in ℝ≥0;
• WithZero ℤ, then MonoidWithZero.valueMonoid = {1}.

MonoidWithZeroHom.ValueMonoid₀ is the MonoidWithZero obtained by adjoining 0 to the previous type.

Likewise, MonoidWithZeroHom.valueGroup is the subgroup of Bˣ generated by the invertible elements in range f and MonoidWithZeroHom.ValueGroup₀ adds a 0 to the previous group.

When B is commutative, then both MonoidWithZeroHom.valueGroup f and MonoidWithZeroHom.ValueGroup₀ f are also commutative and the former can be described more explicitly (see MonoidWithZeroHom.mem_valueGroup_iff_of_comm).

Main declarations

• valueMonoid f is the smallest submonoid of Bˣ containing the range of f;
• ValueMonoid₀ f is the smallest monoid with 0 containing the range of f;
• valueGroup f is the smallest subgroup of Bˣ containing the range of f;
• ValueMonoid₀ f is the smallest group with 0 containing the range of f;
• When B is a group with zero, rather than merely a monoid with zero, the above definitions all coincide: see valueMonoid_eq_valueGroup for an equality as submonoids and valueMonoid_eq_valueGroup' for an equality as subsets.
• When B is a commutative group with zero, MonoidWithZeroHom.valueGroup can be explicitly described as the elements that are ratios of terms in range f, see MonoidWithZeroHom.mem_valueGroup_iff_of_comm.

Implementation details

MonoidWithZeroHom.valueMonoid is defined explicitly in terms of its carrier, by proving the required properties; that it coincides with the submonoid generated by the closure is proven in MonoidWithZeroHom.valueMonoid_eq_closure, but using the latter as definition yields to unwanted unfolding.

theorem MonoidWithZeroHom.mrange_nontrivial {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] [Nontrivial H] (f : G →*₀ H) : Nontrivial ↥(MonoidHom.mrange f)

theorem MonoidWithZeroHom.range_nontrivial {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] [Nontrivial H] (f : G →*₀ H) : (Set.range ⇑f).Nontrivial

def MonoidWithZeroHom.valueMonoid {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] : Submonoid Bˣ

For a morphism of monoids with zero f, this is a smallest submonoid of the invertible elements in the codomain containing the range of f.

theorem MonoidWithZeroHom.one_mem_valueMonoid {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] : 1 ∈ valueMonoid f

theorem MonoidWithZeroHom.coe_one {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] : ⟨1, ⋯⟩ = 1

theorem MonoidWithZeroHom.mem_valueMonoid_iff {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] {b : Bˣ} : b ∈ valueMonoid f ↔ b ∈ Units.val ⁻¹' Set.range ⇑f

theorem MonoidWithZeroHom.valueMonoid_eq_closure {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] : valueMonoid f = Submonoid.closure (Units.val ⁻¹' Set.range ⇑f)

def MonoidWithZeroHom.valueGroup {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] : Subgroup Bˣ

For a morphism of monoids with zero f, this is the smallest subgroup of the invertible elements in the codomain containing the range of f.

theorem MonoidWithZeroHom.valueGroup_def {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] : valueGroup f = Subgroup.closure ↑(valueMonoid f)

@[reducible, inline]

abbrev MonoidWithZeroHom.ValueMonoid₀ {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] : Type u_2

For a morphism of monoids with zero f, this is the smallest submonoid with zero of the codomain containing the range of f.

@[deprecated MonoidWithZeroHom.ValueMonoid₀ (since := "2025-09-03")]

def MonoidWithZeroHom.valueMonoid₀ {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] : Type u_2

Alias of MonoidWithZeroHom.ValueMonoid₀.

---

For a morphism of monoids with zero f, this is the smallest submonoid with zero of the codomain containing the range of f.

@[reducible, inline]

abbrev MonoidWithZeroHom.ValueGroup₀ {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] : Type u_2

For a morphism of monoids with zero f, this is a smallest subgroup with zero of the codomain containing the range of f.

@[deprecated MonoidWithZeroHom.ValueGroup₀ (since := "2025-09-03")]

def MonoidWithZeroHom.valueGroup₀ {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] : Type u_2

Alias of MonoidWithZeroHom.ValueGroup₀.

---

For a morphism of monoids with zero f, this is a smallest subgroup with zero of the codomain containing the range of f.

theorem MonoidWithZeroHom.mem_valueMonoid {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] {b : Bˣ} (hb : ↑b ∈ Set.range ⇑f) : b ∈ valueMonoid f

theorem MonoidWithZeroHom.mem_valueGroup {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] {b : Bˣ} (hb : ↑b ∈ Set.range ⇑f) : b ∈ valueGroup f

theorem MonoidWithZeroHom.inv_mem_valueGroup {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B] {b : Bˣ} (hb : ↑b ∈ Set.range ⇑f) : b⁻¹ ∈ valueGroup f

theorem MonoidWithZeroHom.valueMonoid_eq_valueGroup {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] {f : F} [GroupWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] : valueMonoid f = (valueGroup f).toSubmonoid

theorem MonoidWithZeroHom.valueMonoid_eq_valueGroup' {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [GroupWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] : ↑(valueMonoid f) = ↑(valueGroup f)

theorem MonoidWithZeroHom.valueGroup_eq_range {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] {f : F} [GroupWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] : Units.val '' ↑(valueGroup f) = Set.range ⇑f \ {0}

theorem MonoidWithZeroHom.mem_valueGroup_iff_of_comm {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [CommGroupWithZero B] [MonoidWithZeroHomClass F A B] {y : Bˣ} : y ∈ valueGroup f ↔ ∃ (a : A), f a ≠ 0 ∧ ∃ (x : A), f a * ↑y = f x

instance MonoidWithZeroHom.instCommGroupWithZeroValueGroup₀ {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [CommGroupWithZero B] [MonoidWithZeroHomClass F A B] : CommGroupWithZero (ValueGroup₀ f)