Morleyization on coded structures

The first coded endpoint: a countable relational base L and a countable family Φ.

• morleyCode Φ : StructureSpace L → StructureSpace (L.morleyize Φ) sends a code to the code of the canonical expansion of its structure: base coordinates are copied, and the coordinate of a defined symbol at a tuple is the truth of the named formula there.
• toStructure_morleyCode: the decoded structure of the expansion code is the canonical expansion of the decoded structure.
• measurable_morleyCode: the map is Borel (base coordinates are projections, defined coordinates are modelsOfBounded_measurableSet); morleyCode_injective: the reduct recovers the code. Hence measurableEmbedding_morleyCode (Lusin–Souslin, through Measurable.measurableEmbedding) and Borel images of Borel classes (measurableSet_image_morleyCode).
• range_morleyCode: the image is exactly the class of expansion codes satisfying the defining theory, by uniqueness of expansions satisfying it.
• morleyCode_iso_iff: two expansion codes are isomorphic iff the base codes are — the classification boundary, from nonempty_morleyEquiv_iff.

Borel, not necessarily continuous: a defined coordinate is the truth of an infinitary formula. The fragment logic topology is a separate construction.

instance FirstOrder.Language.morleyize_countable_relations {L : Language} [Countable ((l : ℕ) × L.Relations l)] (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) [Countable ↑Φ] : Countable ((n : ℕ) × (L.morleyize Φ).Relations n)

The defined symbols of a countable family form a countable sigma type.

noncomputable def FirstOrder.Language.morleyCode {L : Language} [L.IsRelational] (Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) (c : L.StructureSpace) : (L.morleyize Φ).StructureSpace

The expansion code: base coordinates copied, defined coordinates by truth.

Equations

• FirstOrder.Language.morleyCode Φ c ⟨⟨n, Sum.inl R⟩, v⟩ = c ⟨⟨n, R⟩, v⟩
• FirstOrder.Language.morleyCode Φ c ⟨⟨fst, Sum.inr φ⟩, v⟩ = decide (c ∈ FirstOrder.Language.ModelsOfBounded (↑φ) Empty.elim v)

theorem FirstOrder.Language.morleyCode_inl {L : Language} [L.IsRelational] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (c : L.StructureSpace) {n : ℕ} (R : L.Relations n) (v : Fin n → ℕ) : morleyCode Φ c ⟨⟨n, Sum.inl R⟩, v⟩ = c ⟨⟨n, R⟩, v⟩

theorem FirstOrder.Language.morleyCode_inr {L : Language} [L.IsRelational] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (c : L.StructureSpace) {n : ℕ} (φ : DefinedSym Φ n) (v : Fin n → ℕ) : morleyCode Φ c ⟨⟨n, Sum.inr φ⟩, v⟩ = true ↔ c ∈ ModelsOfBounded (↑φ) Empty.elim v

theorem FirstOrder.Language.toStructure_morleyCode {L : Language} [L.IsRelational] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (c : L.StructureSpace) : (morleyCode Φ c).toStructure = morleyExpansion Φ ℕ

The decoded expansion code is the canonical expansion of the decoded base code.

Borel, injective, and the image

theorem FirstOrder.Language.measurable_morleyCode {L : Language} [L.IsRelational] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} : Measurable (morleyCode Φ)

The expansion code is Borel: base coordinates are projections, defined coordinates are formula satisfaction.

theorem FirstOrder.Language.morleyCode_injective {L : Language} [L.IsRelational] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} : Function.Injective (morleyCode Φ)

The expansion code is injective: the base coordinates recover the code.

theorem FirstOrder.Language.measurableEmbedding_morleyCode {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} [Countable ↑Φ] : MeasurableEmbedding (morleyCode Φ)

Lusin–Souslin: the expansion code is a measurable embedding.

theorem FirstOrder.Language.measurableSet_image_morleyCode {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} [Countable ↑Φ] {C : Set L.StructureSpace} (hC : MeasurableSet C) : MeasurableSet (morleyCode Φ '' C)

Borel images: the expansion code sends Borel classes to Borel classes.

def FirstOrder.Language.reductCode {L : Language} {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (d : (L.morleyize Φ).StructureSpace) : L.StructureSpace

The base reduct of an expansion code: drop the defined coordinates.

Equations

• FirstOrder.Language.reductCode d q = d ⟨⟨q.fst.fst, Sum.inl q.fst.snd⟩, q.snd⟩

theorem FirstOrder.Language.reductCode_morleyCode {L : Language} [L.IsRelational] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (c : L.StructureSpace) : reductCode (morleyCode Φ c) = c

theorem FirstOrder.Language.isExpansionOn_toStructure_reductCode {L : Language} [L.IsRelational] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (d : (L.morleyize Φ).StructureSpace) : (lhomMorleyize Φ).IsExpansionOn ℕ

The decoded expansion code is an expansion of its decoded reduct along the inclusion.

theorem FirstOrder.Language.range_morleyCode {L : Language} [L.IsRelational] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} : Set.range (morleyCode Φ) = {d : (L.morleyize Φ).StructureSpace | (definingTheory Φ).Model ℕ}

The image is the class of expansion codes satisfying the defining theory.

theorem FirstOrder.Language.morleyCode_iso_iff {L : Language} [L.IsRelational] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (c d : L.StructureSpace) : (L.morleyize Φ).structureIsoSetoid (morleyCode Φ c) (morleyCode Φ d) ↔ L.structureIsoSetoid c d

The classification boundary: expansion codes are isomorphic iff the base codes are.