feat: port ModelTheory.Ultraproducts (#3976)

Co-authored-by: Chris Hughes <chrishughes24@gmail.com>

Mathlib.lean

@@ -1781,6 +1781,7 @@ import Mathlib.ModelTheory.Semantics
 import Mathlib.ModelTheory.Skolem
 import Mathlib.ModelTheory.Substructures
 import Mathlib.ModelTheory.Syntax
+import Mathlib.ModelTheory.Ultraproducts
 import Mathlib.NumberTheory.ADEInequality
 import Mathlib.NumberTheory.Basic
 import Mathlib.NumberTheory.ClassNumber.AdmissibleAbs

Mathlib/ModelTheory/Ultraproducts.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2022 Aaron Anderson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aaron Anderson
+
+! This file was ported from Lean 3 source module model_theory.ultraproducts
+! leanprover-community/mathlib commit f1ae620609496a37534c2ab3640b641d5be8b6f0
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.ModelTheory.Quotients
+import Mathlib.Order.Filter.Germ
+import Mathlib.Order.Filter.Ultrafilter
+
+/-! # Ultraproducts and Łoś's Theorem
+
+## Main Definitions
+* `FirstOrder.Language.Ultraproduct.Structure` is the ultraproduct structure on `Filter.Product`.
+
+## Main Results
+* Łoś's Theorem: `FirstOrder.Language.Ultraproduct.sentence_realize`. An ultraproduct models a
+sentence `φ` if and only if the set of structures in the product that model `φ` is in the
+ultrafilter.
+
+## Tags
+ultraproduct, Los's theorem
+
+-/
+
+
+universe u v
+
+variable {α : Type _} (M : α → Type _) (u : Ultrafilter α)
+
+open FirstOrder Filter
+
+open Filter
+
+namespace FirstOrder
+
+namespace Language
+
+open Structure
+
+variable {L : Language.{u, v}} [∀ a, L.Structure (M a)]
+
+namespace Ultraproduct
+
+instance setoidPrestructure : L.Prestructure ((u : Filter α).productSetoid M) :=
+  { (u : Filter α).productSetoid M with
+    toStructure :=
+      { funMap := fun {n} f x a => funMap f fun i => x i a
+        RelMap := fun {n} r x => ∀ᶠ a : α in u, RelMap r fun i => x i a }
+    fun_equiv := fun {n} f x y xy => by
+      refine' mem_of_superset (iInter_mem.2 xy) fun a ha => _
+      simp only [Set.mem_iInter, Set.mem_setOf_eq] at ha
+      simp only [Set.mem_setOf_eq, ha]
+    rel_equiv := fun {n} r x y xy => by
+      rw [← iff_eq_eq]
+      refine' ⟨fun hx => _, fun hy => _⟩
+      · refine' mem_of_superset (inter_mem hx (iInter_mem.2 xy)) _
+        rintro a ⟨ha1, ha2⟩
+        simp only [Set.mem_iInter, Set.mem_setOf_eq] at *
+        rw [← funext ha2]
+        exact ha1
+      · refine' mem_of_superset (inter_mem hy (iInter_mem.2 xy)) _
+        rintro a ⟨ha1, ha2⟩
+        simp only [Set.mem_iInter, Set.mem_setOf_eq] at *
+        rw [funext ha2]
+        exact ha1 }
+#align first_order.language.ultraproduct.setoid_prestructure FirstOrder.Language.Ultraproduct.setoidPrestructure
+
+variable {M} {u}
+
+instance «structure» : L.Structure ((u : Filter α).Product M) :=
+  Language.quotientStructure
+set_option linter.uppercaseLean3 false in
+#align first_order.language.ultraproduct.Structure FirstOrder.Language.Ultraproduct.structure
+
+theorem funMap_cast {n : ℕ} (f : L.Functions n) (x : Fin n → ∀ a, M a) :
+    (funMap f fun i => (x i : (u : Filter α).Product M)) =
+      (fun a => funMap f fun i => x i a : (u : Filter α).Product M) := by
+  apply funMap_quotient_mk'
+#align first_order.language.ultraproduct.fun_map_cast FirstOrder.Language.Ultraproduct.funMap_cast
+
+theorem term_realize_cast {β : Type _} (x : β → ∀ a, M a) (t : L.Term β) :
+    (t.realize fun i => (x i : (u : Filter α).Product M)) =
+      (fun a => t.realize fun i => x i a : (u : Filter α).Product M) := by
+  convert @Term.realize_quotient_mk' L _ ((u : Filter α).productSetoid M)
+      (Ultraproduct.setoidPrestructure M u) _ t x using 2
+  ext a
+  induction t
+  case var =>
+    rfl
+  case func _ _ _ t_ih =>
+    simp only [Term.realize, t_ih]
+    rfl
+#align first_order.language.ultraproduct.term_realize_cast FirstOrder.Language.Ultraproduct.term_realize_cast
+
+variable [∀ a : α, Nonempty (M a)]
+
+theorem boundedFormula_realize_cast {β : Type _} {n : ℕ} (φ : L.BoundedFormula β n)
+    (x : β → ∀ a, M a) (v : Fin n → ∀ a, M a) :
+    (φ.Realize (fun i : β => (x i : (u : Filter α).Product M))
+        (fun i => (v i : (u : Filter α).Product M))) ↔
+      ∀ᶠ a : α in u, φ.Realize (fun i : β => x i a) fun i => v i a := by
+  letI := (u : Filter α).productSetoid M
+  induction' φ with _ _ _ _ _ _ _ _ m _ _ ih ih' k φ ih
+  · simp only [BoundedFormula.Realize, eventually_const]
+  · have h2 : ∀ a : α, (Sum.elim (fun i : β => x i a) fun i => v i a) = fun i => Sum.elim x v i a :=
+      fun a => funext fun i => Sum.casesOn i (fun i => rfl) fun i => rfl
+    simp only [BoundedFormula.Realize, h2, term_realize_cast]
+    erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm,
+      term_realize_cast, term_realize_cast]
+    exact Quotient.eq''
+  · have h2 : ∀ a : α, (Sum.elim (fun i : β => x i a) fun i => v i a) = fun i => Sum.elim x v i a :=
+      fun a => funext fun i => Sum.casesOn i (fun i => rfl) fun i => rfl
+    simp only [BoundedFormula.Realize, h2]
+    erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm]
+    conv_lhs => enter [2, i]; erw [term_realize_cast]
+    apply relMap_quotient_mk'
+  · simp only [BoundedFormula.Realize, ih v, ih' v]
+    rw [Ultrafilter.eventually_imp]
+  · simp only [BoundedFormula.Realize]
+    apply Iff.trans (b := ∀ m : ∀ a : α, M a,
+      φ.Realize (fun i : β => (x i : (u : Filter α).Product M))
+        (Fin.snoc (((↑) : (∀ a, M a) → (u : Filter α).Product M) ∘ v)
+          (m : (u : Filter α).Product M)))
+    · exact forall_quotient_iff
+    have h' :
+      ∀ (m : ∀ a, M a) (a : α),
+        (fun i : Fin (k + 1) => (Fin.snoc v m : _ → ∀ a, M a) i a) =
+          Fin.snoc (fun i : Fin k => v i a) (m a) := by
+      refine' fun m a => funext (Fin.reverseInduction _ fun i _ => _)
+      · simp only [Fin.snoc_last]
+      · simp only [Fin.snoc_castSucc]
+    simp only [← Fin.comp_snoc]
+    simp only [Function.comp, ih, h']
+    refine' ⟨fun h => _, fun h m => _⟩
+    · contrapose! h
+      simp_rw [← Ultrafilter.eventually_not, not_forall] at h
+      refine'
+        ⟨fun a : α =>
+          Classical.epsilon fun m : M a =>
+            ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m),
+          _⟩
+      rw [← Ultrafilter.eventually_not]
+      exact Filter.mem_of_superset h fun a ha => Classical.epsilon_spec ha
+    · rw [Filter.eventually_iff] at *
+      exact Filter.mem_of_superset h fun a ha => ha (m a)
+#align first_order.language.ultraproduct.bounded_formula_realize_cast FirstOrder.Language.Ultraproduct.boundedFormula_realize_cast
+
+theorem realize_formula_cast {β : Type _} (φ : L.Formula β) (x : β → ∀ a, M a) :
+    (φ.Realize fun i => (x i : (u : Filter α).Product M)) ↔
+      ∀ᶠ a : α in u, φ.Realize fun i => x i a := by
+  simp_rw [Formula.Realize, ← boundedFormula_realize_cast φ x, iff_eq_eq]
+  exact congr rfl (Subsingleton.elim _ _)
+#align first_order.language.ultraproduct.realize_formula_cast FirstOrder.Language.Ultraproduct.realize_formula_cast
+
+/-- Łoś's Theorem : A sentence is true in an ultraproduct if and only if the set of structures it is
+  true in is in the ultrafilter. -/
+theorem sentence_realize (φ : L.Sentence) :
+    (u : Filter α).Product M ⊨ φ ↔ ∀ᶠ a : α in u, M a ⊨ φ := by
+  simp_rw [Sentence.Realize]
+  erw [← realize_formula_cast φ, iff_eq_eq]
+  exact congr rfl (Subsingleton.elim _ _)
+#align first_order.language.ultraproduct.sentence_realize FirstOrder.Language.Ultraproduct.sentence_realize
+
+nonrec instance Product.instNonempty : Nonempty ((u : Filter α).Product M) :=
+  letI : ∀ a, Inhabited (M a) := fun _ => Classical.inhabited_of_nonempty'
+  instNonempty
+#align first_order.language.ultraproduct.product.nonempty FirstOrder.Language.Ultraproduct.Product.instNonempty
+
+end Ultraproduct
+
+end Language
+
+end FirstOrder