feat: add liftWithConstants and withConstantsStructure for embeddings

Author: NoneMore

Mathlib/ModelTheory/ElementaryMaps.lean

@@ -194,6 +194,20 @@ theorem comp_assoc (f : M ↪ₑ[L] N) (g : N ↪ₑ[L] P) (h : P ↪ₑ[L] Q) :
     (h.comp g).comp f = h.comp (g.comp f) :=
   rfl
 
+def liftWithConstants (f : M ↪ₑ[L] N) (A : Set M) :
+    @ElementaryEmbedding (L[[A]]) M N _ (f.toEmbedding.withConstantsStructure A) := by
+  letI : L[[A]].Structure N := f.toEmbedding.withConstantsStructure A
+  refine ⟨f,?_⟩
+  intro n φ x
+  simp only [Formula.Realize,
+← BoundedFormula.realize_constantsVarsEquiv]
+  have h: @Sum.elim (↑A) (Fin n) N (fun a ↦ ↑(L.con a)) (⇑f ∘ x) =
+    f ∘ @Sum.elim (↑A) (Fin n) M (fun a ↦ ↑(L.con a)) x := by
+    rw [Sum.comp_elim]
+    congr 1
+  have h': (default : Fin 0 → N) = f ∘ (default : Fin 0 → M) := List.ofFn_inj.mp rfl
+  simp only [h, coe_con, h', map_boundedFormula]
+
 end ElementaryEmbedding
 
 variable (L) (M)

Mathlib/ModelTheory/LanguageMap.lean

@@ -499,6 +499,35 @@ instance map_constants_inclusion_isExpansionOn :
     (L.lhomWithConstantsMap (Set.inclusion h)).IsExpansionOn M :=
   LHom.sumMap_isExpansionOn _ _ _
 
+variable {L} (A) {N : Type w'} [L.Structure N] (f : M ↪[L] N)
+
+def Embedding.withConstantsStructure : L[[A]].Structure N :=
+  letI : (constantsOn A).Structure N := constantsOn.structure fun a => f a
+  L.withConstantsStructure A
+
+def Embedding.liftWithConstants :
+    @Embedding (L[[A]]) M N _ (f.withConstantsStructure A) := by
+  letI : L[[A]].Structure N := f.withConstantsStructure A
+  refine ⟨f.toEmbedding,?_,?_⟩
+  · intro n g x
+    cases g with
+    | inl g =>
+      simp only [withConstants_funMap_sumInl]
+      exact f.map_fun' g x
+    | inr c =>
+      cases n with
+      | succ n => exact isEmptyElim c
+      | zero =>
+        simp only [withConstants_funMap_sumInr, constantMap]
+        rfl
+  · intro n R x
+    cases R with
+    | inl R =>
+      simp only [withConstants_relMap_sumInl]
+      exact f.map_rel' R x
+    | inr r =>
+      exact isEmptyElim r
+
 end WithConstants
 
 end Language