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.

noncomputable instance FirstOrder.Language.instEncodableRelQueryOn (L : Language) [Countable ((l : ℕ) × L.Relations l)] (α : Type u_1) [Encodable α] : Encodable (L.RelQueryOn α)

Equations

• L.instEncodableRelQueryOn α = Encodable.ofCountable (L.RelQueryOn α)

instance FirstOrder.Language.instCompactSpaceStructureSpaceOn (L : Language) (α : Type u_1) : CompactSpace (L.StructureSpaceOn α)

instance FirstOrder.Language.instMetrizableSpaceStructureSpaceOn (L : Language) [Countable ((l : ℕ) × L.Relations l)] (α : Type u_1) [Encodable α] : TopologicalSpace.MetrizableSpace (L.StructureSpaceOn α)

instance FirstOrder.Language.instSecondCountableTopologyStructureSpaceOn (L : Language) [Countable ((l : ℕ) × L.Relations l)] (α : Type u_1) [Encodable α] : SecondCountableTopology (L.StructureSpaceOn α)

instance FirstOrder.Language.instIsCompletelyMetrizableSpaceStructureSpaceOn (L : Language) [Countable ((l : ℕ) × L.Relations l)] (α : Type u_1) [Encodable α] : TopologicalSpace.IsCompletelyMetrizableSpace (L.StructureSpaceOn α)

instance FirstOrder.Language.instPolishSpaceStructureSpaceOn (L : Language) [Countable ((l : ℕ) × L.Relations l)] (α : Type u_1) [Encodable α] : PolishSpace (L.StructureSpaceOn α)

instance FirstOrder.Language.instBorelSpaceStructureSpaceOn (L : Language) [Countable ((l : ℕ) × L.Relations l)] (α : Type u_1) [Encodable α] : BorelSpace (L.StructureSpaceOn α)

instance FirstOrder.Language.instStandardBorelSpaceStructureSpaceOn (L : Language) [Countable ((l : ℕ) × L.Relations l)] (α : Type u_1) [Encodable α] : StandardBorelSpace (L.StructureSpaceOn α)

instance FirstOrder.Language.instPolishSpaceStructurePairSpaceOn (L : Language) [Countable ((l : ℕ) × L.Relations l)] (α : Type u_1) [Encodable α] : PolishSpace (L.StructurePairSpaceOn α)

instance FirstOrder.Language.instBorelSpaceStructurePairSpaceOn (L : Language) [Countable ((l : ℕ) × L.Relations l)] (α : Type u_1) [Encodable α] : BorelSpace (L.StructurePairSpaceOn α)

instance FirstOrder.Language.instStandardBorelSpaceStructurePairSpaceOn (L : Language) [Countable ((l : ℕ) × L.Relations l)] (α : Type u_1) [Encodable α] : StandardBorelSpace (L.StructurePairSpaceOn α)

noncomputable instance FirstOrder.Language.instEncodableRelQuery (L : Language) [Countable ((l : ℕ) × L.Relations l)] : Encodable L.RelQuery

RelQuery L is encodable when the language has countably many relation symbols. This is the key ingredient for all topological instances.

Equations

• L.instEncodableRelQuery = Encodable.ofCountable L.RelQuery

instance FirstOrder.Language.instCompactSpaceStructureSpace (L : Language) : CompactSpace L.StructureSpace

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

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).

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

The pair space StructureSpace L × StructureSpace L is Polish.

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

The pair space is Borel.

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

The pair space is standard Borel.