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) [L.Structure M] :

Set (CategoryTheory.Bundled L.Structure)

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

Equations

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

Instances For

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

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, L.age ↑M ⊆ K

Instances For

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

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 L.Structure) => Nonempty (L.Embedding ↑M ↑N)) K

Instances For

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

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 L.Structure)) :

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

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

Instances

theorem FirstOrder.Language.IsFraisse.is_nonempty {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K] :

K.Nonempty

theorem FirstOrder.Language.IsFraisse.FG {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K] (M : CategoryTheory.Bundled L.Structure) :

M ∈ K → FirstOrder.Language.Structure.FG L ↑M

theorem FirstOrder.Language.IsFraisse.is_equiv_invariant {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K] (M : CategoryTheory.Bundled L.Structure) (N : CategoryTheory.Bundled L.Structure) :

Nonempty (L.Equiv ↑M ↑N) → (M ∈ K ↔ N ∈ K)

theorem FirstOrder.Language.IsFraisse.is_essentially_countable {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K] :

(Quotient.mk' '' K).Countable

theorem FirstOrder.Language.IsFraisse.hereditary {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K] :

FirstOrder.Language.Hereditary K

theorem FirstOrder.Language.IsFraisse.jointEmbedding {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K] :

FirstOrder.Language.JointEmbedding K

theorem FirstOrder.Language.IsFraisse.amalgamation {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K] :

FirstOrder.Language.Amalgamation K

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

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

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

L.age M ⊆ L.age N

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

L.age M = L.age N

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

N ∈ L.age ↑M

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

M ∈ K ↔ N ∈ K

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

(L.age M).Nonempty

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

FirstOrder.Language.Hereditary (L.age M)

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

FirstOrder.Language.JointEmbedding (L.age M)

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

(Quotient.mk' '' L.age M).Countable

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 : ι) → L.Structure (G i)] (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] :

L.age (FirstOrder.Language.DirectLimit G f) = ⋃ (i : ι), L.age (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 L.Structure)} (hn : K.Nonempty) (h : ∀ (M N : CategoryTheory.Bundled L.Structure), Nonempty (L.Equiv ↑M ↑N) → (M ∈ K ↔ N ∈ K)) (hc : (Quotient.mk' '' K).Countable) (fg : ∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) (hp : FirstOrder.Language.Hereditary K) (jep : FirstOrder.Language.JointEmbedding K) :

∃ (M : CategoryTheory.Bundled L.Structure), FirstOrder.Language.Structure.CG L ↑M ∧ L.age ↑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 L.Structure)} [Countable ((l : ℕ) × L.Functions l)] :

(∃ (M : CategoryTheory.Bundled L.Structure), Countable ↑M ∧ L.age ↑M = K) ↔ K.Nonempty ∧ (∀ (M N : CategoryTheory.Bundled L.Structure), Nonempty (L.Equiv ↑M ↑N) → (M ∈ K ↔ N ∈ K)) ∧ (Quotient.mk' '' K).Countable ∧ (∀ 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) [L.Structure M] :

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

Equations

L.IsUltrahomogeneous M = ∀ (S : L.Substructure M), S.FG → ∀ (f : L.Embedding (↥S) M), ∃ (g : L.Equiv M M), f = g.toEmbedding.comp S.subtype

Instances For

structure FirstOrder.Language.IsFraisseLimit {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled L.Structure)) (M : Type w) [L.Structure 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 : L.IsUltrahomogeneous M
age : L.age M = K

Instances For

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

L.IsUltrahomogeneous M

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

L.age M = K

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

FirstOrder.Language.Amalgamation (L.age M)

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

FirstOrder.Language.IsFraisse (L.age M)

theorem FirstOrder.Language.IsFraisseLimit.isFraisse {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled L.Structure)) {M : Type w} [L.Structure 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é.