Morita extensions are conservative

Proved

MoritaEquiv.conservative

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 $\Sigma$ -formula $\alpha$ in context: $\alpha$ holds in all models of $T$ iff (its image) holds in all models of $T^+$ .

Preamble

import Mathlib
import Definitions.Def_MoritaEquiv_defs

open CategoryTheory

Formal statement

namespace MoritaEquiv

/-- Barrett–Halvorson, Theorem 4.2: a Morita extension `T⁺` of `T` is conservative:
`T ⊨ A` iff `T⁺ ⊨ A` for every `Σ`-axiom `A` (formula in context, read as its universal closure). -/
theorem conservative {L : Sig} {T : Theory L} (D : MoritaData L T) (A : Axiom L) :
    (∀ M : Model T, M.str.Satisfies A) ↔ ∀ N : Model D.ext, N.str.Satisfies (A.map D.incl) := 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.2

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 $\Sigma$ -formula $\alpha$ in any context: $\alpha$ holds under all assignments in every model of $T$ if and only if its image in $\Sigma^+$ holds under all assignments in every model of $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