The power $\Sigma$ -algebra $A^{\wp}$

Definition

MSKleene_Power

by Cosme · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

formal-languagesmany-sorted-algebratree-automatauniversal-algebra

The power (subset) $\Sigma$ -algebra $A^{\wp}$ associated with a many-sorted $\Sigma$ -algebra $A$ (Proposition 2.32; for single-sorted algebras, Mezei–Wright 1967).

Its carrier is the sortwise powerset $s \mapsto \mathrm{Set}(A_s)$ . For an operation symbol $\sigma$ of rank $(\mathbf{s},s)$ and a tuple of subsets $(L_i)_i$ , the interpreted operation returns the image

\sigma^{A^{\wp}}((L_i)_i) = \{\, \sigma^{A}((x_i)_i) \mid x_i \in L_i \text{ for every } i \,\}.

The predicate Args.pmem expresses that an argument tuple is a componentwise member of a tuple of subsets, and powerOp packages the image above. The singleton $S$ -sorted map $\{\cdot\}^{\Sigma}_A : A \to A^{\wp}$ , $x \mapsto \{x\}$ , is also defined.

This object is where regular expressions are interpreted as languages.

Definition code

/-
The power (subset) `Σ`-algebra `A^℘` associated with a many-sorted `Σ`-algebra
`A` (Proposition 2.32; for single-sorted algebras, Mezei–Wright 1967, Def. 2.2).

Carrier: sortwise powerset `s ↦ Set (A_s)`.
Operation `σ^{A^℘}`: sends a tuple of subsets `(L_i)` to the image
`{ σ^A(x_i) | x_i ∈ L_i for every i }`.

Also: the singleton map `{·} : A → A^℘`, `x ↦ {x}`, as an `S`-sorted map.
-/
import Definitions.Def_MSKleene_Core

namespace MSKleene

universe u

variable {S : Type u} {sig : Signature S}

/-- `Args.pmem xs Ls` holds when the argument tuple `xs` is a componentwise
member of the tuple of subsets `Ls`. -/
def Args.pmem {A : SSet S} :
    {w : List S} → Args A w → Args (fun s => Set (A s)) w → Prop
  | [], _, _ => True
  | _ :: _, (x, xs), (L, Ls) => x ∈ L ∧ Args.pmem xs Ls

/-- The image of a tuple of subsets under an operation of the algebra `A`:
`{ A.op σ xs | xs a componentwise member of Ls }`. -/
def powerOp (A : Algebra sig) {w : List S} {s : S} (σ : sig w s)
    (Ls : Args (fun s => Set (A.carrier s)) w) : Set (A.carrier s) :=
  { y | ∃ xs : Args A.carrier w, Args.pmem xs Ls ∧ y = A.op σ xs }

/-- The power `Σ`-algebra `A^℘` (Proposition 2.32). -/
def powerAlgebra (A : Algebra sig) : Algebra sig where
  carrier := fun s => Set (A.carrier s)
  op := fun σ Ls => powerOp A σ Ls

@[simp] theorem powerAlgebra_carrier (A : Algebra sig) (s : S) :
    (powerAlgebra A).carrier s = Set (A.carrier s) := rfl

@[simp] theorem powerAlgebra_op (A : Algebra sig) {w : List S} {s : S}
    (σ : sig w s) (Ls : Args (fun s => Set (A.carrier s)) w) :
    (powerAlgebra A).op σ Ls = powerOp A σ Ls := rfl

/-- The singleton `S`-sorted map `{·}^Σ_A : A → A^℘`. -/
def singletonMap (A : Algebra sig) : SMap A.carrier (powerAlgebra A).carrier :=
  fun s a => ({a} : Set (A.carrier s))

theorem singletonMap_apply (A : Algebra sig) (s : S) (a : A.carrier s) :
    singletonMap A s a = ({a} : Set (A.carrier s)) := rfl

end MSKleene

Source

Gong, Ruiz Mora, Sanmartín Vich, Cosme Llópez, "A Kleene theorem for free many-sorted algebras", 2026, https://arxiv.org/abs/1808.08217 (predecessor CVCL20)

Read-back

What the Lean code literally says, in plain math · claude-sonnet-5

Args.pmem

This definition introduces a predicate ("positional membership"). Fix an arbitrary type $S$ whose elements are called sorts, and an implicit family $A : S \to \mathrm{Type}$ assigning a type $A_s$ to each sort $s$ . For a list of sorts $w = [s_1, \dots, s_k]$ (implicit), $\mathrm{Args}(A, w)$ denotes the iterated product $A_{s_1} \times \cdots \times A_{s_k}$ (a one‑element type when $w$ is empty), and $\mathrm{Args}(s \mapsto \mathrm{Set}(A_s), w)$ denotes the product $\mathrm{Set}(A_{s_1}) \times \cdots \times \mathrm{Set}(A_{s_k})$ whose $i$ ‑th entry is a subset of $A_{s_i}$ . Given a tuple $xs \in \mathrm{Args}(A, w)$ and a tuple of subsets $Ls \in \mathrm{Args}(s \mapsto \mathrm{Set}(A_s), w)$ , the proposition $\mathrm{pmem}(xs, Ls)$ is defined by recursion on $w$ :

when $w$ is the empty list, $\mathrm{pmem}(xs, Ls) = \mathrm{True}$ — it holds unconditionally, and both tuples are the trivial one‑element tuple;
when $w = s :: w'$ , writing $xs = (x, xs')$ with $x \in A_s$ and $Ls = (L, Ls')$ with $L \subseteq A_s$ , we have $\mathrm{pmem}(xs, Ls) = (x \in L) \ \wedge\ \mathrm{pmem}(xs', Ls')$ .

Thus $\mathrm{pmem}(xs, Ls)$ asserts that every component of the tuple $xs$ lies in the correspondingly positioned subset of $Ls$ ; for the empty arity it is vacuously true.

powerOp

Fix a sort type $S$ and an implicit signature $\mathrm{sig}$ over $S$ , where a signature assigns to each arity list $w \in \mathrm{List}(S)$ and result sort $s \in S$ a type $\mathrm{sig}(w,s)$ of operation symbols. Let $A$ be an algebra for $\mathrm{sig}$ : it provides a carrier family $s \mapsto A.\mathrm{carrier}_s$ and, for each operation symbol $\sigma \in \mathrm{sig}(w,s)$ , an interpretation $A.\mathrm{op}(\sigma, -) : \mathrm{Args}(A.\mathrm{carrier}, w) \to A.\mathrm{carrier}_s$ . Given an implicit arity $w$ and result sort $s$ , an operation symbol $\sigma \in \mathrm{sig}(w,s)$ , and a tuple $Ls$ whose $i$ ‑th entry is a subset $L_i \subseteq A.\mathrm{carrier}_{w_i}$ , the definition sets

\mathrm{powerOp}(A, \sigma, Ls) \;=\; \{\, y \;\mid\; \exists\, xs \in \mathrm{Args}(A.\mathrm{carrier}, w),\ \ \mathrm{pmem}(xs, Ls) \ \wedge\ y = A.\mathrm{op}(\sigma, xs) \,\}

as a subset of $A.\mathrm{carrier}_s$ . In words, it is the set of all values obtained by applying the operation $\sigma$ of $A$ to some argument tuple $xs$ each of whose components lies in the corresponding subset listed by $Ls$ . When $w$ is the empty list, there are no components, $\mathrm{pmem}$ holds trivially, and this reduces to the singleton $\{\,A.\mathrm{op}(\sigma, \ast)\,\}$ containing the interpreted constant, with $Ls$ the trivial empty tuple.

powerAlgebra

With $S$ and $\mathrm{sig}$ as above and $A$ an algebra for $\mathrm{sig}$ , this defines a new algebra $\mathrm{powerAlgebra}(A)$ for the same signature $\mathrm{sig}$ . Its carrier at each sort $s$ is $\mathrm{Set}(A.\mathrm{carrier}_s)$ , the type of all subsets of $A$ 's carrier at $s$ . Its interpretation of an operation symbol $\sigma$ applied to a tuple of subsets $Ls$ is $\mathrm{powerOp}(A, \sigma, Ls)$ , the set described in the previous paragraph.

powerAlgebra_carrier

This theorem is marked as a simplification lemma. It states that for every algebra $A$ for $\mathrm{sig}$ and every sort $s \in S$ , the carrier of the algebra $\mathrm{powerAlgebra}(A)$ at sort $s$ is equal, as a type, to $\mathrm{Set}(A.\mathrm{carrier}_s)$ . The proof is by reflexivity, i.e. the two sides are definitionally equal.

powerAlgebra_op

This theorem is marked as a simplification lemma. It states that for every algebra $A$ for $\mathrm{sig}$ , every implicit arity $w$ and result sort $s$ , every operation symbol $\sigma \in \mathrm{sig}(w,s)$ , and every tuple $Ls$ whose $i$ ‑th component is a subset of $A.\mathrm{carrier}_{w_i}$ , the interpretation of $\sigma$ in the algebra $\mathrm{powerAlgebra}(A)$ applied to $Ls$ equals $\mathrm{powerOp}(A, \sigma, Ls)$ . The proof is by reflexivity.

singletonMap

With $S$ , $\mathrm{sig}$ , and an algebra $A$ for $\mathrm{sig}$ , this defines $\mathrm{singletonMap}(A)$ as a sorted map from the carrier of $A$ to the carrier of $\mathrm{powerAlgebra}(A)$ ; that is, a family of functions indexed by sorts, where at sort $s$ it is a function $A.\mathrm{carrier}_s \to \mathrm{Set}(A.\mathrm{carrier}_s)$ . Concretely, at sort $s$ it sends an element $a$ to the singleton subset $\{a\}$ of $A.\mathrm{carrier}_s$ . It is asserted only to be such a sorted map; there is no claim that it is a homomorphism of algebras.

singletonMap_apply

This theorem (not marked as a simplification lemma) states that for every algebra $A$ for $\mathrm{sig}$ , every sort $s \in S$ , and every element $a \in A.\mathrm{carrier}_s$ , the value of $\mathrm{singletonMap}(A)$ at sort $s$ on the argument $a$ is the singleton set $\{a\} \subseteq A.\mathrm{carrier}_s$ . The proof is by reflexivity.

Human review

Endorsed by Shuze Chen · Sep 9, 2026
Endorsed by Cosme · Sep 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The power Σ\SigmaΣ-algebra A℘A^{\wp}A℘

The power $\Sigma$ -algebra $A^{\wp}$