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 #

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.

References #

TODO #

Show existence and uniqueness of Fraïssé limits

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

def first_order.language.age (L : first_order.language) (M : Type w) [L.Structure M] :

set (category_theory.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 : category_theory.bundled L.Structure | first_order.language.Structure.fg L ↥N ∧ nonempty (L.embedding ↥N M)}

def first_order.language.hereditary {L : first_order.language} (K : set (category_theory.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

first_order.language.hereditary K = ∀ (M : category_theory.bundled L.Structure), M ∈ K → L.age ↥M ⊆ K

def first_order.language.joint_embedding {L : first_order.language} (K : set (category_theory.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

first_order.language.joint_embedding K = directed_on (λ (M N : category_theory.bundled L.Structure), nonempty (L.embedding ↥M ↥N)) K

def first_order.language.amalgamation {L : first_order.language} (K : set (category_theory.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

first_order.language.amalgamation K = ∀ (M N P : category_theory.bundled L.Structure) (MN : L.embedding ↥M ↥N) (MP : L.embedding ↥M ↥P), M ∈ K → N ∈ K → P ∈ K → (∃ (Q : category_theory.bundled L.Structure) (NQ : L.embedding ↥N ↥Q) (PQ : L.embedding ↥P ↥Q), Q ∈ K ∧ NQ.comp MN = PQ.comp MP)

@[class]

structure first_order.language.is_fraisse {L : first_order.language} (K : set (category_theory.bundled L.Structure)) :

Prop

is_nonempty : K.nonempty
fg : ∀ (M : category_theory.bundled L.Structure), M ∈ K → first_order.language.Structure.fg L ↥M
is_equiv_invariant : ∀ (M N : category_theory.bundled L.Structure), nonempty (L.equiv ↥M ↥N) → (M ∈ K ↔ N ∈ K)
is_essentially_countable : (quotient.mk '' K).countable
hereditary : first_order.language.hereditary K
joint_embedding : first_order.language.joint_embedding K
amalgamation : first_order.language.amalgamation K

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.age.is_equiv_invariant (L : first_order.language) (M : Type w) [L.Structure M] (N P : category_theory.bundled L.Structure) (h : nonempty (L.equiv ↥N ↥P)) :

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

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

theorem first_order.language.Structure.fg.mem_age_of_equiv {L : first_order.language} {M N : category_theory.bundled L.Structure} (h : first_order.language.Structure.fg L ↥M) (MN : nonempty (L.equiv ↥M ↥N)) :

N ∈ L.age ↥M

theorem first_order.language.hereditary.is_equiv_invariant_of_fg {L : first_order.language} {K : set (category_theory.bundled L.Structure)} (h : first_order.language.hereditary K) (fg : ∀ (M : category_theory.bundled L.Structure), M ∈ K → first_order.language.Structure.fg L ↥M) (M N : category_theory.bundled L.Structure) (hn : nonempty (L.equiv ↥M ↥N)) :

M ∈ K ↔ N ∈ K

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

(L.age M).nonempty

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

first_order.language.hereditary (L.age M)

theorem first_order.language.age.joint_embedding {L : first_order.language} (M : Type w) [L.Structure M] :

first_order.language.joint_embedding (L.age M)

theorem first_order.language.age.countable_quotient {L : first_order.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).

@[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))] :

L.age (first_order.language.direct_limit 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 first_order.language.exists_cg_is_age_of {L : first_order.language} {K : set (category_theory.bundled L.Structure)} (hn : K.nonempty) (h : ∀ (M N : category_theory.bundled L.Structure), nonempty (L.equiv ↥M ↥N) → (M ∈ K ↔ N ∈ K)) (hc : (quotient.mk '' K).countable) (fg : ∀ (M : category_theory.bundled L.Structure), M ∈ K → first_order.language.Structure.fg L ↥M) (hp : first_order.language.hereditary K) (jep : first_order.language.joint_embedding K) :

∃ (M : category_theory.bundled L.Structure), first_order.language.Structure.cg L ↥M ∧ L.age ↥M = K

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

theorem first_order.language.exists_countable_is_age_of_iff {L : first_order.language} {K : set (category_theory.bundled L.Structure)} [countable (Σ (l : ℕ), L.functions l)] :

(∃ (M : category_theory.bundled L.Structure), countable ↥M ∧ L.age ↥M = K) ↔ K.nonempty ∧ (∀ (M N : category_theory.bundled L.Structure), nonempty (L.equiv ↥M ↥N) → (M ∈ K ↔ N ∈ K)) ∧ (quotient.mk '' K).countable ∧ (∀ (M : category_theory.bundled L.Structure), M ∈ K → first_order.language.Structure.fg L ↥M) ∧ first_order.language.hereditary K ∧ first_order.language.joint_embedding K

def first_order.language.is_ultrahomogeneous (L : first_order.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.is_ultrahomogeneous M = ∀ (S : L.substructure M), S.fg → ∀ (f : L.embedding ↥S M), ∃ (g : L.equiv M M), f = g.to_embedding.comp S.subtype

structure first_order.language.is_fraisse_limit {L : first_order.language} (K : set (category_theory.bundled L.Structure)) (M : Type w) [L.Structure M] [countable (Σ (l : ℕ), L.functions l)] [countable M] :

Prop

ultrahomogeneous : L.is_ultrahomogeneous M
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.

theorem first_order.language.is_ultrahomogeneous.amalgamation_age {L : first_order.language} {M : Type w} [L.Structure M] (h : L.is_ultrahomogeneous M) :

first_order.language.amalgamation (L.age M)

theorem first_order.language.is_ultrahomogeneous.age_is_fraisse {L : first_order.language} {M : Type w} [L.Structure M] [countable M] (h : L.is_ultrahomogeneous M) :

first_order.language.is_fraisse (L.age M)

theorem first_order.language.is_fraisse_limit.is_fraisse {L : first_order.language} (K : set (category_theory.bundled L.Structure)) {M : Type w} [L.Structure M] [countable (Σ (l : ℕ), L.functions l)] [countable M] (h : first_order.language.is_fraisse_limit K M) :

first_order.language.is_fraisse K

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