Elementary embeddings commute with function symbols

Proved

MoritaEquiv.ElemEmb.map_funMap

by Alien60 · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

definabilitymany-sorted-logicmodel-theorymorita-equivalence

Let $L$ be a many-sorted signature and let $h : M \to N$ be an elementary embedding of $L$ -structures (a sortwise family of maps $h_s : M_s \to N_s$ preserving and reflecting the satisfaction of every formula). Then $h$ commutes with the interpretation of every function symbol: for each $f : s_0 \times \dots \times s_{m-1} \to s$ in $L$ and all $x_j \in M_{s_j}$ ,

h_s\big(f^M(x_0,\dots,x_{m-1})\big) = f^N\big(h_{s_0}(x_0),\dots,h_{s_{m-1}}(x_{m-1})\big).

Constants are the case $m = 0$ . This is the basic fact that elementary embeddings are in particular homomorphisms of the underlying many-sorted structures.

Preamble

import Mathlib
import Definitions.Def_MoritaEquiv_defs

open CategoryTheory

Formal statement

namespace MoritaEquiv

/-- Elementary embeddings commute with the interpretations of function symbols. -/
theorem ElemEmb.map_funMap {L : Sig} {M N : Str L} (h : ElemEmb M N) {m : ℕ} {dom : Fin m → L.Srt}
    {s : L.Srt} (f : L.Func m dom s) (xs : (j : Fin m) → M.carrier (dom j)) :
    h.toFun s (M.funMap f xs) = N.funMap f (fun j => h.toFun (dom j) (xs j)) := by sorry

end MoritaEquiv

Source

T. W. Barrett, H. Halvorson, Morita Equivalence, Rev. Symb. Logic 9 (2016) 556-582, https://arxiv.org/abs/1506.04675 (arXiv v1), §4.1 (explicit definitions of new sorts) and §5 (proof of Proposition 5.2)

View graph