The reduct functor Π is full

Proved

MoritaEquiv.proj_full

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. $\Pi$ is full: every elementary embedding $\Pi N\to\Pi N'$ is the restriction of an elementary embedding $N\to N'$ .

Preamble

import Mathlib
import Definitions.Def_MoritaEquiv_defs

open CategoryTheory

Formal statement

namespace MoritaEquiv

/-- Barrett–Halvorson, Proposition 5.3: for a Morita extension `T⁺` of `T`, the reduct functor
`Π : Mod(T⁺) ⥤ Mod(T)` is full: every elementary embedding `M|Σ → N|Σ` between reducts of
models of `T⁺` extends to an elementary embedding `M → N`. -/
theorem proj_full {L : Sig} {T : Theory L} (D : MoritaData L T) : D.proj.Full := 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, Proposition 5.3 (with Lemma 4.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). $\Pi$ is full: for models $N,N'$ of $T^+$ , every elementary embedding $g:\Pi N\to\Pi N'$ of $\Sigma$ -structures equals $\Pi h$ for some elementary embedding $h:N\to N'$ of $\Sigma^+$ -structures.

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