Semigroup ideals

This file defines (left) semigroup ideals (also called monoid ideals sometimes), which are sets s in a semigroup such that a * b ∈ s whenever b ∈ s. Note that semigroup ideals are different from ring ideals (Ideal in Mathlib): a ring ideal is a semigroup ideal that is also an additive submonoid of the ring.

References

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

@[reducible, inline]

abbrev SemigroupIdeal (M : Type u_1) [Mul M] : Type u_1

A (left) semigroup ideal in a semigroup M is a set s such that a * b ∈ s whenever b ∈ s.

@[reducible, inline]

abbrev AddSemigroupIdeal (M : Type u_1) [Add M] : Type u_1

A (left) additive semigroup ideal in an additive semigroup M is a set s such that a + b ∈ s whenever b ∈ s.

theorem SemigroupIdeal.mul_mem {M : Type u_1} [Mul M] (I : SemigroupIdeal M) (x : M) {y : M} : y ∈ I → x * y ∈ I

theorem AddSemigroupIdeal.add_mem {M : Type u_1} [Add M] (I : AddSemigroupIdeal M) (x : M) {y : M} : y ∈ I → x + y ∈ I

@[reducible, inline]

abbrev SemigroupIdeal.closure {M : Type u_1} [Mul M] (s : Set M) : SemigroupIdeal M

The semigroup ideal generated by a set s.

@[reducible, inline]

abbrev AddSemigroupIdeal.closure {M : Type u_1} [Add M] (s : Set M) : AddSemigroupIdeal M

The additive semigroup ideal generated by a set s.

theorem SemigroupIdeal.mem_closure {M : Type u_1} [Mul M] {s : Set M} {x : M} : x ∈ closure s ↔ ∀ (p : SemigroupIdeal M), s ⊆ ↑p → x ∈ p

theorem AddSemigroupIdeal.mem_closure {M : Type u_1} [Add M] {s : Set M} {x : M} : x ∈ closure s ↔ ∀ (p : AddSemigroupIdeal M), s ⊆ ↑p → x ∈ p

theorem SemigroupIdeal.subset_closure {M : Type u_1} [Mul M] {s : Set M} : s ⊆ ↑(closure s)

theorem AddSemigroupIdeal.subset_closure {M : Type u_1} [Add M] {s : Set M} : s ⊆ ↑(closure s)

theorem SemigroupIdeal.mem_closure_of_mem {M : Type u_1} [Mul M] {s : Set M} {x : M} (hx : x ∈ s) : x ∈ closure s

theorem AddSemigroupIdeal.mem_closure_of_mem {M : Type u_1} [Add M] {s : Set M} {x : M} (hx : x ∈ s) : x ∈ closure s

theorem SemigroupIdeal.closure_le {M : Type u_1} [Mul M] {s : Set M} {I : SemigroupIdeal M} : closure s ≤ I ↔ s ⊆ ↑I

theorem AddSemigroupIdeal.closure_le {M : Type u_1} [Add M] {s : Set M} {I : AddSemigroupIdeal M} : closure s ≤ I ↔ s ⊆ ↑I

theorem SemigroupIdeal.closure_mono {M : Type u_1} [Mul M] {s t : Set M} (h : s ⊆ t) : closure s ≤ closure t

theorem AddSemigroupIdeal.closure_mono {M : Type u_1} [Add M] {s t : Set M} (h : s ⊆ t) : closure s ≤ closure t

theorem SemigroupIdeal.coe_closure {M : Type u_1} [Semigroup M] {s : Set M} : ↑(closure s) = s ∪ Set.univ * s

The semigroup ideal generated by s is s ∪ Set.univ * s.

theorem AddSemigroupIdeal.coe_closure {M : Type u_1} [AddSemigroup M] {s : Set M} : ↑(closure s) = s ∪ (Set.univ + s)

The additive semigroup ideal generated by s is s ∪ Set.univ + s.

theorem SemigroupIdeal.mem_closure' {M : Type u_1} [Semigroup M] {s : Set M} {x : M} : x ∈ closure s ↔ x ∈ s ∨ ∃ (y : M), ∃ z ∈ s, y * z = x

The semigroup ideal generated by s is s ∪ Set.univ * s.

theorem AddSemigroupIdeal.mem_closure' {M : Type u_1} [AddSemigroup M] {s : Set M} {x : M} : x ∈ closure s ↔ x ∈ s ∨ ∃ (y : M), ∃ z ∈ s, y + z = x

The additive semigroup ideal generated by s is s ∪ Set.univ + s.

theorem SemigroupIdeal.coe_closure' {M : Type u_1} [Monoid M] {s : Set M} : ↑(closure s) = Set.univ * s

In a monoid, the semigroup ideal generated by s is Set.univ * s.

theorem AddSemigroupIdeal.coe_closure' {M : Type u_1} [AddMonoid M] {s : Set M} : ↑(closure s) = Set.univ + s

In an additive monoid, the semigroup ideal generated by s is Set.univ + s.

theorem SemigroupIdeal.mem_closure'' {M : Type u_1} [Monoid M] {s : Set M} {x : M} : x ∈ closure s ↔ ∃ (y : M), ∃ z ∈ s, y * z = x

In a monoid, the semigroup ideal generated by s is Set.univ * s.

theorem AddSemigroupIdeal.mem_closure'' {M : Type u_1} [AddMonoid M] {s : Set M} {x : M} : x ∈ closure s ↔ ∃ (y : M), ∃ z ∈ s, y + z = x

In an additive monoid, the semigroup ideal generated by s is Set.univ + s.

def SemigroupIdeal.FG {M : Type u_1} [Mul M] (I : SemigroupIdeal M) : Prop

A semigroup ideal is finitely generated if it is generated by a finite set.

This is defeq to SubMulAction.FG, but unfolds more nicely.

def AddSemigroupIdeal.FG {M : Type u_1} [Add M] (I : AddSemigroupIdeal M) : Prop

An additive semigroup ideal is finitely generated if it is generated by a finite set.

This is defeq to SubAddAction.FG, but unfolds more nicely.

theorem SemigroupIdeal.fg_iff {M : Type u_1} [Mul M] {I : SemigroupIdeal M} : I.FG ↔ ∃ (s : Finset M), I = closure ↑s

theorem AddSemigroupIdeal.fg_iff {M : Type u_1} [Add M] {I : AddSemigroupIdeal M} : I.FG ↔ ∃ (s : Finset M), I = closure ↑s