The reduct functor Π is faithful

Proved

MoritaEquiv.proj_faithful

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 faithful: an elementary embedding of models of $T^+$ is determined by its restriction to the old sorts.

Preamble

import Mathlib
import Definitions.Def_MoritaEquiv_defs

open CategoryTheory

Formal statement

namespace MoritaEquiv

/-- Barrett–Halvorson, Proposition 5.2: for a Morita extension `T⁺` of `T`, the reduct functor
`Π : Mod(T⁺) ⥤ Mod(T)` is faithful. -/
theorem proj_faithful {L : Sig} {T : Theory L} (D : MoritaData L T) : D.proj.Faithful := 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.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). $\Pi$ is faithful: for models $N,N'$ of $T^+$ and elementary embeddings $h,h':N\to N'$ , if $h$ and $h'$ agree on every old sort then $h=h'$ .

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