Elementary Maps Between First-Order Structures #
Main Definitions #
- A
FirstOrder.Language.ElementaryEmbedding
is an embedding that commutes with the realizations of formulas. - A
FirstOrder.Language.ElementarySubstructure
is a substructure where the realization of each formula agrees with the realization in the larger model. - The
FirstOrder.Language.elementaryDiagram
of a structure is the set of all sentences with parameters that the structure satisfies. FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram
is the canonical elementary embedding of any structure into a model of its elementary diagram.
Main Results #
- The Tarski-Vaught Test for embeddings:
FirstOrder.Language.Embedding.isElementary_of_exists
gives a simple criterion for an embedding to be elementary. - The Tarski-Vaught Test for substructures:
FirstOrder.Language.Substructure.isElementary_of_exists
gives a simple criterion for a substructure to be elementary.
- toFun : M → N
- map_formula' : ∀ ⦃n : ℕ⦄ (φ : FirstOrder.Language.Formula L (Fin n)) (x : Fin n → M), FirstOrder.Language.Formula.Realize φ (↑s ∘ x) ↔ FirstOrder.Language.Formula.Realize φ x
An elementary embedding of first-order structures is an embedding that commutes with the realizations of formulas.
Instances For
An elementary embedding of first-order structures is an embedding that commutes with the realizations of formulas.
Instances For
An elementary embedding is also a first-order embedding.
Instances For
An elementary embedding is also a first-order homomorphism.
Instances For
The identity elementary embedding from a structure to itself
Instances For
Composition of elementary embeddings
Instances For
Composition of elementary embeddings is associative.
The elementary diagram of an L
-structure is the set of all sentences with parameters it
satisfies.
Instances For
The canonical elementary embedding of an L
-structure into any model of its elementary diagram
Instances For
The Tarski-Vaught test for elementarity of an embedding.
Bundles an embedding satisfying the Tarski-Vaught test as an elementary embedding.
Instances For
A first-order equivalence is also an elementary embedding.
Instances For
A substructure is elementary when every formula applied to a tuple in the subtructure agrees with its value in the overall structure.
Instances For
- toSubstructure : FirstOrder.Language.Substructure L M
- isElementary' : FirstOrder.Language.Substructure.IsElementary ↑s
An elementary substructure is one in which every formula applied to a tuple in the subtructure agrees with its value in the overall structure.
Instances For
The natural embedding of an L.Substructure
of M
into M
.
Instances For
The substructure 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.