Elementary Maps Between First-Order Structures #
Main Definitions #
- A
first_order.language.elementary_embedding
is an embedding that commutes with the realizations of formulas. - A
first_order.language.elementary_substructure
is a substructure where the realization of each formula agrees with the realization in the larger model.
- to_fun : M → N
- map_formula' : (∀ {n : ℕ} (φ : L.formula (fin n)) (x : fin n → M), first_order.language.realize_formula N φ (self.to_fun ∘ x) ↔ first_order.language.realize_formula M φ x) . "obviously"
An elementary embedding of first-order structures is an embedding that commutes with the realizations of formulas.
Equations
- first_order.language.elementary_embedding.has_coe_to_fun = {coe := λ (f : L.elementary_embedding M N), f.to_fun}
An elementary embedding is also a first-order embedding.
Equations
- f.to_embedding = {to_embedding := {to_fun := ⇑f, inj' := _}, map_fun' := _, map_rel' := _}
An elementary embedding is also a first-order homomorphism.
The identity elementary embedding from a structure to itself
Equations
- first_order.language.elementary_embedding.refl L M = {to_fun := id M, map_formula' := _}
Equations
Composition of elementary embeddings
Composition of elementary embeddings is associative.
A first-order equivalence is also an elementary embedding.
Equations
- f.to_elementary_embedding = {to_fun := ⇑f, map_formula' := _}
A substructure is elementary when every formula applied to a tuple in the subtructure agrees with its value in the overall structure.
Equations
- S.is_elementary = ∀ {n : ℕ} (φ : L.formula (fin n)) (x : fin n → ↥S), first_order.language.realize_formula M φ (coe ∘ x) ↔ first_order.language.realize_formula ↥S φ x
- to_substructure : L.substructure M
- is_elementary' : self.to_substructure.is_elementary
An elementary substructure is one in which every formula applied to a tuple in the subtructure agrees with its value in the overall structure.
Equations
- first_order.language.elementary_substructure.set_like = {coe := λ (x : L.elementary_substructure M), x.to_substructure.carrier, coe_injective' := _}
The natural embedding of an L.substructure
of M
into M
.
Equations
- S.subtype = {to_fun := coe coe_to_lift, map_formula' := _}
The substructure M
of the structure M
is elementary.