Elementary Extensions

Stream: mathlib4

[Yongxi Lin (Aaron)]

Given a language L and an L.Structure M, what is the best way to state in lean that M has an elementary extension N? Here's my attempt:

import Mathlib

open FirstOrder Language Structure

variable {L : Language} {M : Type*} [L.Structure M]

example : ∃ (N : Type*) (hN : L.Structure N) (S : L.ElementarySubstructure N), Nonempty (S ≃[L] M) := by sorry

This seems very uncanonical but this is the best I can do because the type of M is not set N, and L.ElementarySubstructure N is defined by using set N.

[Aaron Anderson]

You want to show that there is some N with an L.Structure N instance and an L.ElementaryEmbedding M N such that whatever other properties are satisfied by that elementary embedding.

[Aaron Anderson]

This is mathematically equivalent to there existing a substructure of N that is isomorphic to M, but is the version I would work with.