The realized-spectrum relation is Borel

For a fragment F and an arity n, the realized spectrum of a coded structure c is the set of F-types of its n-tuples, Fragment.realizedSpectrum F n c. Two codes are F,n-spectrum equivalent (SameRealizedSpectrum) when they realize the same spectrum: every tuple of one has a matching tuple in the other, where matching means agreement on every member of the slice. Tuples and the slice are countable, so the relation is a countable combination of Borel satisfaction conditions (measurableSet_sameRealizedSpectrum). No topology on a powerset of types is needed.

Isomorphism refines the relation (sameRealizedSpectrum_of_iso): the pointed-type transport sends tuples to tuples of the same type. The converse is not claimed.

Everything here is below Silver; the dichotomy and the thinness characterization are in Conditional/FragmentSpectrumThin.lean.

Classical background: Marker, Lectures on Infinitary Model Theory (Cambridge, 2016), Corollary 3.3.3, works with the relation of realizing the same fragment types.

theorem FirstOrder.Language.Fragment.slice_countable {L : Language} {F : L.Fragment} (hF : F.toSet.Countable) (n : ℕ) : Countable (F.slice n)

The arity slice of a countable fragment is countable.

def FirstOrder.Language.Fragment.realizedSpectrum {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (c : L.StructureSpace) : Set (F.slice n → Bool)

The realized spectrum of a code at arity n: the F-types of its n-tuples.

Equations

• F.realizedSpectrum n c = Set.range fun (a : Fin n → ℕ) => F.pointedType c a

theorem FirstOrder.Language.Fragment.realizedSpectrum_eq_typeSpectrum_singleton {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (c : L.StructureSpace) : F.realizedSpectrum n c = F.typeSpectrum n {c}

theorem FirstOrder.Language.Fragment.realizedSpectrum_countable {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (c : L.StructureSpace) : (F.realizedSpectrum n c).Countable

def FirstOrder.Language.Fragment.SameRealizedSpectrum {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (c d : L.StructureSpace) : Prop

Spectrum equivalence: the two codes realize the same F-types at arity n.

Equations

• F.SameRealizedSpectrum n c d = (F.realizedSpectrum n c = F.realizedSpectrum n d)

theorem FirstOrder.Language.Fragment.sameRealizedSpectrum_iff {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (c d : L.StructureSpace) : F.SameRealizedSpectrum n c d ↔ (∀ (a : Fin n → ℕ), ∃ (b : Fin n → ℕ), F.pointedType c a = F.pointedType d b) ∧ ∀ (b : Fin n → ℕ), ∃ (a : Fin n → ℕ), F.pointedType d b = F.pointedType c a

Spectrum equivalence, expanded: every tuple of each code has a matching tuple in the other.

theorem FirstOrder.Language.Fragment.sameRealizedSpectrum_refl {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (c : L.StructureSpace) : F.SameRealizedSpectrum n c c

theorem FirstOrder.Language.Fragment.sameRealizedSpectrum_symm {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) {c d : L.StructureSpace} (h : F.SameRealizedSpectrum n c d) : F.SameRealizedSpectrum n d c

theorem FirstOrder.Language.Fragment.sameRealizedSpectrum_trans {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) {c d e : L.StructureSpace} (h₁ : F.SameRealizedSpectrum n c d) (h₂ : F.SameRealizedSpectrum n d e) : F.SameRealizedSpectrum n c e

def FirstOrder.Language.Fragment.sameRealizedSpectrumSetoid {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) : Setoid L.StructureSpace

The spectrum-equivalence setoid.

Equations

• F.sameRealizedSpectrumSetoid n = { r := F.SameRealizedSpectrum n, iseqv := ⋯ }

theorem FirstOrder.Language.Fragment.sameRealizedSpectrum_of_iso {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) {c d : L.StructureSpace} (h : L.structureIsoSetoid c d) : F.SameRealizedSpectrum n c d

Isomorphism refines spectrum equivalence.

Borelness

theorem FirstOrder.Language.Fragment.measurableSet_sameRealizedSpectrum {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (hF : F.toSet.Countable) : MeasurableSet {p : L.StructureSpace × L.StructureSpace | F.SameRealizedSpectrum n p.1 p.2}

Spectrum equivalence is Borel for a countable fragment: countable unions and intersections over tuples of the agreement conditions.