Recognizable and $s$-recognizable languages

Algebra.Finite

This declaration is parametrized implicitly by a universe level, a type $S$ whose elements are called sorts, and a signature $\mathrm{sig}$ over $S$ (a signature assigns to each pair consisting of a list $w$ of sorts and a single sort $s$ a type $\mathrm{sig}\,w\,s$, whose elements are the operation symbols of input arity $w$ and output sort $s$). Given an algebra $B$ for $\mathrm{sig}$ — a structure providing a carrier family $s \mapsto B_s$ that assigns a type to every sort, together with an interpretation of each operation symbol as a function from tuples of carrier elements (of the sorts listed in $w$) to $B_s$ — the definition Algebra.Finite B is the proposition that the dependent sum (total space) $\Sigma_{s : S}\, B_s$, whose elements are the pairs $(s, x)$ with $s : S$ a sort and $x$ an element of $B_s$, is a finite type in the sense of Mathlib's Finite predicate (i.e. it admits a bijection with $\{0, 1, \dots, n-1\}$ for some natural number $n$). This is a single finiteness condition on the disjoint union of all carriers taken together; it does not by itself assert that $S$ is finite, nor that each individual $B_s$ is finite, and it holds, for example, whenever every $B_s$ is empty, irrespective of the cardinality of $S$.

IsRecognizable

Parametrized implicitly by a universe level, a sort type $S$, and a signature $\mathrm{sig}$ on $S$. Its inputs are an algebra $A$ for $\mathrm{sig}$ (a carrier family $s \mapsto A_s$ together with operation interpretations) and a family $L$ assigning to each sort $s$ a subset $L_s \subseteq A_s$. The proposition IsRecognizable A L asserts that there exists an algebra $B$ for $\mathrm{sig}$ such that:

1. the total space $\Sigma_{s : S}\, B_s$ (pairs $(s, x)$ with $x \in B_s$) is a finite type in Mathlib's Finite sense; and
2. there exist a homomorphism $f : A \to B$ and a family $M$ assigning to each sort $s$ a subset $M_s \subseteq B_s$, such that for every sort $s$ the preimage

$$f_s^{-1}(M_s) \;=\; \{\, a \in A_s \mid f_s(a) \in M_s \,\}$$

is equal, as a subset of $A_s$, to $L_s$.

Here a homomorphism $f : A \to B$ consists of a family of maps $f_s : A_s \to B_s$ (one per sort) together with a proof that for every operation symbol $\sigma \in \mathrm{sig}\,w\,s$ and every argument tuple $\mathrm{args}$ of sorts $w$, $f_s\big(A.\mathrm{op}\,\sigma\,\mathrm{args}\big) = B.\mathrm{op}\,\sigma\,\big(f \text{ applied componentwise to } \mathrm{args}\big)$. No surjectivity of $f$ is required, and $M$ is an arbitrary family of subsets of the carriers of $B$ (no closure or saturation condition). The equality in clause 2 is required at every sort simultaneously, using the same $B$, $f$, and $M$; if $S$ is empty this universal condition over sorts is vacuous, so the statement then reduces to the mere existence of a finite algebra $B$ with a homomorphism $A \to B$.

sRecognizable

Parametrized implicitly by a universe level, a sort type $S$, and a signature $\mathrm{sig}$ on $S$. Its inputs are an algebra $A$ for $\mathrm{sig}$, one fixed sort $s : S$, and a single subset $L \subseteq A_s$ of the carrier of $A$ at that sort (not a family over all sorts). The proposition sRecognizable A s L asserts that there exists an algebra $B$ for $\mathrm{sig}$ such that:

1. the total space $\Sigma_{t : S}\, B_t$ is a finite type in Mathlib's Finite sense; and
2. there exist a homomorphism $f : A \to B$ and a single subset $M \subseteq B_s$ (at the same fixed sort $s$) such that

$$f_s^{-1}(M) \;=\; \{\, a \in A_s \mid f_s(a) \in M \,\} \;=\; L,$$

an equality of subsets of $A_s$.

The homomorphism $f : A \to B$ is a full homomorphism (a map $f_t : A_t \to B_t$ for every sort $t$, satisfying the operation-compatibility condition for every operation symbol), but only its component $f_s$ at the single sort $s$ is constrained by clause 2; the behaviour of $f$ and the choice of subsets at all other sorts are otherwise unconstrained. No surjectivity of $f$ is required.

Recognizable

Parametrized implicitly by a universe level, a sort type $S$, and a signature $\mathrm{sig}$ on $S$. Given an algebra $A$ for $\mathrm{sig}$, Recognizable A is defined to be the set of all families $L$ — where a family assigns to each sort $s$ a subset $L_s \subseteq A_s$ — such that IsRecognizable A L holds; that is, $\{\, L \mid \text{there exists a finite algebra } B, \text{ a homomorphism } f : A \to B, \text{ and a family of subsets } M \text{ of } B \text{ with } f_s^{-1}(M_s) = L_s \text{ for every sort } s \,\}$. The ambient type is the collection of all such sort-indexed families of subsets of $A$'s carriers, and Recognizable A is the sub-collection of those that satisfy the recognizability condition spelled out under IsRecognizable.

RecS

Parametrized implicitly by a universe level, a sort type $S$, and a signature $\mathrm{sig}$ on $S$. Given an algebra $A$ for $\mathrm{sig}$ and one fixed sort $s : S$, RecS A s is defined to be the set of all subsets $L \subseteq A_s$ such that sRecognizable A s L holds; that is, $\{\, L \mid \text{there exists a finite algebra } B, \text{ a homomorphism } f : A \to B, \text{ and a subset } M \subseteq B_s \text{ with } f_s^{-1}(M) = L \,\}$. The ambient type is the collection of all subsets of the carrier $A_s$, and RecS A s is the sub-collection of those subsets that are recognizable at the single sort $s$ in the sense spelled out under sRecognizable.