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 #

Main Results #

Implementation Notes #

References #


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.

Instances For

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

    Instances For

      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.

      Instances For

        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.

        Instances For

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


            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 jFirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun i j h => ↑(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.

            Instances For

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

              Instances For