[Merged by Bors] - feat(model_theory/basic): define quotient structures

src/model_theory/basic.lean

@@ -1077,5 +1077,48 @@ instance : boolean_algebra (L.definable_set M α) :=
 end definable_set
 end definability
 
+section quotients
+
+variables (L) {M' : Type*}
+
+/-- A prestructure is a first-order structure with a `setoid` equivalence relation on it,
+  such that quotienting by that equivalence relation is still a structure. -/
+class prestructure (s : setoid M') :=
+(to_structure : L.Structure M')
+(fun_equiv : ∀{n} {f : L.functions n} (x y : fin n → M'),
+  x ≈ y → fun_map f x ≈ fun_map f y)
+(rel_equiv : ∀{n} {r : L.relations n} (x y : fin n → M') (h : x ≈ y),
+  (rel_map r x = rel_map r y))
+
+variables {L} {M'} {s : setoid M'} [ps : L.prestructure s]
+
+instance quotient_structure :
+  L.Structure (quotient s) :=
+{ fun_map := λ n f x, quotient.map (@fun_map L M' ps.to_structure n f) prestructure.fun_equiv
+    (quotient.fin_choice x),
+  rel_map := λ n r x, quotient.lift (@rel_map L M' ps.to_structure n r) prestructure.rel_equiv
+    (quotient.fin_choice x) }
+
+variables [s]
+include s
+
+lemma fun_map_quotient_mk {n : ℕ} (f : L.functions n) (x : fin n → M') :
+  fun_map f (λ i, ⟦x i⟧) = ⟦@fun_map _ _ ps.to_structure _ f x⟧ :=
+begin
+  change quotient.map (@fun_map L M' ps.to_structure n f) prestructure.fun_equiv
+    (quotient.fin_choice _) = _,
+  rw [quotient.fin_choice_eq, quotient.map_mk],
+end
+
+lemma realize_term_quotient_mk {β : Type*} (x : β → M') (t : L.term β) :
+  realize_term (λ i, ⟦x i⟧) t = ⟦@realize_term _ _ ps.to_structure _ x t⟧ :=
+begin
+  induction t with a1 a2 a3 a4 ih a6 a7 a8 a9 a0,
+  { refl },
+  simp only [ih, fun_map_quotient_mk, realize_term],
+end
+
+end quotients
+
 end language
 end first_order