feat(model_theory/basic.lean): Elementary embeddings and elementary s…

…ubstructures (#11089)

Defines elementary embeddings between structures
Defines when substructures are elementary
Provides lemmas about preservation of realizations of terms and formulas under various maps

src/model_theory/basic.lean

@@ -27,6 +27,8 @@ This file defines first-order languages and structures in the style of the
 * A `first_order.language.embedding`, denoted `M ↪[L] N`, is an embedding from the `L`-structure `M`
   to the `L`-structure `N` that commutes with the interpretations of functions, and which preserves
   the interpretations of relations in both directions.
+* A `first_order.language.elementary_embedding`, denoted `M ↪ₑ[L] N`, is an embedding from the
+  `L`-structure `M` to the `L`-structure `N` that commutes with the realizations of all formulas.
 * A `first_order.language.equiv`, denoted `M ≃[L] N`, is an equivalence from the `L`-structure `M`
   to the `L`-structure `N` that commutes with the interpretations of functions, and which preserves
   the interpretations of relations in both directions.
@@ -105,7 +107,7 @@ open first_order.language.Structure
 /-- A homomorphism between first-order structures is a function that commutes with the
   interpretations of functions and maps tuples in one structure where a given relation is true to
   tuples in the second structure where that relation is still true. -/
-protected structure hom :=
+structure hom :=
 (to_fun : M → N)
 (map_fun' : ∀{n} (f : L.functions n) x, to_fun (fun_map f x) = fun_map f (to_fun ∘ x) . obviously)
 (map_rel' : ∀{n} (r : L.relations n) x, rel_map r x → rel_map r (to_fun ∘ x) . obviously)
@@ -114,15 +116,15 @@ localized "notation A ` →[`:25 L `] ` B := L.hom A B" in first_order
 
 /-- An embedding of first-order structures is an embedding that commutes with the
   interpretations of functions and relations. -/
-protected structure embedding extends M ↪ N :=
+structure embedding extends M ↪ N :=
 (map_fun' : ∀{n} (f : L.functions n) x, to_fun (fun_map f x) = fun_map f (to_fun ∘ x) . obviously)
 (map_rel' : ∀{n} (r : L.relations n) x, rel_map r (to_fun ∘ x) ↔ rel_map r x . obviously)
 
 localized "notation A ` ↪[`:25 L `] ` B := L.embedding A B" in first_order
 
 /-- An equivalence of first-order structures is an equivalence that commutes with the
   interpretations of functions and relations. -/
-protected structure equiv extends M ≃ N :=
+structure equiv extends M ≃ N :=
 (map_fun' : ∀{n} (f : L.functions n) x, to_fun (fun_map f x) = fun_map f (to_fun ∘ x) . obviously)
 (map_rel' : ∀{n} (r : L.relations n) x, rel_map r (to_fun ∘ x) ↔ rel_map r x . obviously)
 
@@ -138,7 +140,7 @@ lemma fun_map_eq_coe_const {c : L.const} {x : fin 0 → M} :
 
 namespace hom
 
-@[simps] instance has_coe_to_fun : has_coe_to_fun (M →[L] N) (λ _, M → N) := ⟨to_fun⟩
+instance has_coe_to_fun : has_coe_to_fun (M →[L] N) (λ _, M → N) := ⟨to_fun⟩
 
 @[simp] lemma to_fun_eq_coe {f : M →[L] N} : f.to_fun = (f : M → N) := rfl
 
@@ -189,7 +191,7 @@ end hom
 
 namespace embedding
 
-@[simps] instance has_coe_to_fun : has_coe_to_fun (M ↪[L] N) (λ _, M → N) := ⟨λ f, f.to_fun⟩
+instance has_coe_to_fun : has_coe_to_fun (M ↪[L] N) (λ _, M → N) := ⟨λ f, f.to_fun⟩
 
 @[simp] lemma map_fun (φ : M ↪[L] N) {n : ℕ} (f : L.functions n) (x : fin n → M) :
   φ (fun_map f x) = fun_map f (φ ∘ x) := φ.map_fun' f x
@@ -282,7 +284,13 @@ namespace equiv
   end,
   .. f.to_equiv.symm }
 
-@[simps] instance has_coe_to_fun : has_coe_to_fun (M ≃[L] N) (λ _, M → N) := ⟨λ f, f.to_fun⟩
+instance has_coe_to_fun : has_coe_to_fun (M ≃[L] N) (λ _, M → N) := ⟨λ f, f.to_fun⟩
+
+@[simp]
+lemma apply_symm_apply (f : M ≃[L] N) (a : N) : f (f.symm a) = a := f.to_equiv.apply_symm_apply a
+
+@[simp]
+lemma symm_apply_apply (f : M ≃[L] N) (a : M) : f.symm (f a) = a := f.to_equiv.symm_apply_apply a
 
 @[simp] lemma map_fun (φ : M ≃[L] N) {n : ℕ} (f : L.functions n) (x : fin n → M) :
   φ (fun_map f x) = fun_map f (φ ∘ x) := φ.map_fun' f x
@@ -298,7 +306,7 @@ def to_embedding (f : M ≃[L] N) : M ↪[L] N :=
 { to_fun := f,
   inj' := f.to_equiv.injective }
 
-/-- A first-order equivalence is also a first-order embedding. -/
+/-- A first-order equivalence is also a first-order homomorphism. -/
 def to_hom (f : M ≃[L] N) : M →[L] N :=
 { to_fun := f }
 
@@ -774,6 +782,15 @@ def subtype (S : L.substructure M) : S ↪[L] M :=
 
 @[simp] theorem coe_subtype : ⇑S.subtype = coe := rfl
 
+/-- The equivalence between the maximal substructure of a structure and the structure itself. -/
+def top_equiv : (⊤ : L.substructure M) ≃[L] M  :=
+{ to_fun := subtype ⊤,
+  inv_fun := λ m, ⟨m, mem_top m⟩,
+  left_inv := λ m, by simp,
+  right_inv := λ m, rfl }
+
+@[simp] lemma coe_top_equiv : ⇑(top_equiv : (⊤ : L.substructure M) ≃[L] M) = coe := rfl
+
 /-- A dependent version of `substructure.closure_induction`. -/
 @[elab_as_eliminator] lemma closure_induction' (s : set M) {p : Π x, x ∈ closure L s → Prop}
   (Hs : ∀ x (h : x ∈ s), p x (subset_closure h))
@@ -825,6 +842,11 @@ export term
 
 variable {L}
 
+/-- Relabels a term's variables along a particular function. -/
+@[simp] def term.relabel {α β : Type} (g : α → β) : L.term α → L.term β
+| (var i) := var (g i)
+| (func f ts) := func f (λ i, (ts i).relabel)
+
 instance {α : Type} [inhabited α] : inhabited (L.term α) :=
 ⟨var default⟩
 
@@ -837,6 +859,41 @@ instance {α} : has_coe L.const (L.term α) :=
 | (var k)         := v k
 | (func f ts)     := fun_map f (λ i, realize_term (ts i))
 
+@[simp] lemma realize_term_relabel {α β : Type} (g : α → β) (v : β → M) (t : L.term α) :
+  realize_term v (t.relabel g) = realize_term (v ∘ g) t :=
+begin
+  induction t with _ n f ts ih,
+  { refl, },
+  { simp [ih] }
+end
+
+@[simp] lemma hom.realize_term {α : Type} (v : α → M)
+  (t : L.term α) (g : M →[L] N) :
+  realize_term (g ∘ v) t = g (realize_term v t) :=
+begin
+  induction t,
+  { refl },
+  { rw [realize_term, realize_term, g.map_fun],
+    refine congr rfl _,
+    ext x,
+    simp [t_ih x], },
+end
+
+@[simp] lemma embedding.realize_term {α : Type}  (v : α → M)
+  (t : L.term α) (g : M ↪[L] N) :
+  realize_term (g ∘ v) t = g (realize_term v t) :=
+g.to_hom.realize_term v t
+
+@[simp] lemma equiv.realize_term {α : Type}  (v : α → M)
+  (t : L.term α) (g : M ≃[L] N) :
+  realize_term (g ∘ v) t = g (realize_term v t) :=
+g.to_hom.realize_term v t
+
+@[simp] lemma realize_term_substructure {α : Type} {S : L.substructure M} (v : α → S)
+  (t : L.term α) :
+  realize_term (coe ∘ v) t = (↑(realize_term v t) : M) :=
+S.subtype.realize_term v t
+
 variable (L)
 /-- `bounded_formula α n` is the type of formulas with free variables indexed by `α` and up to `n`
   additional free variables. -/
@@ -878,6 +935,27 @@ variable {n : ℕ}
 
 @[simps] instance : has_sup (L.bounded_formula α n) := ⟨λ f g, bd_imp (bd_not f) g⟩
 
+/-- Relabels a bounded formula's variables along a particular function. -/
+@[simp] def bounded_formula.relabel {α β : Type} (g : α → β) :
+  ∀ {n : ℕ}, L.bounded_formula α n → L.bounded_formula β n
+| n bd_falsum := bd_falsum
+| n (bd_equal t₁ t₂) := bd_equal (t₁.relabel (sum.elim (sum.inl ∘ g) sum.inr))
+    (t₂.relabel (sum.elim (sum.inl ∘ g) sum.inr))
+| n (bd_rel R ts) := bd_rel R ((term.relabel (sum.elim (sum.inl ∘ g) sum.inr)) ∘ ts)
+| n (bd_imp f₁ f₂) := bd_imp f₁.relabel f₂.relabel
+| n (bd_all f) := bd_all f.relabel
+
+namespace formula
+
+/-- The equality of two terms as a first-order formula. -/
+def equal (t₁ t₂ : L.term α) : (L.formula α) :=
+bd_equal (t₁.relabel sum.inl) (t₂.relabel sum.inl)
+
+/-- The graph of a function as a first-order formula. -/
+def graph (f : L.functions n) : L.formula (fin (n + 1)) :=
+equal (func f (λ i, var i)) (var n)
+
+end formula
 end formula
 
 variable {L}
@@ -910,6 +988,81 @@ realize_formula M φ pempty.elim
 
 variable {M}
 
+@[simp] lemma realize_bounded_formula_relabel {α β : Type} {n : ℕ}
+  (g : α → β) (v : β → M) (xs : fin n → M) (φ : L.bounded_formula α n) :
+  realize_bounded_formula M (φ.relabel g) v xs ↔ realize_bounded_formula M φ (v ∘ g) xs :=
+begin
+  have h : ∀ (m : ℕ) (xs' : fin m → M), sum.elim v xs' ∘
+    sum.elim (sum.inl ∘ g) sum.inr = sum.elim (v ∘ g) xs',
+  { intros m xs',
+    ext x,
+    cases x;
+    simp, },
+  induction φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3,
+  { refl },
+  { simp [h _ xs] },
+  { simp [h _ xs] },
+  { simp [ih1, ih2] },
+  { simp [ih3] }
+end
+
+@[simp] lemma equiv.realize_bounded_formula {α : Type} {n : ℕ}  (v : α → M)
+  (xs : fin n → M) (φ : L.bounded_formula α n) (g : M ≃[L] N) :
+  realize_bounded_formula N φ (g ∘ v) (g ∘ xs) ↔ realize_bounded_formula M φ v xs :=
+begin
+  induction φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3,
+  { refl },
+  { simp only [realize_bounded_formula, ← sum.comp_elim, equiv.realize_term, g.injective.eq_iff] },
+  { simp only [realize_bounded_formula, ← sum.comp_elim, equiv.realize_term, g.map_rel], },
+  { rw [realize_bounded_formula, ih1, ih2, realize_bounded_formula] },
+  { rw [realize_bounded_formula, realize_bounded_formula],
+    split,
+    { intros h a,
+      have h' := h (g a),
+      rw [← fin.comp_cons, ih3] at h',
+      exact h' },
+    { intros h a,
+      have h' := h (g.symm a),
+      rw [← ih3, fin.comp_cons, g.apply_symm_apply] at h',
+      exact h' }}
+end
+
+@[simp] lemma realize_bounded_formula_top {α : Type} {n : ℕ} (v : α → (⊤ : L.substructure M))
+  (xs : fin n → (⊤ : L.substructure M)) (φ : L.bounded_formula α n) :
+  realize_bounded_formula (⊤ : L.substructure M) φ v xs ↔
+  realize_bounded_formula M φ (coe ∘ v) (coe ∘ xs) :=
+begin
+  rw ← substructure.top_equiv.realize_bounded_formula v xs φ,
+  simp,
+end
+
+@[simp] lemma realize_formula_relabel {α β : Type}
+  (g : α → β) (v : β → M) (φ : L.formula α) :
+  realize_formula M (φ.relabel g) v ↔ realize_formula M φ (v ∘ g) :=
+by rw [realize_formula, realize_formula, realize_bounded_formula_relabel]
+
+@[simp] lemma realize_formula_equiv {α : Type}  (v : α → M) (φ : L.formula α)
+  (g : M ≃[L] N) :
+  realize_formula N φ (g ∘ v) ↔ realize_formula M φ v :=
+begin
+  rw [realize_formula, realize_formula, ← equiv.realize_bounded_formula v fin_zero_elim φ g,
+    iff_eq_eq],
+  exact congr rfl (funext fin_zero_elim),
+end
+
+@[simp]
+lemma realize_equal {α : Type*} (t₁ t₂ : L.term α) (x : α → M) :
+  realize_formula M (formula.equal t₁ t₂) x ↔ realize_term x t₁ = realize_term x t₂ :=
+by simp [formula.equal, realize_formula]
+
+@[simp]
+lemma realize_graph {l : ℕ} (f : L.functions l) (x : fin l → M) (y : M) :
+  realize_formula M (formula.graph f) (fin.snoc x y) ↔ fun_map f x = y :=
+begin
+  simp only [formula.graph, realize_term, fin.coe_eq_cast_succ, realize_equal, fin.snoc_cast_succ],
+  rw [fin.coe_nat_eq_last, fin.snoc_last],
+end
+
 section definability
 
 variables (L) [fintype α]