Linear and semilinear sets

This file defines linear and semilinear sets. In an AddCommMonoid, a linear set is a coset of a finitely generated additive submonoid, and a semilinear set is a finite union of linear sets.

We prove that semilinear sets are closed under union, projection, set addition and additive closure. We also prove that any semilinear set can be decomposed into a finite union of proper linear sets, which are linear sets with linearly independent submonoid generators (periods).

Main Definitions

• IsLinearSet: a set is linear if it is a coset of a finitely generated additive submonoid.
• IsSemilinearSet: a set is semilinear if it is a finite union of linear sets.
• IsProperLinearSet: a linear set is proper if its submonoid generators (periods) are linearly independent.
• IsProperSemilinearSet: a semilinear set is proper if it is a finite union of proper linear sets.

Main Results

• IsSemilinearSet is closed under union, projection, set addition and additive closure.
• IsSemilinearSet.isProperSemilinearSet: every semilinear set is a finite union of proper linear sets.

Naming convention

IsSemilinearSet.proj projects a semilinear set of ι ⊕ κ → M to ι → M by taking Sum.inl on the index. It is a special case of IsSemilinearSet.image, and is useful in proving semilinearity of sets in form { x | ∃ y, p x y }.

References

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

def IsLinearSet {M : Type u_1} [AddCommMonoid M] (s : Set M) : Prop

A set is linear if it is a coset of a finitely generated additive submonoid.

Equations

• IsLinearSet s = ∃ (a : M) (t : Set M), t.Finite ∧ s = a +ᵥ ↑(AddSubmonoid.closure t)

theorem isLinearSet_iff {M : Type u_1} [AddCommMonoid M] {s : Set M} : IsLinearSet s ↔ ∃ (a : M) (t : Finset M), s = a +ᵥ ↑(AddSubmonoid.closure ↑t)

An equivalent expression of IsLinearSet in terms of Finset instead of Set.Finite.

@[simp]

theorem IsLinearSet.singleton {M : Type u_1} [AddCommMonoid M] (a : M) : IsLinearSet {a}

theorem IsLinearSet.closure_finset {M : Type u_1} [AddCommMonoid M] (s : Finset M) : IsLinearSet ↑(AddSubmonoid.closure ↑s)

theorem IsLinearSet.closure_of_finite {M : Type u_1} [AddCommMonoid M] {s : Set M} (hs : s.Finite) : IsLinearSet ↑(AddSubmonoid.closure s)

theorem isLinearSet_iff_exists_fg_eq_vadd {M : Type u_1} [AddCommMonoid M] {s : Set M} : IsLinearSet s ↔ ∃ (a : M) (P : AddSubmonoid M), P.FG ∧ s = a +ᵥ ↑P

theorem IsLinearSet.of_fg {M : Type u_1} [AddCommMonoid M] {P : AddSubmonoid M} (hP : P.FG) : IsLinearSet ↑P

@[simp]

theorem IsLinearSet.univ {M : Type u_1} [AddCommMonoid M] [AddMonoid.FG M] : IsLinearSet Set.univ

theorem IsLinearSet.vadd {M : Type u_1} [AddCommMonoid M] {s : Set M} (a : M) (hs : IsLinearSet s) : IsLinearSet (a +ᵥ s)

theorem IsLinearSet.add {M : Type u_1} [AddCommMonoid M] {s₁ s₂ : Set M} (hs₁ : IsLinearSet s₁) (hs₂ : IsLinearSet s₂) : IsLinearSet (s₁ + s₂)

theorem IsLinearSet.image {M : Type u_1} {N : Type u_2} {F : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [FunLike F M N] [AddMonoidHomClass F M N] {s : Set M} (hs : IsLinearSet s) (f : F) : IsLinearSet (⇑f '' s)

def IsSemilinearSet {M : Type u_1} [AddCommMonoid M] (s : Set M) : Prop

A set is semilinear if it is a finite union of linear sets.

Equations

• IsSemilinearSet s = ∃ (S : Set (Set M)), S.Finite ∧ (∀ t ∈ S, IsLinearSet t) ∧ s = ⋃₀ S

theorem IsLinearSet.isSemilinearSet {M : Type u_1} [AddCommMonoid M] {s : Set M} (h : IsLinearSet s) : IsSemilinearSet s

@[simp]

theorem IsSemilinearSet.empty {M : Type u_1} [AddCommMonoid M] : IsSemilinearSet ∅

@[simp]

theorem IsSemilinearSet.singleton {M : Type u_1} [AddCommMonoid M] (a : M) : IsSemilinearSet {a}

theorem IsSemilinearSet.closure_finset {M : Type u_1} [AddCommMonoid M] (s : Finset M) : IsSemilinearSet ↑(AddSubmonoid.closure ↑s)

theorem IsSemilinearSet.closure_of_finite {M : Type u_1} [AddCommMonoid M] {s : Set M} (hs : s.Finite) : IsSemilinearSet ↑(AddSubmonoid.closure s)

theorem IsSemilinearSet.of_fg {M : Type u_1} [AddCommMonoid M] {P : AddSubmonoid M} (hP : P.FG) : IsSemilinearSet ↑P

@[simp]

theorem IsSemilinearSet.univ {M : Type u_1} [AddCommMonoid M] [AddMonoid.FG M] : IsSemilinearSet Set.univ

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

Semilinear sets are closed under union.

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

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

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

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

theorem IsSemilinearSet.of_finite {M : Type u_1} [AddCommMonoid M] {s : Set M} (hs : s.Finite) : IsSemilinearSet s

theorem IsSemilinearSet.vadd {M : Type u_1} [AddCommMonoid M] {s : Set M} (a : M) (hs : IsSemilinearSet s) : IsSemilinearSet (a +ᵥ s)

theorem IsSemilinearSet.add {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 addition.

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

theorem isSemilinearSet_image_iff {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddCommMonoid N] {s : Set M} {F : Type u_6} [EquivLike F M N] [AddEquivClass F M N] (f : F) : IsSemilinearSet (⇑f '' s) ↔ IsSemilinearSet s

theorem IsSemilinearSet.proj {M : Type u_1} {ι : Type u_3} {κ : Type u_4} [AddCommMonoid M] {s : Set (ι ⊕ κ → M)} (hs : IsSemilinearSet s) : IsSemilinearSet {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s}

Semilinear sets are closed under projection (from ι ⊕ κ → M to ι → M by taking Sum.inl on the index). It is a special case of IsSemilinearSet.image.

theorem IsSemilinearSet.proj' {M : Type u_1} {ι : Type u_3} {κ : Type u_4} [AddCommMonoid M] {p : (ι → M) → (κ → M) → Prop} : IsSemilinearSet {x : ι ⊕ κ → M | p (x ∘ Sum.inl) (x ∘ Sum.inr)} → IsSemilinearSet {x : ι → M | ∃ (y : κ → M), p x y}

A variant of Semilinear.proj for backward reasoning.

theorem IsLinearSet.closure {M : Type u_1} [AddCommMonoid M] {s : Set M} (hs : IsLinearSet s) : IsSemilinearSet ↑(AddSubmonoid.closure s)

theorem IsSemilinearSet.closure {M : Type u_1} [AddCommMonoid M] {s : Set M} (hs : IsSemilinearSet s) : IsSemilinearSet ↑(AddSubmonoid.closure s)

Semilinear sets are closed under additive closure.

def IsProperLinearSet {M : Type u_1} [AddCommMonoid M] (s : Set M) : Prop

A linear set is proper if its submonoid generators (periods) are linearly independent.

Equations

• IsProperLinearSet s = ∃ (a : M) (t : Set M), t.Finite ∧ LinearIndepOn ℕ id t ∧ s = a +ᵥ ↑(AddSubmonoid.closure t)

theorem isProperLinearSet_iff {M : Type u_1} [AddCommMonoid M] {s : Set M} : IsProperLinearSet s ↔ ∃ (a : M) (t : Finset M), LinearIndepOn ℕ id ↑t ∧ s = a +ᵥ ↑(AddSubmonoid.closure ↑t)

theorem IsProperLinearSet.isLinearSet {M : Type u_1} [AddCommMonoid M] {s : Set M} (hs : IsProperLinearSet s) : IsLinearSet s

@[simp]

theorem IsProperLinearSet.singleton {M : Type u_1} [AddCommMonoid M] (a : M) : IsProperLinearSet {a}

def IsProperSemilinearSet {M : Type u_1} [AddCommMonoid M] (s : Set M) : Prop

A semilinear set is proper if it is a finite union of proper linear sets.

Equations

• IsProperSemilinearSet s = ∃ (S : Set (Set M)), S.Finite ∧ (∀ t ∈ S, IsProperLinearSet t) ∧ s = ⋃₀ S

theorem IsProperSemilinearSet.isSemilinearSet {M : Type u_1} [AddCommMonoid M] {s : Set M} (hs : IsProperSemilinearSet s) : IsSemilinearSet s

theorem IsProperLinearSet.isProperSemilinearSet {M : Type u_1} [AddCommMonoid M] {s : Set M} (hs : IsProperLinearSet s) : IsProperSemilinearSet s

@[simp]

theorem IsProperSemilinearSet.empty {M : Type u_1} [AddCommMonoid M] : IsProperSemilinearSet ∅

theorem IsProperSemilinearSet.union {M : Type u_1} [AddCommMonoid M] {s₁ s₂ : Set M} (hs₁ : IsProperSemilinearSet s₁) (hs₂ : IsProperSemilinearSet s₂) : IsProperSemilinearSet (s₁ ∪ s₂)

theorem IsProperSemilinearSet.sUnion {M : Type u_1} [AddCommMonoid M] {S : Set (Set M)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsProperSemilinearSet s) : IsProperSemilinearSet (⋃₀ S)

theorem IsProperSemilinearSet.biUnion {M : Type u_1} {ι : Type u_3} [AddCommMonoid M] {s : Set ι} {t : ι → Set M} (hs : s.Finite) (ht : ∀ i ∈ s, IsProperSemilinearSet (t i)) : IsProperSemilinearSet (⋃ i ∈ s, t i)

theorem IsProperSemilinearSet.biUnion_finset {M : Type u_1} {ι : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : ι → Set M} (ht : ∀ i ∈ s, IsProperSemilinearSet (t i)) : IsProperSemilinearSet (⋃ i ∈ s, t i)

theorem IsLinearSet.isProperSemilinearSet {M : Type u_1} [AddCommMonoid M] {s : Set M} [IsCancelAdd M] (hs : IsLinearSet s) : IsProperSemilinearSet s

theorem IsSemilinearSet.isProperSemilinearSet {M : Type u_1} [AddCommMonoid M] {s : Set M} [IsCancelAdd M] (hs : IsSemilinearSet s) : IsProperSemilinearSet s

The proper decomposition of semilinear sets: every semilinear set is a finite union of proper linear sets.