Large sets in semigroups

DefinitionPiecewise syndetic subsets of a semigroup#✓fully proved

A set \(D\) in a semigroup \(S\) is piecewise syndetic when there is a finite set \(G \subseteq S\) such that for every finite set \(F \subseteq S\) there is \(x \in S\) with \(Fx \subseteq \bigcup_{t \in G} t^{-1} D\), where \(Fx = \{fx : f \in F\}\) and \(t^{-1} D = \{s \in S : ts \in D\}\).

def IsMulPiecewiseSyndetic (D : Set S) : Prop :=
  ∃ G : Finset S, ∀ F : Finset S, ∃ x : S, ∀ f ∈ F, ∃ t ∈ G, t * (f * x) ∈ D
Sources
  • Aninda Chakraborty and Sayan Goswami, An Analogue to the Infinitary Hales–Jewett Theorem, INTEGERS 24 (2024), Article A74, Section 2 (piecewise syndetic sets, after Hindman--Strauss).
Used by 3
Used byPiecewise syndetic sets contain Hales–Jewett configurations · A nonempty semigroup is piecewise syndetic in itself · The empty set is not piecewise syndetic in a semigroup

DefinitionJ-sets in a semigroup#✓fully proved

A set \(D\) in a semigroup \(S\) is a \(J\)-set when for every nonempty finite set \(F\) of sequences \(f : \mathbb{N} \to S\), where \(\mathbb{N} = \{0, 1, 2, \dots\}\), there are an integer \(m \ge 1\), elements \(a_1, \dots, a_{m+1} \in S\) and indices \(t_1 < \dots < t_m\) in \(\mathbb{N}\) such that \(a_1 f(t_1) a_2 f(t_2) \cdots a_m f(t_m) a_{m+1} \in D\) for every \(f \in F\).

def IsMulJSet (D : Set S) : Prop :=
  ∀ F : Finset (ℕ → S), F.Nonempty → ∃ (m : ℕ) (a : Fin (m + 2) → S) (t : Fin (m + 1) → ℕ),
    StrictMono t ∧ ∀ f ∈ F,
      (List.ofFn fun j : Fin m => a j.succ.castSucc * f (t j.succ)).foldl (· * ·)
          (a 0 * f (t 0)) * a (Fin.last (m + 1)) ∈ D
Sources
  • Aninda Chakraborty and Sayan Goswami, An Analogue to the Infinitary Hales–Jewett Theorem, INTEGERS 24 (2024), Article A74, Definition 2.4(3).
Used by 7
Used byJ-sets contain Hales–Jewett configurations · Variable patterns of variable words in J-sets · Variable-count sums of variable words in J-sets · C-sets in a semigroup · A nonempty semigroup is a J-set in itself · The empty set is not a C-set in a semigroup · The empty set is not a J-set in a nonempty semigroup

DefinitionCentral sets in a semigroup#✓fully proved

Let \(S\) be a semigroup and let \(\beta S\) be the set of ultrafilters on \(S\), with the product for which \(D \in pq\) exactly when \(\{x \in S : \{y \in S : xy \in D\} \in q\} \in p\). A two-sided ideal of \(\beta S\) is a set \(I \subseteq \beta S\) with \(rq \in I\) and \(qr \in I\) for all \(q \in I\) and \(r \in \beta S\). A set \(D \subseteq S\) is central when some \(p \in \beta S\) with \(pp = p\) lies in every nonempty two-sided ideal of \(\beta S\) and has \(D \in p\).

Equivalently, \(D \in p\) for a minimal idempotent \(p\), that is, an idempotent of the smallest two-sided ideal \(K(\beta S)\), which is itself a nonempty two-sided ideal lying in all of them.

def IsCentralSet (D : Set S) : Prop :=
  ∃ p : Ultrafilter S, p * p = p ∧
    (∀ I : Set (Ultrafilter S), I.Nonempty → (∀ q ∈ I, ∀ r, r * q ∈ I ∧ q * r ∈ I) → p ∈ I) ∧
    D ∈ p
Sources
  • Aninda Chakraborty and Sayan Goswami, An Analogue to the Infinitary Hales–Jewett Theorem, INTEGERS 24 (2024), Article A74, Section 2.1 (central sets).
Used by 2
Used byInfinitary Hales–Jewett configurations in central sets · The empty set is not central in a semigroup

DefinitionC-sets in a semigroup#✓fully proved

Let \(S\) be a semigroup and let \(\beta S\) be the set of ultrafilters on \(S\), with the product for which \(D \in pq\) exactly when \(\{x \in S : \{y \in S : xy \in D\} \in q\} \in p\). Let \(J(S)\) be the set of ultrafilters on \(S\) all of whose members are \(J\)-sets. A set \(D \subseteq S\) is a \(C\)-set when \(D \in p\) for some \(p \in J(S)\) with \(pp = p\).

def IsCSet (D : Set S) : Prop :=
  ∃ p : Ultrafilter S, p * p = p ∧ (∀ B ∈ p, IsMulJSet B) ∧ D ∈ p
Sources
  • Aninda Chakraborty and Sayan Goswami, An Analogue to the Infinitary Hales–Jewett Theorem, INTEGERS 24 (2024), Article A74, Definition 2.4(3) (C-sets).
Uses 1 · Used by 4
Statement usesJ-sets in a semigroup
Used byInfinitary Hales–Jewett configurations in C-sets · Variable patterns of variable words in C-sets · Variable-count sums of variable words in C-sets · The empty set is not a C-set in a semigroup

TheoremA nonempty semigroup is piecewise syndetic in itself#✓fully proved

If \(S\) is a nonempty semigroup, then \(S\) is a piecewise syndetic subset of \(S\).

theorem isMulPiecewiseSyndetic_univ [Nonempty S] : IsMulPiecewiseSyndetic (Set.univ : Set S)
Sources
  • Aninda Chakraborty and Sayan Goswami, An Analogue to the Infinitary Hales–Jewett Theorem, INTEGERS 24 (2024), Article A74, Section 2 (piecewise syndetic sets).
Uses 1
Statement usesPiecewise syndetic subsets of a semigroup

TheoremThe empty set is not piecewise syndetic in a semigroup#✓fully proved

In every semigroup \(S\), the empty subset of \(S\) is not piecewise syndetic.

theorem not_isMulPiecewiseSyndetic_empty : ¬ IsMulPiecewiseSyndetic (∅ : Set S)
Sources
  • Aninda Chakraborty and Sayan Goswami, An Analogue to the Infinitary Hales–Jewett Theorem, INTEGERS 24 (2024), Article A74, Section 2 (piecewise syndetic sets).
Uses 1
Statement usesPiecewise syndetic subsets of a semigroup

TheoremA nonempty semigroup is a J-set in itself#✓fully proved

If \(S\) is a nonempty semigroup, then \(S\) is a \(J\)-set in \(S\).

theorem isMulJSet_univ [Nonempty S] : IsMulJSet (Set.univ : Set S)
Sources
  • Aninda Chakraborty and Sayan Goswami, An Analogue to the Infinitary Hales–Jewett Theorem, INTEGERS 24 (2024), Article A74, Definition 2.4(3).
Uses 1
Statement usesJ-sets in a semigroup

TheoremThe empty set is not a J-set in a nonempty semigroup#✓fully proved

If \(S\) is a nonempty semigroup, then the empty subset of \(S\) is not a \(J\)-set.

theorem not_isMulJSet_empty [Nonempty S] : ¬ IsMulJSet (∅ : Set S)
Sources
  • Aninda Chakraborty and Sayan Goswami, An Analogue to the Infinitary Hales–Jewett Theorem, INTEGERS 24 (2024), Article A74, Definition 2.4(3).
Uses 1
Statement usesJ-sets in a semigroup

TheoremThe empty set is not central in a semigroup#✓fully proved

In every semigroup \(S\), the empty subset of \(S\) is not central.

theorem not_isCentralSet_empty : ¬ IsCentralSet (∅ : Set S)
Sources
  • Aninda Chakraborty and Sayan Goswami, An Analogue to the Infinitary Hales–Jewett Theorem, INTEGERS 24 (2024), Article A74, Section 2.1 (central sets).
Uses 1
Statement usesCentral sets in a semigroup

TheoremThe empty set is not a C-set in a semigroup#✓fully proved

In every semigroup \(S\), the empty subset of \(S\) is not a \(C\)-set.

theorem not_isCSet_empty : ¬ IsCSet (∅ : Set S)
Sources
  • Aninda Chakraborty and Sayan Goswami, An Analogue to the Infinitary Hales–Jewett Theorem, INTEGERS 24 (2024), Article A74, Definition 2.4(3) (C-sets).
Uses 2
Statement usesC-sets in a semigroup
Proof usesJ-sets in a semigroup
10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.