An affine monoid with no non-trivial unit is generated by its irreducible elements

This file proves that an additive cancellative monoid with no non-trivial unit unit is generated by its irreducible elements.

theorem irreducible_mem_submonoidClosure_subset {M : Type u_1} [CommMonoid M] [Subsingleton Mˣ] {S : Set M} : {p : M | p ∈ Submonoid.closure S ∧ Irreducible p} ⊆ S

Any set S inside a monoid with a single unit contains the irreducible elements of the submonoid it generates.

theorem addIrreducible_mem_addSubmonoidClosure_subset {M : Type u_1} [AddCommMonoid M] [Subsingleton (AddUnits M)] {S : Set M} : {p : M | p ∈ AddSubmonoid.closure S ∧ AddIrreducible p} ⊆ S

Any set S inside an additive monoid with a single unit contains the irreducible elements of the submonoid it generates.

theorem irreducible_subset_of_submonoidClosure_eq_top {M : Type u_1} [CommMonoid M] [Subsingleton Mˣ] {S : Set M} (hS : Submonoid.closure S = ⊤) : {p : M | Irreducible p} ⊆ S

In a monoid with a single unit, irreducible elements lie in all generating sets.

theorem addIrreducible_subset_of_addSubmonoidClosure_eq_top {M : Type u_1} [AddCommMonoid M] [Subsingleton (AddUnits M)] {S : Set M} (hS : AddSubmonoid.closure S = ⊤) : {p : M | AddIrreducible p} ⊆ S

In an additive monoid with a single unit, irreducible elements lie in all generating sets.

theorem Submonoid.FG.finite_irreducible_mem_submonoidClosure {M : Type u_1} [CommMonoid M] [Subsingleton Mˣ] {S : Submonoid M} (hS : S.FG) : {p : M | p ∈ S ∧ Irreducible p}.Finite

A finitely generated submonoid of a monoid with a single unit has finitely many irreducible elements.

theorem AddSubmonoid.FG.finite_addIrreducible_mem_addSubmonoidClosure {M : Type u_1} [AddCommMonoid M] [Subsingleton (AddUnits M)] {S : AddSubmonoid M} (hS : S.FG) : {p : M | p ∈ S ∧ AddIrreducible p}.Finite

A finitely generated submonoid of an additive monoid with a single unit has finitely many irreducible elements.

theorem finite_irreducible {M : Type u_1} [CommMonoid M] [Subsingleton Mˣ] [Monoid.FG M] : {p : M | Irreducible p}.Finite

A finitely generated monoid with a single unit has finitely many irreducible elements.

theorem finite_addIrreducible {M : Type u_1} [AddCommMonoid M] [Subsingleton (AddUnits M)] [AddMonoid.FG M] : {p : M | AddIrreducible p}.Finite

A finitely generated additive monoid with a single unit has finitely many irreducible elements.

@[simp]

theorem Submonoid.closure_irreducible {M : Type u_1} [CancelCommMonoid M] [Subsingleton Mˣ] [Monoid.FG M] : closure {p : M | Irreducible p} = ⊤

A finitely generated cancellative monoid with a single unit is generated by its (finitely many) irreducible elements.

@[simp]

theorem AddSubmonoid.closure_addIrreducible {M : Type u_1} [AddCancelCommMonoid M] [Subsingleton (AddUnits M)] [AddMonoid.FG M] : closure {p : M | AddIrreducible p} = ⊤

A finitely generated cancellative additive monoid with a single unit is generated by its (finitely many) irreducible elements.