FirstOrder.Language.age_directLimit
theorem FirstOrder.Language.age_directLimit :
∀ {L : FirstOrder.Language} {ι : Type w} [inst : Preorder ι] [inst_1 : IsDirected ι fun x x_1 => x ≤ x_1]
[inst_2 : Nonempty ι] (G : ι → Type (max w w')) [inst_3 : (i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_4 : DirectedSystem G fun i j h => ⇑(f i j h)],
L.age (FirstOrder.Language.DirectLimit G f) = ⋃ i, L.age (G i)
This theorem states that for any first-order language `L` and any type `ι` with a preorder and a directed system of structures `G : ι → Type`, and a directed system of embeddings `f` between these structures, the "age" of the direct limit of these structures is the union of the "ages" of the individual structures. In this context, the "age" of a structure refers to the set of isomorphism types of its finitely generated substructures.
More concisely: For any first-order language `L`, type `ι` with a preorder, and directed systems of structures `G : ι → Type` and embeddings `f : ∀ i j, G i → G j`, the age of the direct limit of `G` is the union of the ages of the individual structures `G i`.
|
FirstOrder.Language.age.countable_quotient
theorem FirstOrder.Language.age.countable_quotient :
∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] [h : Countable M],
(Quotient.mk' '' L.age M).Countable
The theorem `FirstOrder.Language.age.countable_quotient` states that for any first-order language `L` and any type `M` that is a structure for `L` and is countable, the set of equivalence classes (or isomorphism classes) of the age of `M` under the canonical quotient map is countable. Here, the "age" of a structure refers to the set of its finite substructures, up to isomorphism.
More concisely: For any countable first-order language L and countable type M as its structure, the set of equivalence classes of M's finite substructures up to isomorphism is countable.
|
FirstOrder.Language.IsFraisseLimit.isFraisse
theorem FirstOrder.Language.IsFraisseLimit.isFraisse :
∀ {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled L.Structure)) {M : Type w} [inst : L.Structure M]
[inst_1 : Countable ((l : ℕ) × L.Functions l)] [inst_2 : Countable M],
FirstOrder.Language.IsFraisseLimit K M → FirstOrder.Language.IsFraisse K
This theorem states that for any first-order language `L` and any set `K` of structures for `L`, if the type `M` carries a structure for `L` and `M` is countable, along with the set of possible functions from natural numbers `ℕ` to `L`, then if `M` is a Fraïssé limit of the class `K`, it implies that the class `K` is indeed a Fraïssé class. A Fraïssé class is a class of structures satisfying the Fraïssé property, named after the French mathematician Roland Fraïssé, and a Fraïssé limit is a special kind of limit of a Fraïssé class.
More concisely: If `M` is a countable structures carrying a first-order language `L` and is a Fraïssé limit of a class `K` of structures for `L`, then `K` is a Fraïssé class.
|
FirstOrder.Language.exists_cg_is_age_of
theorem FirstOrder.Language.exists_cg_is_age_of :
∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)},
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 → ∃ M, FirstOrder.Language.Structure.CG L ↑M ∧ L.age ↑M = K
This theorem provides sufficient conditions for a class to be the age of a countably-generated structure in the context of first-order languages. Specifically, for any first-order language `L` and a set `K` of `L`-structures, if `K` is nonempty, every pair of `L`-structures `M` and `N` for which there exists an equivalence relation are either both in `K` or both not in `K`, the set of equivalence classes of elements in `K` is countable, every `L`-structure in `K` is finitely-generated, `K` has the hereditary property (meaning that all finitely-generated structures that embed into structures in `K` are also in `K`), and `K` has the joint embedding property (meaning that for every pair of `L`-structures in `K`, there exists another `L`-structure in `K` into which both of the original structures embed), then there exists a countably-generated `L`-structure `M` such that `M` is of age `K`.
More concisely: Given a nonempty set `K` of finitely-generated, embeddable structures in a first-order language `L` satisfying the hereditary and joint embedding properties, and having a countable set of equivalence classes of elements under an equivalence relation where structures related by the relation are either both in `K` or both not in `K`, there exists a countably-generated structure `M` in `L` of age equal to `K`.
|