Documentation

Mathlib.ModelTheory.Fraisse

Fraïssé Classes and Fraïssé Limits #

This file pertains to the ages of countable first-order structures. The age of a structure is the class of all finitely-generated structures that embed into it.

Of particular interest are Fraïssé classes, which are exactly the ages of countable ultrahomogeneous structures. To each is associated a unique (up to nonunique isomorphism) Fraïssé limit - the countable ultrahomogeneous structure with that age.

Main Definitions #

FirstOrder.Language.age is the class of finitely-generated structures that embed into a particular structure.
A class K is FirstOrder.Language.Hereditary when all finitely-generated structures that embed into structures in K are also in K.
A class K has FirstOrder.Language.JointEmbedding when for every M, N in K, there is another structure in K into which both M and N embed.
A class K has FirstOrder.Language.Amalgamation when for any pair of embeddings of a structure M in K into other structures in K, those two structures can be embedded into a fourth structure in K such that the resulting square of embeddings commutes.
FirstOrder.Language.IsFraisse indicates that a class is nonempty, isomorphism-invariant, essentially countable, and satisfies the hereditary, joint embedding, and amalgamation properties.
FirstOrder.Language.IsFraisseLimit indicates that a structure is a Fraïssé limit for a given class.

Main Results #

We show that the age of any structure is isomorphism-invariant and satisfies the hereditary and joint-embedding properties.
FirstOrder.Language.age.countable_quotient shows that the age of any countable structure is essentially countable.
FirstOrder.Language.exists_countable_is_age_of_iff gives necessary and sufficient conditions for a class to be the age of a countable structure in a language with countably many functions.

Implementation Notes #

Classes of structures are formalized with Set (Bundled L.Structure).
Some results pertain to countable limit structures, others to countably-generated limit structures. In the case of a language with countably many function symbols, these are equivalent.

References #

[W. Hodges, A Shorter Model Theory][Hodges97]
[K. Tent, M. Ziegler, A Course in Model Theory][Tent_Ziegler]

TODO #

Show existence and uniqueness of Fraïssé limits

The Age of a Structure and Fraïssé Classes #

def FirstOrder.Language.age (L : FirstOrder.Language) (M : Type w) [FirstOrder.Language.Structure L M] :

Set (CategoryTheory.Bundled (FirstOrder.Language.Structure L))

The age of a structure M is the class of finitely-generated structures that embed into it.

Equations

FirstOrder.Language.age L M = {N : CategoryTheory.Bundled (FirstOrder.Language.Structure L) | FirstOrder.Language.Structure.FG L ↑N ∧ Nonempty (FirstOrder.Language.Embedding L (↑N) M)}

Instances For

def FirstOrder.Language.Hereditary {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled (FirstOrder.Language.Structure L))) :

A class K has the hereditary property when all finitely-generated structures that embed into structures in K are also in K.

Equations

FirstOrder.Language.Hereditary K = ∀ M ∈ K, FirstOrder.Language.age L ↑M ⊆ K

Instances For

def FirstOrder.Language.JointEmbedding {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled (FirstOrder.Language.Structure L))) :

A class K has the joint embedding property when for every M, N in K, there is another structure in K into which both M and N embed.

Equations

FirstOrder.Language.JointEmbedding K = DirectedOn (fun (M N : CategoryTheory.Bundled (FirstOrder.Language.Structure L)) => Nonempty (FirstOrder.Language.Embedding L ↑M ↑N)) K

Instances For

def FirstOrder.Language.Amalgamation {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled (FirstOrder.Language.Structure L))) :

A class K has the amalgamation property when for any pair of embeddings of a structure M in K into other structures in K, those two structures can be embedded into a fourth structure in K such that the resulting square of embeddings commutes.

Equations

One or more equations did not get rendered due to their size.

Instances For

class FirstOrder.Language.IsFraisse {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled (FirstOrder.Language.Structure L))) :

A Fraïssé class is a nonempty, isomorphism-invariant, essentially countable class of structures satisfying the hereditary, joint embedding, and amalgamation properties.

is_nonempty : Set.Nonempty K
FG : ∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M
is_equiv_invariant : ∀ (M N : CategoryTheory.Bundled (FirstOrder.Language.Structure L)), Nonempty (FirstOrder.Language.Equiv L ↑M ↑N) → (M ∈ K ↔ N ∈ K)
is_essentially_countable : Set.Countable (Quotient.mk' '' K)
hereditary : FirstOrder.Language.Hereditary K
jointEmbedding : FirstOrder.Language.JointEmbedding K
amalgamation : FirstOrder.Language.Amalgamation K

Instances

theorem FirstOrder.Language.age.is_equiv_invariant (L : FirstOrder.Language) (M : Type w) [FirstOrder.Language.Structure L M] (N : CategoryTheory.Bundled (FirstOrder.Language.Structure L)) (P : CategoryTheory.Bundled (FirstOrder.Language.Structure L)) (h : Nonempty (FirstOrder.Language.Equiv L ↑N ↑P)) :

N ∈ FirstOrder.Language.age L M ↔ P ∈ FirstOrder.Language.age L M

theorem FirstOrder.Language.Embedding.age_subset_age {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {N : Type w} [FirstOrder.Language.Structure L N] (MN : FirstOrder.Language.Embedding L M N) :

FirstOrder.Language.age L M ⊆ FirstOrder.Language.age L N

theorem FirstOrder.Language.Equiv.age_eq_age {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {N : Type w} [FirstOrder.Language.Structure L N] (MN : FirstOrder.Language.Equiv L M N) :

FirstOrder.Language.age L M = FirstOrder.Language.age L N

theorem FirstOrder.Language.Structure.FG.mem_age_of_equiv {L : FirstOrder.Language} {M : CategoryTheory.Bundled (FirstOrder.Language.Structure L)} {N : CategoryTheory.Bundled (FirstOrder.Language.Structure L)} (h : FirstOrder.Language.Structure.FG L ↑M) (MN : Nonempty (FirstOrder.Language.Equiv L ↑M ↑N)) :

N ∈ FirstOrder.Language.age L ↑M

theorem FirstOrder.Language.Hereditary.is_equiv_invariant_of_fg {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled (FirstOrder.Language.Structure L))} (h : FirstOrder.Language.Hereditary K) (fg : ∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) (M : CategoryTheory.Bundled (FirstOrder.Language.Structure L)) (N : CategoryTheory.Bundled (FirstOrder.Language.Structure L)) (hn : Nonempty (FirstOrder.Language.Equiv L ↑M ↑N)) :

M ∈ K ↔ N ∈ K

theorem FirstOrder.Language.age.nonempty {L : FirstOrder.Language} (M : Type w) [FirstOrder.Language.Structure L M] :

Set.Nonempty (FirstOrder.Language.age L M)

theorem FirstOrder.Language.age.hereditary {L : FirstOrder.Language} (M : Type w) [FirstOrder.Language.Structure L M] :

FirstOrder.Language.Hereditary (FirstOrder.Language.age L M)

theorem FirstOrder.Language.age.jointEmbedding {L : FirstOrder.Language} (M : Type w) [FirstOrder.Language.Structure L M] :

FirstOrder.Language.JointEmbedding (FirstOrder.Language.age L M)

theorem FirstOrder.Language.age.countable_quotient {L : FirstOrder.Language} (M : Type w) [FirstOrder.Language.Structure L M] [h : Countable M] :

Set.Countable (Quotient.mk' '' FirstOrder.Language.age L M)

The age of a countable structure is essentially countable (has countably many isomorphism classes).

theorem FirstOrder.Language.age_directLimit {L : FirstOrder.Language} {ι : Type w} [Preorder ι] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [Nonempty ι] (G : ι → Type (max w w')) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] :

FirstOrder.Language.age L (FirstOrder.Language.DirectLimit G f) = ⋃ (i : ι), FirstOrder.Language.age L (G i)

The age of a direct limit of structures is the union of the ages of the structures.

theorem FirstOrder.Language.exists_cg_is_age_of {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled (FirstOrder.Language.Structure L))} (hn : Set.Nonempty K) (h : ∀ (M N : CategoryTheory.Bundled (FirstOrder.Language.Structure L)), Nonempty (FirstOrder.Language.Equiv L ↑M ↑N) → (M ∈ K ↔ N ∈ K)) (hc : Set.Countable (Quotient.mk' '' K)) (fg : ∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) (hp : FirstOrder.Language.Hereditary K) (jep : FirstOrder.Language.JointEmbedding K) :

∃ (M : CategoryTheory.Bundled (FirstOrder.Language.Structure L)), FirstOrder.Language.Structure.CG L ↑M ∧ FirstOrder.Language.age L ↑M = K

Sufficient conditions for a class to be the age of a countably-generated structure.

theorem FirstOrder.Language.exists_countable_is_age_of_iff {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled (FirstOrder.Language.Structure L))} [Countable ((l : ℕ) × L.Functions l)] :

(∃ (M : CategoryTheory.Bundled (FirstOrder.Language.Structure L)), Countable ↑M ∧ FirstOrder.Language.age L ↑M = K) ↔ Set.Nonempty K ∧ (∀ (M N : CategoryTheory.Bundled (FirstOrder.Language.Structure L)), Nonempty (FirstOrder.Language.Equiv L ↑M ↑N) → (M ∈ K ↔ N ∈ K)) ∧ Set.Countable (Quotient.mk' '' K) ∧ (∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) ∧ FirstOrder.Language.Hereditary K ∧ FirstOrder.Language.JointEmbedding K

def FirstOrder.Language.IsUltrahomogeneous (L : FirstOrder.Language) (M : Type w) [FirstOrder.Language.Structure L M] :

A structure M is ultrahomogeneous if every embedding of a finitely generated substructure into M extends to an automorphism of M.

Equations

One or more equations did not get rendered due to their size.

Instances For

structure FirstOrder.Language.IsFraisseLimit {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled (FirstOrder.Language.Structure L))) (M : Type w) [FirstOrder.Language.Structure L M] [Countable ((l : ℕ) × L.Functions l)] [Countable M] :

A structure M is a Fraïssé limit for a class K if it is countably generated, ultrahomogeneous, and has age K.

ultrahomogeneous : FirstOrder.Language.IsUltrahomogeneous L M
age : FirstOrder.Language.age L M = K

Instances For

theorem FirstOrder.Language.IsUltrahomogeneous.amalgamation_age {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (h : FirstOrder.Language.IsUltrahomogeneous L M) :

FirstOrder.Language.Amalgamation (FirstOrder.Language.age L M)

theorem FirstOrder.Language.IsUltrahomogeneous.age_isFraisse {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] [Countable M] (h : FirstOrder.Language.IsUltrahomogeneous L M) :

FirstOrder.Language.IsFraisse (FirstOrder.Language.age L M)

theorem FirstOrder.Language.IsFraisseLimit.isFraisse {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled (FirstOrder.Language.Structure L))) {M : Type w} [FirstOrder.Language.Structure L M] [Countable ((l : ℕ) × L.Functions l)] [Countable M] (h : FirstOrder.Language.IsFraisseLimit K M) :

FirstOrder.Language.IsFraisse K

If a class has a Fraïssé limit, it must be Fraïssé.