# mathlib3documentation

model_theory.fraisse

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• first_order.language.age is the class of finitely-generated structures that embed into a particular structure.
• A class K has the first_order.language.hereditary when all finitely-generated structures that embed into structures in K are also in K.
• A class K has the first_order.language.joint_embedding when for every M, N in K, there is another structure in K into which both M and N embed.
• A class K has the first_order.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.
• first_order.language.is_fraisse indicates that a class is nonempty, isomorphism-invariant, essentially countable, and satisfies the hereditary, joint embedding, and amalgamation properties.
• first_order.language.is_fraisse_limit 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.
• first_order.language.age.countable_quotient shows that the age of any countable structure is essentially countable.
• first_order.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.

## TODO #

• Show existence and uniqueness of Fraïssé limits

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

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

Equations

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

Equations

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

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
@[class]

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

theorem first_order.language.embedding.age_subset_age {L : first_order.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 first_order.language.equiv.age_eq_age {L : first_order.language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (MN : L.equiv M N) :
L.age M = L.age N

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

@[simp]
theorem first_order.language.age_direct_limit {L : first_order.language} {ι : Type w} [preorder ι] [nonempty ι] (G : ι Type (max w w')) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] :
= (i : ι), L.age (G i)

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

theorem first_order.language.exists_cg_is_age_of {L : first_order.language} {K : set } (hn : K.nonempty) (h : (M N : , nonempty (L.equiv M N) (M K N K)) (hc : .countable) (fg : (M : , )  :
(M : , L.age M = K

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

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

Equations
structure first_order.language.is_fraisse_limit {L : first_order.language} (K : set ) (M : Type w) [L.Structure M] [countable (Σ (l : ), L.functions l)] [countable M] :
Prop
• ultrahomogeneous :
• age : L.age M = K

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

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