Semilinear sets are closed under intersection, set difference and complement

This file proves that the semilinear sets in any commutative monoid are closed under intersection and set difference. They are also closed under complement if the monoid is finitely generated. We prove these results on ℕ ^ k first (which are private APIs in this file) and then generalize to any commutative monoid.

Main Results

• isSemilinearSet_setOf_eq: the set of solutions to a linear equation a + f x = b + g y is semilinear.
• IsSemilinearSet.inter, IsSemilinearSet.diff: semilinear sets are closed under intersection and set difference.
• IsSemilinearSet.compl: semilinear sets in a finitely generated commutative monoid are closed under complement.

References

• Seymour Ginsburg and Edwin H. Spanier, Bounded ALGOL-Like Languages
• Samuel Eilenberg and M. P. Schützenberger, Rational Sets in Commutative Monoids

Semilinearity from slice property

A set s is said to have slice property if a + b + c ∈ s whenever a ∈ s, a + b ∈ s and a + c ∈ s. In ℕ ^ k, any set that has slice property is a semilinear set. This is an important lemma to prove the semilinearity of linear equation solutions.

Semilinearity of linear equations and preimages

theorem isSemilinearSet_setOf_eq {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddCommMonoid N] [AddMonoid.FG M] {F : Type u_5} {G : Type u_6} [FunLike F M N] [AddMonoidHomClass F M N] [FunLike G M N] [AddMonoidHomClass G M N] (a b : N) (f : F) (g : G) : IsSemilinearSet {x : M | a + f x = b + g x}

The set of solutions to a linear equation a + f x = b + g y in a finitely generated monoid is semilinear.

theorem Nat.isSemilinearSet_setOf_mulVec_eq {ι : Type u_3} {κ : Type u_4} [Fintype κ] (u v : ι → ℕ) (A B : Matrix ι κ ℕ) : IsSemilinearSet {x : κ → ℕ | u + A.mulVec x = v + B.mulVec x}

Matrix version of isSemilinearSet_setOf_eq.

theorem isLinearSet_iff_exists_fin_addMonoidHom {M : Type u_1} [AddCommMonoid M] {s : Set M} : IsLinearSet s ↔ ∃ (a : M) (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ Set.range ⇑f

theorem Nat.isLinearSet_iff_exists_matrix {ι : Type u_3} {s : Set (ι → ℕ)} : IsLinearSet s ↔ ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A.mulVec x_1 = x}

theorem IsSemilinearSet.preimage {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddCommMonoid N] [AddMonoid.FG M] {F : Type u_5} [FunLike F M N] [AddMonoidHomClass F M N] {s : Set N} (hs : IsSemilinearSet s) (f : F) : IsSemilinearSet (⇑f ⁻¹' s)

The preimage of a semilinear set under an homomorphism in a finitely generated monoid is semilinear.

Semilinear sets are included in finitely generated submonoids

theorem IsLinearSet.exists_fg_eq_subtypeVal {M : Type u_1} [AddCommMonoid M] {s : Set M} (hs : IsLinearSet s) : ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsLinearSet s' ∧ s = Subtype.val '' s'

theorem IsSemilinearSet.exists_fg_eq_subtypeVal {M : Type u_1} [AddCommMonoid M] {s : Set M} (hs : IsSemilinearSet s) : ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsSemilinearSet s' ∧ s = Subtype.val '' s'

theorem IsSemilinearSet.exists_fg_eq_subtypeVal₂ {M : Type u_1} [AddCommMonoid M] {s₁ s₂ : Set M} (hs₁ : IsSemilinearSet s₁) (hs₂ : IsSemilinearSet s₂) : ∃ (P : AddSubmonoid M) (s₁' : Set ↥P) (s₂' : Set ↥P), P.FG ∧ IsSemilinearSet s₁' ∧ s₁ = Subtype.val '' s₁' ∧ IsSemilinearSet s₂' ∧ s₂ = Subtype.val '' s₂'

Semilinearity of intersection

theorem IsSemilinearSet.inter {M : Type u_1} [AddCommMonoid M] {s₁ s₂ : Set M} (hs₁ : IsSemilinearSet s₁) (hs₂ : IsSemilinearSet s₂) : IsSemilinearSet (s₁ ∩ s₂)

Semilinear sets are closed under intersection.

theorem IsSemilinearSet.sInter {M : Type u_1} [AddCommMonoid M] [AddMonoid.FG M] {S : Set (Set M)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsSemilinearSet s) : IsSemilinearSet (⋂₀ S)

theorem IsSemilinearSet.iInter {M : Type u_1} {ι : Type u_3} [AddCommMonoid M] [AddMonoid.FG M] [Finite ι] {s : ι → Set M} (hs : ∀ (i : ι), IsSemilinearSet (s i)) : IsSemilinearSet (⋂ (i : ι), s i)

theorem IsSemilinearSet.biInter {M : Type u_1} {ι : Type u_3} [AddCommMonoid M] [AddMonoid.FG M] {s : Set ι} {t : ι → Set M} (hs : s.Finite) (ht : ∀ i ∈ s, IsSemilinearSet (t i)) : IsSemilinearSet (⋂ i ∈ s, t i)

theorem IsSemilinearSet.biInter_finset {M : Type u_1} {ι : Type u_3} [AddCommMonoid M] [AddMonoid.FG M] {s : Finset ι} {t : ι → Set M} (ht : ∀ i ∈ s, IsSemilinearSet (t i)) : IsSemilinearSet (⋂ i ∈ s, t i)

Semilinearity of complement and set difference

We first show that the complement of a proper linear set s in ℕ ^ k is semilinear, through several private definitions:

1. base, periods: the base vector and the set of periods of the proper linear set s.
2. basisSet, basis: the linearly independent periods of s can be extended to a basis of ℚ ^ k.
3. fundamentalDomain: the set of vectors in ℕ ^ k, starting from base, with coordinates under basis in [0, 1) ^ k.
4. floor, fract: every vector in ℕ ^ k can be decomposed into a ℤ-linear combination of basisSet and a vector in fundamentalDomain.
5. setOfFractNe, setOfFloorNeg, setOfFloorPos: the complement of s is decomposed into three semilinear sets.

Closure of semilinear sets under complement and set difference follows.

theorem IsSemilinearSet.diff {M : Type u_1} [AddCommMonoid M] {s₁ s₂ : Set M} (hs₁ : IsSemilinearSet s₁) (hs₂ : IsSemilinearSet s₂) : IsSemilinearSet (s₁ \ s₂)

Semilinear sets are closed under set difference.

theorem IsSemilinearSet.compl {M : Type u_1} [AddCommMonoid M] {s : Set M} [AddMonoid.FG M] (hs : IsSemilinearSet s) : IsSemilinearSet sᶜ

Semilinear sets in a finitely generated monoid are closed under complement.