Ultraproducts and Łoś's Theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main Definitions #
first_order.language.ultraproduct.Structureis the ultraproduct structure onfilter.product.
Main Results #
- Łoś's Theorem:
first_order.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
@[protected, instance]
def
first_order.language.ultraproduct.setoid_prestructure
{α : Type u_1}
(M : α → Type u_2)
(u : ultrafilter α)
{L : first_order.language}
[Π (a : α), L.Structure (M a)] :
L.prestructure (↑u.product_setoid M)
Equations
- first_order.language.ultraproduct.setoid_prestructure M u = {to_structure := {fun_map := λ (n : ℕ) (f : L.functions n) (x : fin n → Π (a : α), M a) (a : α), first_order.language.Structure.fun_map f (λ (i : fin n), x i a), rel_map := λ (n : ℕ) (r : L.relations n) (x : fin n → Π (a : α), M a), ∀ᶠ (a : α) in ↑u, first_order.language.Structure.rel_map r (λ (i : fin n), x i a)}, fun_equiv := _, rel_equiv := _}
@[protected, instance]
def
first_order.language.ultraproduct.Structure
{α : Type u_1}
{M : α → Type u_2}
{u : ultrafilter α}
{L : first_order.language}
[Π (a : α), L.Structure (M a)] :
theorem
first_order.language.ultraproduct.fun_map_cast
{α : Type u_1}
{M : α → Type u_2}
{u : ultrafilter α}
{L : first_order.language}
[Π (a : α), L.Structure (M a)]
{n : ℕ}
(f : L.functions n)
(x : fin n → Π (a : α), M a) :
first_order.language.Structure.fun_map f (λ (i : fin n), ↑(x i)) = ↑(λ (a : α), first_order.language.Structure.fun_map f (λ (i : fin n), x i a))
theorem
first_order.language.ultraproduct.term_realize_cast
{α : Type u_1}
{M : α → Type u_2}
{u : ultrafilter α}
{L : first_order.language}
[Π (a : α), L.Structure (M a)]
{β : Type u_3}
(x : β → Π (a : α), M a)
(t : L.term β) :
first_order.language.term.realize (λ (i : β), ↑(x i)) t = ↑(λ (a : α), first_order.language.term.realize (λ (i : β), x i a) t)
theorem
first_order.language.ultraproduct.bounded_formula_realize_cast
{α : Type u_1}
{M : α → Type u_2}
{u : ultrafilter α}
{L : first_order.language}
[Π (a : α), L.Structure (M a)]
[∀ (a : α), nonempty (M a)]
{β : Type u_3}
{n : ℕ}
(φ : L.bounded_formula β n)
(x : β → Π (a : α), M a)
(v : fin n → Π (a : α), M a) :
theorem
first_order.language.ultraproduct.realize_formula_cast
{α : Type u_1}
{M : α → Type u_2}
{u : ultrafilter α}
{L : first_order.language}
[Π (a : α), L.Structure (M a)]
[∀ (a : α), nonempty (M a)]
{β : Type u_3}
(φ : L.formula β)
(x : β → Π (a : α), M a) :
theorem
first_order.language.ultraproduct.sentence_realize
{α : Type u_1}
{M : α → Type u_2}
{u : ultrafilter α}
{L : first_order.language}
[Π (a : α), L.Structure (M a)]
[∀ (a : α), nonempty (M a)]
(φ : L.sentence) :
Ł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.