Lemma 3.23: substitution homomorphism as family substitution

Proved

MSKleene.subst_family

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

formal-languagesmany-sorted-algebratree-automatauniversal-algebra

Substitution homomorphism as family substitution (Lemma 3.23).

Let $u,s\in S$ , $z\in X_{u}$ , $L\subseteq\mathrm{T}_{\Sigma}(X)_{u}$ , $P\in\mathrm{T}_{\Sigma}(X)_{s}$ . Then $\left(\!\begin{smallmatrix}z\\L\end{smallmatrix}\!\right)^{\sharp}_{s}(P)=\left\{\left(\!\begin{smallmatrix}z\\(Q^{z}_{\alpha})_{\alpha\in|P|_{z}}\end{smallmatrix}\!\right)(P)\ \middle|\ (Q^{z}_{\alpha})\in L^{|P|_{z}}\right\}$ . Consequently, for every $K\subseteq\mathrm{T}_{\Sigma}(X)_{s}$ , $\left(\!\begin{smallmatrix}z\\L\end{smallmatrix}\!\right)^{\sharp\mathsf{p}}_{s}(K)=\bigcup_{P\in K}\left(\!\begin{smallmatrix}z\\L\end{smallmatrix}\!\right)^{\sharp}_{s}(P)$ .

Preamble

import Definitions.Def_MSKleene_Subst
import Definitions.Def_MSKleene_SubstFam

Formal statement

import Definitions.Def_MSKleene_Subst
import Definitions.Def_MSKleene_SubstFam

namespace MSKleene

/-- **The substitution homomorphism as family substitution** (Lemma 3.23).

For `z ∈ X_u`, a language `L ⊆ T_Σ(X)_u`, and a term `P ∈ T_Σ(X)_s`,
`⟨z/L⟩^♯_s(P)` is the set of all `⟨z/qs⟩(P)` where `qs` ranges over families of
terms of `L` indexed by the occurrences of `z` in `P`. Consequently, its
completely additive extension on a language `K` is the union of these values
over the terms in `K`. -/
theorem subst_family {S : Type} (sig : Signature S) (X : SSet S) {u s : S}
    (z : X u) (L : Set (Term sig X u)) (P : Term sig X s) :
    ((substHom z L).toFun s P
      = { R | ∃ qs : Fin (Term.occ z P) → Term sig X u,
              (∀ α, qs α ∈ L) ∧ R = substFam z P qs })
  ∧ (∀ K : Set (Term sig X s),
      substP z L s K = ⋃ Q ∈ K, (substHom z L).toFun s Q) := by
  sorry

end MSKleene

Source

Gong, Ruiz Mora, Sanmartín Vich, Cosme Llópez, "A Kleene theorem for free many-sorted algebras", 2026

Read-back

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

For every type $S$ of sorts, every $S$ -sorted signature $\Sigma$ (assigning a type of operation symbols to each finite input-sort list and output sort), every family $X=(X_t)_{t\in S}$ of variable types, all sorts $u,s\in S$ , every variable $z\in X_u$ , every set $L\subseteq T_\Sigma(X)_u$ , and every term $P\in T_\Sigma(X)_s$ , the following two assertions hold simultaneously. Let $H_{z,L}$ be the recursively induced set-valued evaluation of terms that sends $z$ to $L$ , sends every other variable $y$ to the singleton containing its variable term, and sends an operation application $\sigma(P_1,\ldots,P_n)$ to the set of all $\sigma(R_1,\ldots,R_n)$ obtained by independently choosing $R_i\in H_{z,L}(P_i)$ . First, writing $\operatorname{occ}_z(P)$ for the number of occurrences of $z$ in $P$ —variables contribute $1$ exactly when they are $z$ , and operation applications sum the counts of their arguments—the theorem asserts

H_{z,L}(P) = \left\{ R\in T_\Sigma(X)_s\ \middle|\ \begin{array}{l} \text{there exists }q:\{0,\ldots,\operatorname{occ}_z(P)-1\}\to T_\Sigma(X)_u\\ \text{such that }q_\alpha\in L\text{ for every }\alpha,\text{ and }R \text{ is obtained from }P\\ \text{by replacing its successive occurrences of }z,\text{ traversed left-to-right}\\ \text{through operation arguments, by }q_0,q_1,\ldots \end{array} \right\}.

Second, for every set $K\subseteq T_\Sigma(X)_s$ , the operator $\operatorname{substP}_{z,L,s}$ , defined by taking the union of this set-valued evaluation over the input set, satisfies

\operatorname{substP}_{z,L,s}(K) = \bigcup_{Q\in K}H_{z,L}(Q),

so equivalently a term belongs to this set exactly when it belongs to $H_{z,L}(Q)$ for some $Q\in K$ . No finiteness, decidable-equality, or nonemptiness assumptions are imposed on $S$ , $\Sigma$ , $X$ , $L$ , or $K$ beyond the displayed elements and terms existing. In particular, if $P$ has no occurrence of $z$ , the indexing type is empty and the universal membership condition is vacuous, giving the singleton $\{P\}$ on the right of the first equality even when $L=\varnothing$ ; if $P$ has at least one occurrence of $z$ and $L=\varnothing$ , that right-hand side is empty; and $K=\varnothing$ makes the second union empty.

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