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 and 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.

@[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.

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

noncomputable def MonoidWithZeroHom.ValueGroup₀.embedding {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] {f : F} [MonoidWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] : ValueGroup₀ f →*₀ B

The inclusion of the subgroup with zero generated by the range of a monoid with zero hom f : A \to B into the codomain B.

theorem MonoidWithZeroHom.ValueGroup₀.embedding_apply {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] {f : F} [MonoidWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] (a✝ : ValueGroup₀ f) : embedding a✝ = WithZero.recZeroCoe 0 Units.val ((WithZero.map' (valueGroup f).subtype) a✝)

noncomputable def MonoidWithZeroHom.ValueGroup₀.restrict₀ {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] : A →*₀ ValueGroup₀ f

This is the restriction of f as a function taking values in valueGroup₀ f.

theorem MonoidWithZeroHom.ValueGroup₀.restrict₀_apply {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] (f : F) [MonoidWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] (a : A) : (restrict₀ f) a = if h : f a = 0 then 0 else ↑⟨Units.mk0 (f a) h, ⋯⟩

theorem MonoidWithZeroHom.ValueGroup₀.restrict₀_of_ne_zero {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] {f : F} [MonoidWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] {a : A} (h : f a ≠ 0) : (restrict₀ f) a = ↑⟨Units.mk0 (f a) h, ⋯⟩

@[simp]

theorem MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] {f : F} [MonoidWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] {a : A} : (restrict₀ f) a = 0 ↔ f a = 0

@[simp]

theorem MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_one_iff {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] {f : F} [MonoidWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] {a : A} : (restrict₀ f) a = 1 ↔ f a = 1

@[simp]

theorem MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ {A : Type u_1} {B : Type u_2} {F : Type u_3} [FunLike F A B] {f : F} [MonoidWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] (a : A) : embedding ((restrict₀ f) a) = f a

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}

@[simp]

theorem MonoidWithZeroHom.ValueGroup₀.restrict₀_range_eq_top {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] : Set.range ⇑(restrict₀ f) = ⊤

theorem MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective {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] : Function.Surjective ⇑(restrict₀ f)

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

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 x ≠ 0 ∧ f a * ↑y = f x

def MonoidWithZeroHom.valueGroup.mk {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] (r s : A) (hr : f r ≠ 0) (hs : f s ≠ 0) : ↥(valueGroup f)

The map sending a pair of nonzero r s : A to the element (v r)⁻¹ * (v s) of ValueGroup₀ v.

@[simp]

theorem MonoidWithZeroHom.valueGroup.mk_inj {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] {r₁ s₁ r₂ s₂ : A} {hr₁ : f r₁ ≠ 0} {hs₁ : f s₁ ≠ 0} {hr₂ : f r₂ ≠ 0} {hs₂ : f s₂ ≠ 0} : mk f r₁ s₁ hr₁ hs₁ = mk f r₂ s₂ hr₂ hs₂ ↔ f (r₁ * s₂) = f (r₂ * s₁)

@[simp]

theorem MonoidWithZeroHom.valueGroup.mk_mul {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] {r₁ s₁ r₂ s₂ : A} {hr₁ : f r₁ ≠ 0} {hs₁ : f s₁ ≠ 0} {hr₂ : f r₂ ≠ 0} {hs₂ : f s₂ ≠ 0} : mk f r₁ s₁ hr₁ hs₁ * mk f r₂ s₂ hr₂ hs₂ = mk f (r₁ * r₂) (s₁ * s₂) ⋯ ⋯

def MonoidWithZeroHom.ValueGroup₀.mk {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] [DecidablePred fun (b : B) => b = 0] (r s : A) : ValueGroup₀ f

The map sending a pair of nonzero r s : A to the element (v r)⁻¹ * (v s) of ValueGroup₀ v.

theorem MonoidWithZeroHom.ValueGroup₀.mk_eq_of_ne_zero {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] [DecidablePred fun (b : B) => b = 0] (r s : A) (hr : f r ≠ 0) (hs : f s ≠ 0) : mk f r s = ↑(valueGroup.mk f r s hr hs)

theorem MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk {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] (x : ValueGroup₀ f) : x = 0 ∨ ∃ (r : A) (s : A) (hr : f r ≠ 0) (hs : f s ≠ 0), x = ↑(valueGroup.mk f r s hr hs)

theorem MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk' {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] (x : ValueGroup₀ f) : x = 0 ∨ ∃ (d : { xy : A × A // f xy.1 ≠ 0 ∧ f xy.2 ≠ 0 }), x = ↑(valueGroup.mk f (↑d).1 (↑d).2 ⋯ ⋯)

@[implicit_reducible]

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)