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.toSyntacticMonoid (FreeMonoid.ofList 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?

@cite{lambert-2026} 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: IsDefinite k L → kDefiniteEquation L k is the finite-k half; (∃ k, IsDefinite k L) ↔ 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/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).

References

• @cite{pin-mfa}.
• @cite{eilenberg-1976}.
• @cite{almeida-1995}.
• @cite{perles-rabin-shamir-1963} (the original definite/reverse-definite/ generalized-definite hierarchy).
• @cite{mcnaughton-papert-1971} (variety theory of finite monoids).
• @cite{lambert-2026} §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

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

theorem Language.IsDefinite.satisfies_pinDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} [Finite L.syntacticMonoid] (hk : Core.Computability.Subregular.IsDefinite k L) : 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 : ℕ), Core.Computability.Subregular.IsDefinite k L

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 : ℕ), Core.Computability.Subregular.IsDefinite k L) ↔ 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 (@cite{lambert-2026} Prop 57 limit; @cite{almeida-1995}): ∀ 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

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

theorem Language.IsReverseDefinite.satisfies_pinReverseDefiniteEquation {α : Type u_1} {L : Language α} {k : ℕ} [Finite L.syntacticMonoid] (hk : Core.Computability.Subregular.IsReverseDefinite k L) : 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 : ℕ), Core.Computability.Subregular.IsReverseDefinite k L

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 : ℕ), Core.Computability.Subregular.IsReverseDefinite k L) ↔ 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 (@cite{lambert-2026} Prop 59; @cite{almeida-1995}): 𝒩 = ⟦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 : Core.Computability.Subregular.IsFiniteOrCofinite L) : 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/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) : Core.Computability.Subregular.IsFiniteOrCofinite L

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/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] : Core.Computability.Subregular.IsFiniteOrCofinite L ↔ 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 (@cite{lambert-2026} Prop 58 limit, simplified form; @cite{straubing-1985}): ℒℐ = ⟦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 : Core.Computability.Subregular.IsGeneralizedDefinite k L) : 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 IsGeneralizedDefinite k L 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 : ℕ), Core.Computability.Subregular.IsGeneralizedDefinite k L

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 IsGeneralizedDefinite k L.

theorem Language.exists_isGeneralizedDefinite_iff_satisfies_pinGeneralizedDefiniteEquation {α : Type u_1} {L : Language α} [Finite L.syntacticMonoid] : (∃ (k : ℕ), Core.Computability.Subregular.IsGeneralizedDefinite k L) ↔ 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.