Polish Space and Borel Space Structure on the Structure Space

This file proves that StructureSpace L is a Polish space, a Borel space, and a standard Borel space when the language has countably many relation symbols.

Strategy

StructureSpace L = RelQuery L → Bool with the product topology. When RelQuery L is countable, Encodable.ofCountable provides an encoding, and Mathlib's instances for products of discrete spaces give:

• CompactSpace, MetrizableSpace, SecondCountableTopology (from Pi.*)
• IsCompletelyMetrizableSpace (compact + metrizable → complete)
• PolishSpace = SecondCountableTopology + IsCompletelyMetrizableSpace
• BorelSpace (product σ-algebra = Borel σ-algebra for second-countable spaces)
• StandardBorelSpace (from PolishSpace + BorelSpace)

Since StructureSpace L is a def (not abbrev), type class resolution cannot see through it. We provide the intermediate instances explicitly.

Main Results

• PolishSpace (StructureSpace L): The structure space is Polish.
• BorelSpace (StructureSpace L): The product σ-algebra equals the Borel σ-algebra.
• StandardBorelSpace (StructureSpace L): The structure space is standard Borel.
• Analogous instances for the pair space StructureSpace L × StructureSpace L.

instance FirstOrder.Language.instSecondCountableTopologyStructureSpace (L : Language) [Countable ((l : ℕ) × L.Relations l)] : SecondCountableTopology L.StructureSpace

instance FirstOrder.Language.instIsCompletelyMetrizableSpaceStructureSpace (L : Language) [Countable ((l : ℕ) × L.Relations l)] : TopologicalSpace.IsCompletelyMetrizableSpace L.StructureSpace

instance FirstOrder.Language.instPolishSpaceStructureSpace (L : Language) [Countable ((l : ℕ) × L.Relations l)] : PolishSpace L.StructureSpace

The structure space is Polish: second-countable and completely metrizable. This follows from StructureSpace L = RelQuery L → Bool being a countable product of finite discrete spaces, hence compact and metrizable.

instance FirstOrder.Language.instBorelSpaceStructureSpace (L : Language) [Countable ((l : ℕ) × L.Relations l)] : BorelSpace L.StructureSpace

The product σ-algebra on the structure space equals the Borel σ-algebra.

instance FirstOrder.Language.instStandardBorelSpaceStructureSpace (L : Language) [Countable ((l : ℕ) × L.Relations l)] : StandardBorelSpace L.StructureSpace

The structure space is standard Borel (Polish + Borel).