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.
• Nat.isSemilinearSet_iff_ultimately_periodic: A set of ℕ is semilinear if and only if it is ultimately periodic, i.e. periodic after some number k.

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 isSemilinearSet_iff {M : Type u_1} [AddCommMonoid M] {s : Set M} : IsSemilinearSet s ↔ ∃ (S : Finset (Set M)), (∀ t ∈ S, IsLinearSet t) ∧ s = ⋃₀ ↑S

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

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)

The image of a semilinear set under a homomorphism is semilinear.

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 IsSemilinearSet.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)

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

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_iff {M : Type u_1} [AddCommMonoid M] {s : Set M} : IsProperSemilinearSet s ↔ ∃ (S : Finset (Set M)), (∀ t ∈ S, IsProperLinearSet t) ∧ s = ⋃₀ ↑S

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

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.

theorem Nat.isSemilinearSet_iff_ultimately_periodic {s : Set ℕ} : IsSemilinearSet s ↔ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s

A set of ℕ is semilinear if and only if it is ultimately periodic, i.e. periodic after some number k.