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.
• FirstOrder.Language.IsFraisseLimit.nonempty_equiv shows that any class which is Fraïssé has at most one Fraïssé limit up to equivalence.
• FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite shows that any countably infinite structure in the empty language is a Fraïssé limit of the class of finite structures.
• FirstOrder.Language.empty.isFraisse_finite shows that the class of finite structures in the empty language is Fraïssé.

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 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)}

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

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

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

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

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

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.

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

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

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.fg_substructure {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} (fg : S.FG) : { α := ↥S, str := inferInstance } ∈ L.age M

theorem FirstOrder.Language.age.has_representative_as_substructure {L : FirstOrder.Language} (M : Type w) [L.Structure M] (C : Quotient FirstOrder.Language.equivSetoid) : C ∈ Quotient.mk' '' L.age M → ∃ (V : { V : L.Substructure M // V.FG }), ⟦{ α := ↥↑V, str := inferInstance }⟧ = C

Any class in the age of a structure has a representative which is a finitely generated substructure.

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 (x1 x2 : ι) => x1 ≤ x2] [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] : Prop

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

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] : Prop

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

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.extend_embedding {L : FirstOrder.Language} {M : Type w} [L.Structure M] (M_homog : L.IsUltrahomogeneous M) {S : Type u_1} [L.Structure S] (S_FG : FirstOrder.Language.Structure.FG L S) {T : Type u_2} [L.Structure T] [h : Nonempty (L.Embedding T M)] (f : L.Embedding S M) (g : L.Embedding S T) : ∃ (f' : L.Embedding T M), f = f'.comp g

Any embedding from a finitely generated S to an ultrahomogeneous structure M can be extended to an embedding from any structure with an embedding to M.

theorem FirstOrder.Language.isUltrahomogeneous_iff_IsExtensionPair {L : FirstOrder.Language} {M : Type w} [L.Structure M] (M_CG : FirstOrder.Language.Structure.CG L M) : L.IsUltrahomogeneous M ↔ L.IsExtensionPair M M

A countably generated structure is ultrahomogeneous if and only if any equivalence between finitely generated substructures can be extended to any element in the domain.

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é.

theorem FirstOrder.Language.IsFraisseLimit.isExtensionPair {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] [Countable ((l : ℕ) × L.Functions l)] [Countable M] [Countable N] (hM : FirstOrder.Language.IsFraisseLimit K M) (hN : FirstOrder.Language.IsFraisseLimit K N) : L.IsExtensionPair M N

theorem FirstOrder.Language.IsFraisseLimit.nonempty_equiv {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] [Countable ((l : ℕ) × L.Functions l)] [Countable M] [Countable N] (hM : FirstOrder.Language.IsFraisseLimit K M) (hN : FirstOrder.Language.IsFraisseLimit K N) : Nonempty (L.Equiv M N)

The Fraïssé limit of a class is unique, in that any two Fraïssé limits are isomorphic.

theorem FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite (M : Type u_1) [Countable M] [Infinite M] [FirstOrder.Language.empty.Structure M] : FirstOrder.Language.IsFraisseLimit {S : CategoryTheory.Bundled FirstOrder.Language.empty.Structure | Finite ↑S} M

Any countable infinite structure in the empty language is a Fraïssé limit of the class of finite structures.

theorem FirstOrder.Language.empty.isFraisse_finite : FirstOrder.Language.IsFraisse {S : CategoryTheory.Bundled FirstOrder.Language.empty.Structure | Finite ↑S}

The class of finite structures in the empty language is Fraïssé.