Pin's algebraic characterization of subregular language classes

The classical algebraic-automata-theory characterization of four basic subregular varieties via omega-power equations on the syntactic monoid:

Variety	Equation	Meaning
𝒟 (definite)	s · [w]^ω = [w]^ω	left-absorbing
𝒦 (reverse-definite)	[w]^ω · s = [w]^ω	right-absorbing
𝒩 (co/finite)	both 𝒟's and 𝒦's	both-sided absorbing
ℒℐ (generalized definite)	[w]^ω · s · [w]^ω = [w]^ω	sandwich-absorbing

Where [w]^ω = Monoid.omegaPow (L.syntacticClass w) is the unique idempotent in the cyclic submonoid of [w] (see Linglib/Core/Algebra/IdempotentPower.lean). The variables s range over L.syntacticMonoid and w over non-empty List α (alphabet-relativized form — see Equations.lean for the trivial-letter counterexample motivating the non-empty-w restriction).

Why omega-power and not finite-k?

[Lam26] Props 53/57 (in Equations.lean) give finite-k characterizations parameterized by the suffix/prefix length k. Pin's forms are the unbounded versions: a single k-free equation in the syntactic monoid characterizes membership in the variety. The omegaPow substrate is what eliminates the k parameter.

The two characterizations cohere: L.IsDefinite k → kDefiniteEquation L k is the finite-k half; (∃ k, L.IsDefinite k) ↔ pinDefiniteEquation L is the unbounded half. The unbounded form is the natural Pin/Eilenberg form used throughout algebraic automata theory.

Main definitions

• Language.pinDefiniteEquation L — s · [w]^ω = [w]^ω.
• Language.pinReverseDefiniteEquation L — [w]^ω · s = [w]^ω.
• Language.pinCofiniteEquation L — conjunction of the above two.
• Language.pinGeneralizedDefiniteEquation L — [w]^ω · s · [w]^ω = [w]^ω.

All four require [Finite L.syntacticMonoid] (equivalent to L being regular, by IsRegular.finite_syntacticMonoid).

Main results

• Language.exists_isDefinite_iff_satisfies_pinDefiniteEquation — Pin's 𝒟-iff.
• Language.exists_isReverseDefinite_iff_satisfies_pinReverseDefiniteEquation — Pin's 𝒦-iff.
• Language.isFiniteOrCofinite_iff_satisfies_pinCofiniteEquation — Pin's 𝒩-iff (additionally requires [Finite α]; the language-level reverse direction in Subregular/Language/Definite.lean does not hold for infinite alphabets).
• Language.exists_isGeneralizedDefinite_iff_satisfies_pinGeneralizedDefiniteEquation — Pin's ℒℐ-iff. The reverse direction uses the same prefix-pigeonhole template as 𝒟/𝒦, replacing one-sided absorption with the LI sandwich identity (sandwich_absorbing_of_pin_pigeonhole).

Future work: replace the pigeonhole proofs with the kernel structure

The *_pin_pigeonhole lemmas reprove by hand, for special cases, the structure of the minimal ideal (kernel) of a finite syntactic monoid. Once Green's relations and the Rees–Sushkevich theorem land in mathlib (in progress upstream: the Mathlib.Algebra.Group.GreensRelations development plus idempotent powers in finite semigroups), these characterizations should be rewritten as corollaries of the kernel being a band, which dissolves the pigeonhole entirely:

• 𝒟 (definite) ⟺ the kernel is a right-zero band;
• 𝒦 (reverse-definite) ⟺ the kernel is a left-zero band;
• ℒℐ (generalized definite) ⟺ the kernel is a rectangular band;
• 𝒩 (co/finite) ⟺ the kernel is trivial.

Reference points for that rewrite: Rees–Sushkevich ([pin-mfa] Ch. V Thm 3.33), the minimal ideal of a finite semigroup ([pin-mfa] Ch. V Prop 4.37), and the aperiodic-simple = rectangular-band classification ([pin-mfa] Ch. V Cor 3.34). Do not fork that substrate here; consume it from mathlib when it merges.

References

• [Pin].
• [Eil76].
• [Alm95].
• [PRS63] (the original definite/reverse-definite/ generalized-definite hierarchy).
• [McNP71] (variety theory of finite monoids).
• [Lam26] §6.2 (finite-k companion in Equations.lean).

def Language.pinDefiniteEquation {α : Type u_1} (L : Language α) [Finite L.syntacticMonoid] : Prop

Pin's algebraic equation for definite languages: ∀ s : L.syntacticMonoid, ∀ w : List α, w ≠ [] → s · [w]^ω = [w]^ω.

The non-empty w quantifier (alphabet-relativized form) handles the trivial-letter case the same way kDefiniteEquation does — see the counterexample in Equations.lean. Despite living in a sibling file to Lambert's kDefiniteEquation, this is a classical Pin/Eilenberg omega-power equation, not Lambert-specific — hence the namespace is Language (no author-named namespace).

Equations

• L.pinDefiniteEquation = ∀ (s : L.syntacticMonoid) (w : List α), w ≠ [] → s * Monoid.omegaPow (L.syntacticClass w) = Monoid.omegaPow (L.syntacticClass w)

theorem Language.IsDefinite.satisfies_pinDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} [Finite L.syntacticMonoid] (hk : L.IsDefinite k) : L.pinDefiniteEquation

Pin's theorem (forward direction): if L is k-definite for some k, then its syntactic monoid satisfies Pin's omega-power equation.

Proof: reduce to IsDefinite.satisfies_kDefiniteEquation plus the absorbing-power trick — [w]^ω = [w]^N for some N, and by idempotence [w]^N = [w]^(N·k) whenever k ≥ 1, giving a long-enough representative w^(N·k) (length N·k·|w| ≥ k) of [w]^ω. The k = 0 case forces the syntactic monoid to be trivial, so the equation holds vacuously.

theorem Language.exists_isDefinite_of_satisfies_pinDefiniteEquation {α : Type u_1} {L : Language α} [Finite L.syntacticMonoid] (h : L.pinDefiniteEquation) : ∃ (k : ℕ), L.IsDefinite k

Pin's theorem (reverse direction): if a regular language's syntactic monoid satisfies Pin's omega-power equation, then L is k-definite for some k (specifically, k = Fintype.card L.syntacticMonoid).

theorem Language.exists_isDefinite_iff_satisfies_pinDefiniteEquation {α : Type u_1} {L : Language α} [Finite L.syntacticMonoid] : (∃ (k : ℕ), L.IsDefinite k) ↔ L.pinDefiniteEquation

Pin's theorem: a language is k-definite for some k iff its (necessarily finite) syntactic monoid satisfies Pin's omega-power equation.

def Language.pinReverseDefiniteEquation {α : Type u_1} (L : Language α) [Finite L.syntacticMonoid] : Prop

Pin's algebraic equation for reverse-definite languages ([Lam26] Prop 57 limit; [Alm95]): ∀ s : L.syntacticMonoid, ∀ w : List α, w ≠ [] → [w]^ω · s = [w]^ω.

Mirror of pinDefiniteEquation with right-multiplication instead of left. Same alphabet-relativized non-empty w quantifier.

Equations

• L.pinReverseDefiniteEquation = ∀ (s : L.syntacticMonoid) (w : List α), w ≠ [] → Monoid.omegaPow (L.syntacticClass w) * s = Monoid.omegaPow (L.syntacticClass w)

theorem Language.IsReverseDefinite.satisfies_pinReverseDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} [Finite L.syntacticMonoid] (hk : L.IsReverseDefinite k) : L.pinReverseDefiniteEquation

Pin's K-theorem (forward direction): a reverse-k-definite language's syntactic monoid satisfies Pin's right-absorbing omega-power equation. Mirror of IsDefinite.satisfies_pinDefiniteEquation.

theorem Language.exists_isReverseDefinite_of_satisfies_pinReverseDefiniteEquation {α : Type u_1} {L : Language α} [Finite L.syntacticMonoid] (h : L.pinReverseDefiniteEquation) : ∃ (k : ℕ), L.IsReverseDefinite k

Pin's K-theorem (reverse direction): if a regular language's syntactic monoid satisfies Pin's reverse-definite omega-power equation, then L is reverse-k-definite for some k.

theorem Language.exists_isReverseDefinite_iff_satisfies_pinReverseDefiniteEquation {α : Type u_1} {L : Language α} [Finite L.syntacticMonoid] : (∃ (k : ℕ), L.IsReverseDefinite k) ↔ L.pinReverseDefiniteEquation

Pin's K-theorem: a language is reverse-k-definite for some k iff its (necessarily finite) syntactic monoid satisfies Pin's reverse-definite omega-power equation.

def Language.pinCofiniteEquation {α : Type u_1} (L : Language α) [Finite L.syntacticMonoid] : Prop

Pin's algebraic equation for co/finite languages ([Lam26] Prop 59; [Alm95]): 𝒩 = ⟦sx^ω = x^ω = x^ω s⟧. The conjunction of D's left-absorbing equation and K's right-absorbing equation.

Equations

• L.pinCofiniteEquation = (L.pinDefiniteEquation ∧ L.pinReverseDefiniteEquation)

theorem Language.IsFiniteOrCofinite.satisfies_pinCofiniteEquation {α : Type u_1} {L : Language α} [Finite L.syntacticMonoid] (h : L.IsFiniteOrCofinite) : L.pinCofiniteEquation

Pin's N-theorem (forward direction): a finite-or-cofinite language's syntactic monoid satisfies the conjunction of Pin's D and K omega-power equations. Composes the substrate lemma IsFiniteOrCofinite.exists_isDefinite_and_isReverseDefinite (in Subregular/Language/Definite.lean) with the Pin D and Pin K iff theorems.

theorem Language.isFiniteOrCofinite_of_satisfies_pinCofiniteEquation {α : Type u_1} [Finite α] {L : Language α} [Finite L.syntacticMonoid] (h : L.pinCofiniteEquation) : L.IsFiniteOrCofinite

Pin's N-theorem (reverse direction, α-finite case): if a language over a finite alphabet has a syntactic monoid satisfying both Pin's D and K equations, then it is finite-or-cofinite.

Requires [Finite α] because the language-level reverse direction (isFiniteOrCofinite_of_isDefinite_and_isReverseDefinite in Subregular/Language/Definite.lean) needs it: with infinite α, words of bounded length need not form a finite set.

theorem Language.isFiniteOrCofinite_iff_satisfies_pinCofiniteEquation {α : Type u_1} [Finite α] {L : Language α} [Finite L.syntacticMonoid] : L.IsFiniteOrCofinite ↔ L.pinCofiniteEquation

Pin's N-theorem: over a finite alphabet, a language is finite-or-cofinite iff its syntactic monoid satisfies the conjunction of Pin's D and K omega-power equations.

def Language.pinGeneralizedDefiniteEquation {α : Type u_1} (L : Language α) [Finite L.syntacticMonoid] : Prop

Pin's algebraic equation for generalized-definite languages ([Lam26] Prop 58 limit, simplified form; [Str85]): ℒℐ = ⟦x^ω · s · x^ω = x^ω⟧. Sandwiching s between two copies of the same omega-power absorbs s.

Lambert (paper p. 25) notes this simplified one-variable form is equivalent to the more general two-variable form x^ω · s · z^ω = x^ω · z^ω; the equivalence proof itself uses omega-power idempotence.

Equations

• One or more equations did not get rendered due to their size.

theorem Language.IsGeneralizedDefinite.satisfies_pinGeneralizedDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} [Finite L.syntacticMonoid] (hk : L.IsGeneralizedDefinite k) : L.pinGeneralizedDefiniteEquation

Pin's ℒℐ-theorem (forward direction): a generalized-k-definite language's syntactic monoid satisfies the LI omega-power equation.

Strategy: pick v = w^(N·k) long enough (length ≥ k); apply L.IsGeneralizedDefinite k directly to the pair (v ++ s' ++ v, v) — both have the same length-k left-prefix (the first k chars of v) and same length-k right-suffix (the last k chars of v). The omega-power identity [w]^N · s · [w]^N = [w]^N follows by lifting through [w]^(N·k) = omegaPow [w].

theorem Language.exists_isGeneralizedDefinite_of_satisfies_pinGeneralizedDefiniteEquation {α : Type u_1} {L : Language α} [Finite L.syntacticMonoid] (h : L.pinGeneralizedDefiniteEquation) : ∃ (k : ℕ), L.IsGeneralizedDefinite k

Pin's ℒℐ-theorem (reverse direction): if a regular language's syntactic monoid satisfies Pin's LI omega-power equation, then L is generalized-k-definite for some k (specifically, k = Nat.card L.syntacticMonoid).

Proof: sandwich_absorbing_of_pinGeneralizedDefiniteEquation lifts the omega-power equation to a finite-k sandwich on length-k words; this is exactly kGeneralizedDefiniteEquation L k, which by Lambert Prop 58 (reverse direction in Equations.lean) gives L.IsGeneralizedDefinite k.

theorem Language.exists_isGeneralizedDefinite_iff_satisfies_pinGeneralizedDefiniteEquation {α : Type u_1} {L : Language α} [Finite L.syntacticMonoid] : (∃ (k : ℕ), L.IsGeneralizedDefinite k) ↔ L.pinGeneralizedDefiniteEquation

Pin's ℒℐ-theorem: a language is generalized-k-definite for some k iff its syntactic monoid satisfies Pin's LI omega-power equation.