Elementary Maps Between First-Order Structures #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main Definitions #
first_order.language.elementary_embeddingis an embedding that commutes with the realizations of formulas.
first_order.language.elementary_substructureis a substructure where the realization of each formula agrees with the realization in the larger model.
first_order.language.elementary_diagramof a structure is the set of all sentences with parameters that the structure satisfies.
first_order.language.elementary_embedding.of_models_elementary_diagramis the canonical elementary embedding of any structure into a model of its elementary diagram.
Main Results #
- The Tarski-Vaught Test for embeddings:
first_order.language.embedding.is_elementary_of_existsgives a simple criterion for an embedding to be elementary.
- The Tarski-Vaught Test for substructures:
first_order.language.embedding.is_elementary_of_existsgives a simple criterion for a substructure to be elementary.
- to_fun : M → N
- map_formula' : (∀ ⦃n : ℕ⦄ (φ : L.formula (fin n)) (x : fin n → M), φ.realize (self.to_fun ∘ x) ↔ φ.realize x) . "obviously"
An elementary embedding of first-order structures is an embedding that commutes with the realizations of formulas.
An elementary embedding is also a first-order embedding.
An elementary embedding is also a first-order homomorphism.
The identity elementary embedding from a structure to itself
Composition of elementary embeddings
Composition of elementary embeddings is associative.
The canonical elementary embedding of an
L-structure into any model of its elementary diagram
The Tarski-Vaught test for elementarity of an embedding.
Bundles an embedding satisfying the Tarski-Vaught test as an elementary embedding.
A first-order equivalence is also an elementary embedding.
A substructure is elementary when every formula applied to a tuple in the subtructure agrees with its value in the overall structure.
An elementary substructure is one in which every formula applied to a tuple in the subtructure agrees with its value in the overall structure.
The natural embedding of an
M of the structure
M is elementary.
The Tarski-Vaught test for elementarity of a substructure.
Bundles a substructure satisfying the Tarski-Vaught test as an elementary substructure.