Documentation

Mathlib.ModelTheory.Ultraproducts

Ultraproducts and Łoś's Theorem #

Main Definitions #

Main Results #

Tags #

ultraproduct, Los's theorem

instance FirstOrder.Language.Ultraproduct.setoidPrestructure {α : Type u_1} (M : αType u_2) (u : Ultrafilter α) {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] :
L.Prestructure ((↑u).productSetoid M)
Equations
  • One or more equations did not get rendered due to their size.
instance FirstOrder.Language.Ultraproduct.structure {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] :
L.Structure ((↑u).Product M)
Equations
  • FirstOrder.Language.Ultraproduct.structure = FirstOrder.Language.quotientStructure
theorem FirstOrder.Language.Ultraproduct.funMap_cast {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] {n : } (f : L.Functions n) (x : Fin n(a : α) → M a) :
(FirstOrder.Language.Structure.funMap f fun (i : Fin n) => Quotient.mk' (x i)) = Quotient.mk' fun (a : α) => FirstOrder.Language.Structure.funMap f fun (i : Fin n) => x i a
theorem FirstOrder.Language.Ultraproduct.term_realize_cast {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] {β : Type u_3} (x : β(a : α) → M a) (t : L.Term β) :
FirstOrder.Language.Term.realize (fun (i : β) => Quotient.mk' (x i)) t = Quotient.mk' fun (a : α) => FirstOrder.Language.Term.realize (fun (i : β) => x i a) t
theorem FirstOrder.Language.Ultraproduct.boundedFormula_realize_cast {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] [∀ (a : α), Nonempty (M a)] {β : Type u_3} {n : } (φ : L.BoundedFormula β n) (x : β(a : α) → M a) (v : Fin n(a : α) → M a) :
(φ.Realize (fun (i : β) => Quotient.mk' (x i)) fun (i : Fin n) => Quotient.mk' (v i)) ∀ᶠ (a : α) in u, φ.Realize (fun (i : β) => x i a) fun (i : Fin n) => v i a
theorem FirstOrder.Language.Ultraproduct.realize_formula_cast {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] [∀ (a : α), Nonempty (M a)] {β : Type u_3} (φ : L.Formula β) (x : β(a : α) → M a) :
(φ.Realize fun (i : β) => Quotient.mk' (x i)) ∀ᶠ (a : α) in u, φ.Realize fun (i : β) => x i a
theorem FirstOrder.Language.Ultraproduct.sentence_realize {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] [∀ (a : α), Nonempty (M a)] (φ : L.Sentence) :
(↑u).Product M φ ∀ᶠ (a : α) in u, M a φ

Ł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.

instance FirstOrder.Language.Ultraproduct.Product.instNonempty {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} [∀ (a : α), Nonempty (M a)] :
Nonempty ((↑u).Product M)
Equations
  • =