Semigroup ideals in a canonically ordered and well-quasi-ordered monoid

This file proves that in a canonically ordered and well-quasi-ordered monoid, any semigroup ideal is finitely generated, and the semigroup ideals satisfy the ascending chain condition.

References

• Samuel Eilenberg and M. P. Schützenberger, Rational Sets in Commutative Monoids

theorem SemigroupIdeal.fg_of_wellQuasiOrderedLE {M : Type u_1} [CommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [CanonicallyOrderedMul M] (I : SemigroupIdeal M) : I.FG

In a canonically ordered and well-quasi-ordered monoid, any semigroup ideal is finitely generated.

theorem AddSemigroupIdeal.fg_of_wellQuasiOrderedLE {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [CanonicallyOrderedAdd M] (I : AddSemigroupIdeal M) : I.FG

In a canonically ordered and well-quasi-ordered additive monoid, any semigroup ideal is finitely generated.

instance SemigroupIdeal.instWellFoundedGT {M : Type u_1} [CommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [CanonicallyOrderedMul M] : WellFoundedGT (SemigroupIdeal M)

In a canonically ordered and well-quasi-ordered monoid, the semigroup ideals satisfy the ascending chain condition.

instance AddSemigroupIdeal.instWellFoundedGT {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [CanonicallyOrderedAdd M] : WellFoundedGT (AddSemigroupIdeal M)

A canonically ordered and well-quasi-ordered additive monoid, the semigroup ideals satisfy the ascending chain condition.