Every model of T expands uniquely to a model of T⁺

Proved

MoritaEquiv.expansion_exists_unique

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

category-theorydefinabilitymany-sorted-logicmodel-theorymorita-equivalencephilosophy-of-sciencetheoretical-equivalence

Throughout: many-sorted first-order logic with nonempty sorts; $\mathrm{Mod}(T)$ has the models of $T$ as objects and elementary embeddings as arrows; $D$ is a Morita extension of the $\Sigma$ -theory $T$ (new product, coproduct, subsort and quotient sorts and explicitly defined symbols, with admissibility in every model of $T$ ), $T^+$ the extended theory and $\Pi:\mathrm{Mod}(T^+)\to\mathrm{Mod}(T)$ the reduct functor. For every $M\in\mathrm{Mod}(T)$ there is $N\in\mathrm{Mod}(T^+)$ with $\Pi N\cong M$ , and any two $N,N'$ with $\Pi N\cong M\cong\Pi N'$ are isomorphic in $\mathrm{Mod}(T^+)$ .

Preamble

import Mathlib
import Definitions.Def_MoritaEquiv_defs

open CategoryTheory

Formal statement

namespace MoritaEquiv

/-- Barrett–Halvorson, Theorem 4.1 (with Proposition 5.1): if `T⁺` is a Morita extension of `T`,
every model `M` of `T` has an expansion that is a model of `T⁺` (a model `N` of `T⁺` whose reduct
`Π N = N|Σ` is isomorphic to `M`), and this expansion is unique up to isomorphism. -/
theorem expansion_exists_unique {L : Sig} {T : Theory L} (D : MoritaData L T) (M : Model T) :
    (∃ N : Model D.ext, Nonempty (D.proj.obj N ≅ M)) ∧
      ∀ N N' : Model D.ext, (D.proj.obj N ≅ M) → (D.proj.obj N' ≅ M) → Nonempty (N ≅ N') := 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 (numbering as in arXiv v1), §4.2, Theorem 4.1 (with Prop. 5.1)

Read-back

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

Let $\Sigma$ be a signature, $T$ a $\Sigma$ -theory, $D$ a Morita extension datum over $T$ with extended signature $\Sigma^+$ , extended theory $T^+$ and reduct functor $\Pi:\mathrm{Mod}(T^+)\to\mathrm{Mod}(T)$ (sorts nonempty; arrows are elementary embeddings). For every model $M$ of $T$ : (a) there is a model $N$ of $T^+$ with an isomorphism $\Pi N\cong M$ in $\mathrm{Mod}(T)$ ; (b) for all models $N,N'$ of $T^+$ , if $\Pi N\cong M$ and $\Pi N'\cong M$ then $N\cong N'$ in $\mathrm{Mod}(T^+)$ .

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Alien60 · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph