Morita equivalence implies categorical equivalence

Proved

MoritaEquiv.morita_imp_categorical

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

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

If two many-sorted first-order theories $T_1,T_2$ are Morita equivalent (finite chains of Morita extensions ending in logically equivalent theories over a common signature, up to renaming), then $\mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2)$ , with elementary embeddings as arrows.

Preamble

import Mathlib
import Definitions.Def_MoritaEquiv_defs

open CategoryTheory

Formal statement

namespace MoritaEquiv

/-- Barrett–Halvorson, Theorem 5.1: Morita equivalence entails categorical equivalence,
i.e. Morita equivalent theories have equivalent categories of models
(arrows: elementary embeddings). -/
theorem morita_imp_categorical {L₁ L₂ : Sig} (T₁ : Theory L₁) (T₂ : Theory L₂)
    (h : MoritaEquivalent T₁ T₂) : CategoricallyEquivalent T₁ T₂ := 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), §5, Theorem 5.1

Read-back

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

For all signatures $\Sigma_1,\Sigma_2$ and theories $T_1,T_2$ over them: if $T_1$ and $T_2$ are Morita equivalent (there are finite chains of Morita extensions $T_1\rightsquigarrow T_1'$ , $T_2\rightsquigarrow T_2'$ and a signature map $F$ from the signature of $T_1'$ to that of $T_2'$ , bijective on sorts and on symbols of each profile, such that a structure is a model of $T_2'$ iff its $F$ -reduct is a model of $T_1'$ ), then $\mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2)$ as categories, where objects are models with nonempty carriers in every sort and arrows are elementary embeddings.

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