Indecomposable elements of monoids

def IsMulIndecomposable {ι : Type u_1} {M : Type u_2} [Monoid M] (v : ι → M) (s : Set ι) (i : ι) : Prop

Given a family of elements of a monoid, a member is said to be indecomposable if it cannot be written as a product of two others in a non-trivial way.

Equations

• IsMulIndecomposable v s i = (i ∈ s ∧ ∀ j ∈ s, ∀ k ∈ s, v i = v j * v k → v j = 1 ∨ v k = 1)

def IsAddIndecomposable {ι : Type u_1} {M : Type u_2} [AddMonoid M] (v : ι → M) (s : Set ι) (i : ι) : Prop

Given a family of elements of an additive monoid, a member is said to be indecomposable if it cannot be written as a sum of two others in a non-trivial way.

Equations

• IsAddIndecomposable v s i = (i ∈ s ∧ ∀ j ∈ s, ∀ k ∈ s, v i = v j + v k → v j = 0 ∨ v k = 0)

theorem isMulIndecomposable_id_univ {M : Type u_2} [Monoid M] [Subsingleton Mˣ] {x : M} (hx : x ≠ 1) : IsMulIndecomposable id Set.univ x ↔ Irreducible x

theorem isAddIndecomposable_id_univ {M : Type u_2} [AddMonoid M] [Subsingleton (AddUnits M)] {x : M} (hx : x ≠ 0) : IsAddIndecomposable id Set.univ x ↔ AddIrreducible x

theorem Submonoid.closure_image_one_lt_and_isMulIndecomposable {ι : Type u_1} {M : Type u_2} [Monoid M] [Finite ι] {S : Type u_3} [CommMonoid S] [LinearOrder S] [IsOrderedCancelMonoid S] (v : ι → M) (f : M →* S) : closure (v '' {i : ι | IsMulIndecomposable v {j : ι | 1 < f (v j)} i}) = closure (v '' {i : ι | 1 < f (v i)})

Given a finite family of points v in a monoid M, together with a morphism into a linearly-ordered monoid f : M →* S, the submonoid generated by those points of v which lie in the "half space" where f > 1 is generated by the subset of such points which are indecomposable with respect to points in this half space.

theorem AddSubmonoid.closure_image_pos_and_isAddIndecomposable {ι : Type u_1} {M : Type u_2} [AddMonoid M] [Finite ι] {S : Type u_3} [AddCommMonoid S] [LinearOrder S] [IsOrderedCancelAddMonoid S] (v : ι → M) (f : M →+ S) : closure (v '' {i : ι | IsAddIndecomposable v {j : ι | 0 < f (v j)} i}) = closure (v '' {i : ι | 0 < f (v i)})

Given a finite family of points v in an additive monoid M, together with a morphism into a linearly-ordered additive monoid f : M →+ S, the submonoid generated by those points of v which lie in the half space where f > 0 is generated by the subset of such points which are indecomposable with respect to points in this half space.

If v is the set of roots of a crystallographic root system and S = ℚ, then this is [serre1965](Ch. V, §9, Lemma 2) and it may be used to prove that the root system has a base.