The range of a MonoidHomWithZero

Given a MonoidWithZeroHom f : A → B whose codomain B is a MonoidWithZero, we define the type MonoidHomWithZero.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}.

MonoidHomWithZero.valueMonoid₀ is the MonoidWithZero obtained by adjoining 0 to the previous type.

Likewise, MonoidHomWithZero.valueGroup is the subgroup of Bˣ generated by the invertible elements in range f and ``MonoidHomWithZero.valueGroup₀adds a0` to the previous group.

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

Main Results

• valueMonoid f is the smallest submonoid of Bˣ containing the range of f;
• valueMonoid₀ f is the smallest submonoid 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 subgroup 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, MonoidHomWithZero.valueGroup can be explicitely descibed as the elements that are ratios of terms in range f , see MonoidHomWithZero.mem_valueGroup_iff_of_comm.

Implementation details

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

def MonoidHomWithZero.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.

Equations

• MonoidHomWithZero.valueMonoid f = { carrier := Units.val ⁻¹' Set.range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }

theorem MonoidHomWithZero.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 MonoidHomWithZero.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 MonoidHomWithZero.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.

Equations

• MonoidHomWithZero.valueGroup f = Subgroup.closure ↑(MonoidHomWithZero.valueMonoid f)

theorem MonoidHomWithZero.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 MonoidHomWithZero.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.

Equations

• MonoidHomWithZero.valueMonoid₀ f = WithZero ↥(MonoidHomWithZero.valueMonoid f)

@[reducible, inline]

abbrev MonoidHomWithZero.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.

Equations

• MonoidHomWithZero.valueGroup₀ f = WithZero ↥(MonoidHomWithZero.valueGroup f)

theorem MonoidHomWithZero.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 MonoidHomWithZero.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 MonoidHomWithZero.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 MonoidHomWithZero.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 MonoidHomWithZero.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 MonoidHomWithZero.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 MonoidHomWithZero.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 MonoidHomWithZero.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)

Equations

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