Topology of relational configurations

The product topology on relational configurations is compact Hausdorff, and relabelling by a permutation of the carrier is continuous. Restriction along a vertex map is continuous, and jointly continuous in the vertex map when the target carrier is discrete. Specifying an atom's truth value gives a clopen, measurable cylinder. On countable carriers in countable relational vocabularies the topology is Polish and its Borel σ-algebra is the existing product σ-algebra. The same construction handles finite and empty carriers.

These are the usual spaces of structures used for the logic action; see Gao, Invariant Descriptive Set Theory. The measurable coordinates and encoding of structures are those of TauCeti.RelationalConfiguration; no second space of Boolean codes is introduced.

@[instance_reducible]

instance TauCeti.RelationalConfiguration.instTopologicalSpace {L : FirstOrder.Language} {V : Type u_1} : TopologicalSpace (RelationalConfiguration L V)

instance TauCeti.RelationalConfiguration.instCompactSpace {L : FirstOrder.Language} {V : Type u_1} : CompactSpace (RelationalConfiguration L V)

instance TauCeti.RelationalConfiguration.instT2Space {L : FirstOrder.Language} {V : Type u_1} : T2Space (RelationalConfiguration L V)

theorem TauCeti.RelationalConfiguration.continuous_eval {L : FirstOrder.Language} {V : Type u_1} (a : Atom L V) : Continuous fun (c : RelationalConfiguration L V) => c.eval a

Reading one atom is continuous.

theorem TauCeti.RelationalConfiguration.continuous_iff {L : FirstOrder.Language} {V : Type u_1} {X : Type u_2} [TopologicalSpace X] {f : X → RelationalConfiguration L V} : Continuous f ↔ ∀ (a : Atom L V), Continuous fun (x : X) => (f x).eval a

Continuity into configurations is equivalent to continuity of every atom coordinate.

theorem TauCeti.RelationalConfiguration.continuous_mk {L : FirstOrder.Language} {V : Type u_1} : Continuous mk

Building a configuration from its atom values is continuous.

theorem TauCeti.RelationalConfiguration.continuous_restrict {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} (f : V → W) : Continuous (restrict f)

Restricting along a vertex map is continuous.

theorem TauCeti.RelationalConfiguration.continuous_uncurry_restrict {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} [TopologicalSpace W] [DiscreteTopology W] : Continuous (Function.uncurry restrict)

Restriction is jointly continuous in the vertex map and the configuration when the target carrier is discrete.

instance TauCeti.RelationalConfiguration.instContinuousConstSMulPerm {L : FirstOrder.Language} {V : Type u_1} : ContinuousConstSMul (Equiv.Perm V) (RelationalConfiguration L V)

Each relabelling by a permutation of the carrier is continuous.

theorem TauCeti.RelationalConfiguration.isClopen_setOf_eval {L : FirstOrder.Language} {V : Type u_1} (a : Atom L V) (b : Bool) : IsClopen {c : RelationalConfiguration L V | c.eval a = b}

The configurations giving a fixed answer to one atom form a clopen cylinder.

instance TauCeti.RelationalConfiguration.instSecondCountableTopologyOfRelationsOfCountable {L : FirstOrder.Language} {V : Type u_1} [∀ (n : ℕ), Countable (L.Relations n)] [Countable V] : SecondCountableTopology (RelationalConfiguration L V)

instance TauCeti.RelationalConfiguration.instPolishSpaceOfRelationsOfCountable {L : FirstOrder.Language} {V : Type u_1} [∀ (n : ℕ), Countable (L.Relations n)] [Countable V] : PolishSpace (RelationalConfiguration L V)

instance TauCeti.RelationalConfiguration.instBorelSpaceOfRelationsOfCountable {L : FirstOrder.Language} {V : Type u_1} [∀ (n : ℕ), Countable (L.Relations n)] [Countable V] : BorelSpace (RelationalConfiguration L V)

theorem TauCeti.RelationalConfiguration.mk_le_continuum (L : FirstOrder.Language) (V : Type u_2) [∀ (n : ℕ), Countable (L.Relations n)] [Countable V] : Cardinal.mk (RelationalConfiguration L V) ≤ Cardinal.continuum

There are at most continuum many configurations on a countable carrier in a countable relational vocabulary. Function symbols play no role.