Morleyization and fragment elementarity

For a fragment F, the Morleyization by its members F.toSet names every member of F by a predicate. A base embedding f : N ↪[L] M lifts to an embedding of the canonical expansions exactly when it is F-elementary (exists_morleyEmbedding_iff_aElementary): an embedding of expansions must preserve and reflect each new predicate, which is truth agreement on each member of F at every tuple of N, and conversely that agreement is precisely what the new predicates need. The lift, when it exists, is unique with the given underlying map (morleyEmbedding_unique).

This connects the definitional expansion to the fragment interface directly, without routing through back-and-forth ranks. Nothing here asserts quantifier elimination: named members become atomic, but an arbitrary expanded-language formula need not back-translate into F.

def FirstOrder.Language.IsMorleyLift {L : Language} (F : L.Fragment) {M N : Type w} [L.Structure M] [L.Structure N] (f : L.Embedding N M) (g : (L.morleyize F.toSet).Embedding N M) : Prop

An embedding of canonical expansions with a given underlying map.

Equations

• FirstOrder.Language.IsMorleyLift F f g = (⇑g = ⇑f)

theorem FirstOrder.Language.exists_morleyEmbedding_iff_aElementary {L : Language} (F : L.Fragment) {M N : Type w} [L.Structure M] [L.Structure N] (f : L.Embedding N M) : (∃ (g : (L.morleyize F.toSet).Embedding N M), IsMorleyLift F f g) ↔ AElementary F f

A base embedding lifts to the canonical expansions iff it is F-elementary.

theorem FirstOrder.Language.morleyEmbedding_unique {L : Language} (F : L.Fragment) {M N : Type w} [L.Structure M] [L.Structure N] (f : L.Embedding N M) {g g' : (L.morleyize F.toSet).Embedding N M} (hg : IsMorleyLift F f g) (hg' : IsMorleyLift F f g') : g = g'

The lift is unique with the given underlying map.