feat(model_theory/basic,bundled): Structures induced by equivalences (#13124)

Defines `equiv.induced_Structure`, a structure on the codomain of a bijection that makes the bijection an isomorphism.
Defines maps on bundled models to shift them along bijections and up and down universes.

Author: awainverse

src/model_theory/basic.lean

@@ -6,6 +6,7 @@ Authors: Aaron Anderson, Jesse Michael Han, Floris van Doorn
 import data.fin.vec_notation
 import data.fin.tuple.basic
 import logic.encodable.basic
+import logic.small
 import set_theory.cardinal
 import category_theory.concrete_category.bundled
 
@@ -628,3 +629,22 @@ end sum_Structure
 
 end language
 end first_order
+
+namespace equiv
+open first_order first_order.language first_order.language.Structure
+open_locale first_order
+
+variables {L : language} {M : Type*} {N : Type*} [L.Structure M]
+
+/-- A structure induced by a bijection. -/
+@[simps] def induced_Structure (e : M ≃ N) : L.Structure N :=
+⟨λ n f x, e (fun_map f (e.symm ∘ x)), λ n r x, rel_map r (e.symm ∘ x)⟩
+
+/-- A bijection as a first-order isomorphism with the induced structure on the codomain. -/
+@[simps] def induced_Structure_equiv (e : M ≃ N) :
+  @language.equiv L M N _ (induced_Structure e) :=
+{ map_fun' := λ n f x, by simp [← function.comp.assoc e.symm e x],
+  map_rel' := λ n r x, by simp [← function.comp.assoc e.symm e x],
+  .. e }
+
+end equiv

src/model_theory/bundled.lean

@@ -18,7 +18,7 @@ This file bundles types together with their first-order structure.
 
 -/
 
-universes u v w
+universes u v w w'
 
 variables {L : first_order.language.{u v}}
 
@@ -73,6 +73,24 @@ instance : inhabited (Model (∅ : L.Theory)) :=
 
 end inhabited
 
+variable {T}
+
+/-- Maps a bundled model along a bijection. -/
+def equiv_induced {M : Model.{u v w} T} {N : Type w'} (e : M ≃ N) :
+  Model.{u v w'} T :=
+{ carrier := N,
+  struc := e.induced_Structure,
+  is_model := @equiv.Theory_model L M N _ e.induced_Structure T e.induced_Structure_equiv _,
+  nonempty' := e.symm.nonempty }
+
+/-- Shrinks a small model to a particular universe. -/
+noncomputable def shrink (M : Model.{u v w} T) [small.{w'} M] :
+  Model.{u v w'} T := equiv_induced (equiv_shrink M)
+
+/-- Lifts a model to a particular universe. -/
+def ulift (M : Model.{u v w} T) : Model.{u v (max w w')} T :=
+  equiv_induced (equiv.ulift.symm : M ≃ _)
+
 end Model
 
 variables {T}

src/model_theory/semantics.lean

@@ -580,7 +580,9 @@ end
 
 end bounded_formula
 
-@[simp] lemma equiv.realize_bounded_formula (g : M ≃[L] N) (φ : L.bounded_formula α n)
+namespace equiv
+
+@[simp] lemma realize_bounded_formula (g : M ≃[L] N) (φ : L.bounded_formula α n)
   {v : α → M} {xs : fin n → M} :
   φ.realize (g ∘ v) (g ∘ xs) ↔ φ.realize v xs :=
 begin
@@ -601,13 +603,19 @@ begin
       exact h' }}
 end
 
-@[simp] lemma equiv.realize_formula (g : M ≃[L] N) (φ : L.formula α) {v : α → M}  :
+@[simp] lemma realize_formula (g : M ≃[L] N) (φ : L.formula α) {v : α → M} :
   φ.realize (g ∘ v) ↔ φ.realize v :=
-begin
-  rw [formula.realize, formula.realize, ← g.realize_bounded_formula φ,
-    iff_eq_eq],
-  exact congr rfl (funext fin_zero_elim),
-end
+by rw [formula.realize, formula.realize, ← g.realize_bounded_formula φ,
+    iff_eq_eq, unique.eq_default (g ∘ default)]
+
+lemma realize_sentence (g : M ≃[L] N) (φ : L.sentence) :
+  M ⊨ φ ↔ N ⊨ φ :=
+by rw [sentence.realize, sentence.realize, ← g.realize_formula, unique.eq_default (g ∘ default)]
+
+lemma Theory_model (g : M ≃[L] N) [M ⊨ T] : N ⊨ T :=
+⟨λ φ hφ, (g.realize_sentence φ).1 (Theory.realize_sentence_of_mem T hφ)⟩
+
+end equiv
 
 namespace relations
 open bounded_formula