mathlib3 documentation

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 #

Main Results #

Implementation Notes #

References #

TODO #

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 ι] [is_directed ι has_le.le] [nonempty ι] (G : ι Type (max w w')) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [directed_system G (λ (i j : ι) (h : i j), (f i j h))] :

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

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

Equations

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