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.subset {ι : Type u_1} {M : Type u_2} [Monoid M] (v : ι → M) (s : Set ι) : {i : ι | IsMulIndecomposable v s i} ⊆ s

theorem IsAddIndecomposable.subset {ι : Type u_1} {M : Type u_2} [AddMonoid M] (v : ι → M) (s : Set ι) : {i : ι | IsAddIndecomposable v s i} ⊆ s

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

def IsMulIndecomposable.baseOf {ι : Type u_1} {M : Type u_2} {S : Type u_4} [Monoid M] [LinearOrder S] [Monoid S] (v : ι → M) (f : M →* S) : Set ι

The "base" of a set of points of a monoid relative to a morphism f.

Equations

• IsMulIndecomposable.baseOf v f = {j : ι | IsMulIndecomposable v {i : ι | 1 < f (v i)} j}

def IsAddIndecomposable.baseOf {ι : Type u_1} {M : Type u_2} {S : Type u_4} [AddMonoid M] [LinearOrder S] [AddMonoid S] (v : ι → M) (f : M →+ S) : Set ι

The "base" of v relative to a morphism f.

In the case that v is the set of roots of a crystallographic root system, and S = ℚ, this is the base of the root system associated to f.

Equations

• IsAddIndecomposable.baseOf v f = {j : ι | IsAddIndecomposable v {i : ι | 0 < f (v i)} j}

theorem IsMulIndecomposable.baseOf_subset_one_lt {ι : Type u_1} {M : Type u_2} {S : Type u_4} [Monoid M] [LinearOrder S] [Monoid S] (v : ι → M) (f : M →* S) : baseOf v f ⊆ {i : ι | 1 < f (v i)}

theorem IsAddIndecomposable.baseOf_subset_pos {ι : Type u_1} {M : Type u_2} {S : Type u_4} [AddMonoid M] [LinearOrder S] [AddMonoid S] (v : ι → M) (f : M →+ S) : baseOf v f ⊆ {i : ι | 0 < f (v i)}

theorem IsMulIndecomposable.image_baseOf_inv_comp_eq {ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (f : G →* S) : v '' baseOf v (invMonoidHom.comp f) = ⇑invMonoidHom ∘ v '' baseOf v f

theorem IsAddIndecomposable.image_baseOf_neg_comp_eq {ι : Type u_1} {G : Type u_3} {S : Type u_4} [AddCommGroup G] [LinearOrder S] [InvolutiveNeg ι] [AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G) (hv_neg : ∀ (i : ι), v (-i) = -v i) (f : G →+ S) : v '' baseOf v (negAddMonoidHom.comp f) = ⇑negAddMonoidHom ∘ v '' baseOf v f

theorem Submonoid.closure_image_isMulIndecomposable_baseOf {ι : Type u_1} {M : Type u_2} {S : Type u_4} [Monoid M] [LinearOrder S] [Finite ι] [CommMonoid S] [IsOrderedCancelMonoid S] (v : ι → M) (f : M →* S) : closure (v '' IsMulIndecomposable.baseOf v f) = 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_isAddIndecomposable_baseOf {ι : Type u_1} {M : Type u_2} {S : Type u_4} [AddMonoid M] [LinearOrder S] [Finite ι] [AddCommMonoid S] [IsOrderedCancelAddMonoid S] (v : ι → M) (f : M →+ S) : closure (v '' IsAddIndecomposable.baseOf v f) = 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 [Ser87](Ch. V, §9, Lemma 2) and it may be used to prove that the root system has a base.

theorem Subgroup.closure_image_isMulIndecomposable_baseOf {ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [Finite ι] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (f : G →* S) (hf : ∀ (i : ι), f (v i) ≠ 1) : closure (v '' IsMulIndecomposable.baseOf v f) = closure (Set.range v)

theorem AddSubgroup.closure_image_isAddIndecomposable_baseOf {ι : Type u_1} {G : Type u_3} {S : Type u_4} [AddCommGroup G] [LinearOrder S] [Finite ι] [InvolutiveNeg ι] [AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G) (hv_neg : ∀ (i : ι), v (-i) = -v i) (f : G →+ S) (hf : ∀ (i : ι), f (v i) ≠ 0) : closure (v '' IsAddIndecomposable.baseOf v f) = closure (Set.range v)

theorem IsMulIndecomposable.pairwise_div_notMem_range {ι : Type u_1} {G : Type u_3} [CommGroup G] [InvolutiveInv ι] (v : ι → G) (hv_one : ∀ (i : ι), v i ≠ 1) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (s t : Set ι) (hst : s ⊆ {i : ι | IsMulIndecomposable v t i}) (hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t) : s.Pairwise fun (i j : ι) => v i / v j ∉ Set.range v

theorem IsAddIndecomposable.pairwise_sub_notMem_range {ι : Type u_1} {G : Type u_3} [AddCommGroup G] [InvolutiveNeg ι] (v : ι → G) (hv_zero : ∀ (i : ι), v i ≠ 0) (hv_neg : ∀ (i : ι), v (-i) = -v i) (s t : Set ι) (hst : s ⊆ {i : ι | IsAddIndecomposable v t i}) (hv_t : ∀ (i : ι), i ∈ t ∨ -i ∈ t) : s.Pairwise fun (i j : ι) => v i - v j ∉ Set.range v

theorem IsMulIndecomposable.pairwise_div_notMem_range' {ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (f : G →* S) (hf : ∀ (i : ι), f (v i) ≠ 1) (s : Set ι) (hst : s ⊆ {j : ι | IsMulIndecomposable v {i : ι | 1 < f (v i)} j}) : s.Pairwise fun (i j : ι) => v i / v j ∉ Set.range v

theorem IsAddIndecomposable.pairwise_sub_notMem_range' {ι : Type u_1} {G : Type u_3} {S : Type u_4} [AddCommGroup G] [LinearOrder S] [InvolutiveNeg ι] [AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G) (hv_neg : ∀ (i : ι), v (-i) = -v i) (f : G →+ S) (hf : ∀ (i : ι), f (v i) ≠ 0) (s : Set ι) (hst : s ⊆ {j : ι | IsAddIndecomposable v {i : ι | 0 < f (v i)} j}) : s.Pairwise fun (i j : ι) => v i - v j ∉ Set.range v

theorem IsMulIndecomposable.pairwise_baseOf_div_notMem {ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (f : G →* S) (hf : ∀ (i : ι), f (v i) ≠ 1) : (baseOf v f).Pairwise fun (i j : ι) => v i / v j ∉ Set.range v

theorem IsAddIndecomposable.pairwise_baseOf_sub_notMem {ι : Type u_1} {G : Type u_3} {S : Type u_4} [AddCommGroup G] [LinearOrder S] [InvolutiveNeg ι] [AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G) (hv_neg : ∀ (i : ι), v (-i) = -v i) (f : G →+ S) (hf : ∀ (i : ι), f (v i) ≠ 0) : (baseOf v f).Pairwise fun (i j : ι) => v i - v j ∉ Set.range v

theorem IsMulIndecomposable.mem_or_inv_mem_closure_baseOf {ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [Finite ι] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (f : G →* S) (hf : ∀ (i : ι), f (v i) ≠ 1) (i : ι) : v i ∈ Submonoid.closure (v '' baseOf v f) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' baseOf v f)

theorem IsAddIndecomposable.mem_or_neg_mem_closure_baseOf {ι : Type u_1} {G : Type u_3} {S : Type u_4} [AddCommGroup G] [LinearOrder S] [Finite ι] [InvolutiveNeg ι] [AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G) (hv_neg : ∀ (i : ι), v (-i) = -v i) (f : G →+ S) (hf : ∀ (i : ι), f (v i) ≠ 0) (i : ι) : v i ∈ AddSubmonoid.closure (v '' baseOf v f) ∨ -v i ∈ AddSubmonoid.closure (v '' baseOf v f)

theorem Submonoid.apply_ne_one_of_mem_or_inv_mem_closure {ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (hv_one : ∀ (i : ι), v i ≠ 1) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (f : G →* S) (s : Set ι) (hsp : ∀ (i : ι), v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)) (hf : ∀ i ∈ s, 1 < f (v i)) (i : ι) : f (v i) ≠ 1

theorem AddSubmonoid.apply_ne_zero_of_mem_or_neg_mem_closure {ι : Type u_1} {G : Type u_3} {S : Type u_4} [AddCommGroup G] [LinearOrder S] [InvolutiveNeg ι] [AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G) (hv_zero : ∀ (i : ι), v i ≠ 0) (hv_neg : ∀ (i : ι), v (-i) = -v i) (f : G →+ S) (s : Set ι) (hsp : ∀ (i : ι), v i ∈ closure (v '' s) ∨ -v i ∈ closure (v '' s)) (hf : ∀ i ∈ s, 0 < f (v i)) (i : ι) : f (v i) ≠ 0