Isomorphism of relational configurations

For a relational language L, two configurations on a carrier V are isomorphic when the structures they decode to are isomorphic. This is the equivalence relation whose classes are counted when one counts the models of a sentence on a fixed carrier.

Relabelling a configuration by a permutation of V transports its decoded structure along that permutation, and every isomorphism of decoded structures is such a relabelling. So isomorphism is the orbit relation of the action of Equiv.Perm V, the logic action, on every carrier, finite or infinite. Structures on different carriers, transported to V with Equiv.encodeVia, are isomorphic exactly when their encodings are.

On a finite carrier the permutation group is finite and acts continuously, so the graph of isomorphism is a finite union of graphs of continuous maps. It is therefore closed, and Borel in a countable relational vocabulary. On a countable carrier, in a countable relational vocabulary, the graph of isomorphism is analytic: a permutation is a pair of mutually inverse self-maps of the carrier, these pairs form a closed subset of a Polish space, and relabelling is jointly continuous. Hence the saturation of an analytic set under the logic action is analytic.

A set of configurations is isomorphism invariant when it contains every configuration isomorphic to one of its members. Equivalently, every permutation of the carrier maps it into itself (Mathlib's MulAction.IsInvariantBlock for the logic action), or it equals its saturation Quotient.mk _ ⁻¹' (Quotient.mk _ '' A) under isomorphism.

Main definitions

• TauCeti.RelationalConfiguration.isoSetoid L V — isomorphism of decoded structures, as a setoid on the configurations on V.
• TauCeti.RelationalConfiguration.IsomorphismInvariant — a set of configurations closed under isomorphism.

Main results

• TauCeti.RelationalConfiguration.isoSetoid_iff_exists_perm_smul_eq and TauCeti.RelationalConfiguration.isoSetoid_eq_orbitRel — isomorphism is the orbit relation of the relabelling action of Equiv.Perm V;
• Equiv.isoSetoid_encodeVia_iff — encodings of two structures on a common carrier are isomorphic exactly when the structures are;
• TauCeti.RelationalConfiguration.isClosed_setOf_isoSetoid and TauCeti.RelationalConfiguration.measurableSet_setOf_isoSetoid — on a finite carrier the graph of isomorphism is closed and Borel;
• TauCeti.RelationalConfiguration.analyticSet_setOf_isoSetoid — on a countable carrier the graph of isomorphism is analytic;
• TauCeti.RelationalConfiguration.isomorphismInvariant_iff_isInvariantBlock and TauCeti.RelationalConfiguration.isomorphismInvariant_iff_preimage_image_quotientMk — isomorphism invariance is invariance under the logic action, and is equality with the saturation;
• TauCeti.RelationalConfiguration.analyticSet_iUnion_smul — on a countable carrier the saturation of an analytic set under the logic action is analytic.

References

• Su Gao, Invariant Descriptive Set Theory, the logic action of the permutation group on the space of countable structures.
• Alexander S. Kechris, Classical Descriptive Set Theory.

def TauCeti.RelationalConfiguration.isoSetoid (L : FirstOrder.Language) [L.IsRelational] (V : Type w) : Setoid (RelationalConfiguration L V)

Isomorphism of decoded structures, as a setoid on the configurations on V: two configurations are related when the structures they decode to are isomorphic.

theorem TauCeti.RelationalConfiguration.isoSetoid_apply {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {c d : RelationalConfiguration L V} : (isoSetoid L V) c d ↔ Nonempty (L.Equiv V V)

Two configurations are isomorphic exactly when their decoded structures are.

theorem TauCeti.RelationalConfiguration.perm_smul_eq_encodeVia {L : FirstOrder.Language} [L.IsRelational] {V : Type w} (σ : Equiv.Perm V) (c : RelationalConfiguration L V) : σ • c = Equiv.encodeVia σ

Relabelling by σ encodes the decoded structure transported along σ.

@[simp]

theorem TauCeti.RelationalConfiguration.toStructure_perm_smul {L : FirstOrder.Language} [L.IsRelational] {V : Type w} (σ : Equiv.Perm V) (c : RelationalConfiguration L V) : (σ • c).toStructure = Equiv.inducedStructure σ

Relabelling by σ decodes to the structure transported along σ.

theorem TauCeti.RelationalConfiguration.isoSetoid_perm_smul {L : FirstOrder.Language} [L.IsRelational] {V : Type w} (σ : Equiv.Perm V) (c : RelationalConfiguration L V) : (isoSetoid L V) c (σ • c)

A relabelled configuration is isomorphic to the original one.

theorem TauCeti.RelationalConfiguration.isoSetoid_iff_exists_perm_smul_eq {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {c d : RelationalConfiguration L V} : (isoSetoid L V) c d ↔ ∃ (σ : Equiv.Perm V), σ • c = d

Isomorphism of configurations is relabelling by a permutation of the carrier.

theorem TauCeti.RelationalConfiguration.isoSetoid_eq_orbitRel {L : FirstOrder.Language} [L.IsRelational] {V : Type w} : isoSetoid L V = MulAction.orbitRel (Equiv.Perm V) (RelationalConfiguration L V)

The logic action. Isomorphism of configurations is the orbit relation of the relabelling action of the permutations of the carrier.

theorem Equiv.isoSetoid_encodeVia_iff {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {M : Type w'} {N : Type w''} [L.Structure M] [L.Structure N] (e : M ≃ V) (f : N ≃ V) : (TauCeti.RelationalConfiguration.isoSetoid L V) e.encodeVia f.encodeVia ↔ Nonempty (L.Equiv M N)

Structures transported to a common carrier have isomorphic encodings exactly when they are isomorphic, whatever their universes.

theorem TauCeti.RelationalConfiguration.isClosed_setOf_isoSetoid {L : FirstOrder.Language} [L.IsRelational] {V : Type w} [Finite V] : IsClosed {p : RelationalConfiguration L V × RelationalConfiguration L V | (isoSetoid L V) p.1 p.2}

On a finite carrier the graph of isomorphism is closed: it is the union of the graphs of the finitely many relabellings, each continuous.

theorem TauCeti.RelationalConfiguration.measurableSet_setOf_isoSetoid {L : FirstOrder.Language} [L.IsRelational] {V : Type w} [∀ (n : ℕ), Countable (L.Relations n)] [Finite V] : MeasurableSet {p : RelationalConfiguration L V × RelationalConfiguration L V | (isoSetoid L V) p.1 p.2}

On a finite carrier, in a countable relational vocabulary, the graph of isomorphism is Borel.

theorem TauCeti.RelationalConfiguration.analyticSet_setOf_isoSetoid {L : FirstOrder.Language} [L.IsRelational] {V : Type w} [∀ (n : ℕ), Countable (L.Relations n)] [Countable V] : MeasureTheory.AnalyticSet {p : RelationalConfiguration L V × RelationalConfiguration L V | (isoSetoid L V) p.1 p.2}

On a countable carrier, in a countable relational vocabulary, the graph of isomorphism is analytic.

Isomorphism-invariant sets

def TauCeti.RelationalConfiguration.IsomorphismInvariant {L : FirstOrder.Language} [L.IsRelational] {V : Type w} (A : Set (RelationalConfiguration L V)) : Prop

A set of configurations is isomorphism invariant when it contains every configuration isomorphic to one of its members.

theorem TauCeti.RelationalConfiguration.isomorphismInvariant_iff {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {A : Set (RelationalConfiguration L V)} : IsomorphismInvariant A ↔ ∀ ⦃c d : RelationalConfiguration L V⦄, (isoSetoid L V) c d → c ∈ A → d ∈ A

Unfolding lemma for IsomorphismInvariant.

theorem TauCeti.RelationalConfiguration.IsomorphismInvariant.mem_iff {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {A : Set (RelationalConfiguration L V)} (hA : IsomorphismInvariant A) {c d : RelationalConfiguration L V} (h : (isoSetoid L V) c d) : c ∈ A ↔ d ∈ A

Isomorphic configurations lie in the same isomorphism-invariant sets.

theorem TauCeti.RelationalConfiguration.isomorphismInvariant_iff_isInvariantBlock {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {A : Set (RelationalConfiguration L V)} : IsomorphismInvariant A ↔ MulAction.IsInvariantBlock (Equiv.Perm V) A

Isomorphism invariance is invariance under the logic action: a set of configurations is isomorphism invariant exactly when every permutation of the carrier maps it into itself.

theorem TauCeti.RelationalConfiguration.preimage_image_quotientMk_eq_iUnion_smul {L : FirstOrder.Language} [L.IsRelational] {V : Type w} (A : Set (RelationalConfiguration L V)) : Quotient.mk (isoSetoid L V) ⁻¹' Quotient.mk (isoSetoid L V) '' A = ⋃ (σ : Equiv.Perm V), σ • A

The saturation of a set under isomorphism is the union of its images under the logic action.

theorem TauCeti.RelationalConfiguration.isomorphismInvariant_preimage_quotientMk {L : FirstOrder.Language} [L.IsRelational] {V : Type w} (s : Set (Quotient (isoSetoid L V))) : IsomorphismInvariant (Quotient.mk (isoSetoid L V) ⁻¹' s)

The preimage of any set of isomorphism classes is isomorphism invariant.

theorem TauCeti.RelationalConfiguration.isomorphismInvariant_iff_preimage_image_quotientMk {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {A : Set (RelationalConfiguration L V)} : IsomorphismInvariant A ↔ Quotient.mk (isoSetoid L V) ⁻¹' Quotient.mk (isoSetoid L V) '' A = A

A set is isomorphism invariant exactly when it is its own saturation under isomorphism.

theorem TauCeti.RelationalConfiguration.isomorphismInvariant_iUnion_smul {L : FirstOrder.Language} [L.IsRelational] {V : Type w} (A : Set (RelationalConfiguration L V)) : IsomorphismInvariant (⋃ (σ : Equiv.Perm V), σ • A)

The union of the images of a set under the logic action is isomorphism invariant.

@[simp]

theorem TauCeti.RelationalConfiguration.isomorphismInvariant_empty {L : FirstOrder.Language} [L.IsRelational] {V : Type w} : IsomorphismInvariant ∅

The empty set is isomorphism invariant.

@[simp]

theorem TauCeti.RelationalConfiguration.isomorphismInvariant_univ {L : FirstOrder.Language} [L.IsRelational] {V : Type w} : IsomorphismInvariant Set.univ

The set of all configurations is isomorphism invariant.

theorem TauCeti.RelationalConfiguration.IsomorphismInvariant.compl {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {A : Set (RelationalConfiguration L V)} (hA : IsomorphismInvariant A) : IsomorphismInvariant Aᶜ

The complement of an isomorphism-invariant set is isomorphism invariant.

theorem TauCeti.RelationalConfiguration.IsomorphismInvariant.inter {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {A B : Set (RelationalConfiguration L V)} (hA : IsomorphismInvariant A) (hB : IsomorphismInvariant B) : IsomorphismInvariant (A ∩ B)

The intersection of two isomorphism-invariant sets is isomorphism invariant.

theorem TauCeti.RelationalConfiguration.IsomorphismInvariant.union {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {A B : Set (RelationalConfiguration L V)} (hA : IsomorphismInvariant A) (hB : IsomorphismInvariant B) : IsomorphismInvariant (A ∪ B)

The union of two isomorphism-invariant sets is isomorphism invariant.

theorem TauCeti.RelationalConfiguration.isomorphismInvariant_iInter {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Sort u_1} {A : ι → Set (RelationalConfiguration L V)} (hA : ∀ (i : ι), IsomorphismInvariant (A i)) : IsomorphismInvariant (⋂ (i : ι), A i)

An intersection of isomorphism-invariant sets is isomorphism invariant.

theorem TauCeti.RelationalConfiguration.isomorphismInvariant_iUnion {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Sort u_1} {A : ι → Set (RelationalConfiguration L V)} (hA : ∀ (i : ι), IsomorphismInvariant (A i)) : IsomorphismInvariant (⋃ (i : ι), A i)

A union of isomorphism-invariant sets is isomorphism invariant.

theorem TauCeti.RelationalConfiguration.analyticSet_iUnion_smul {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {A : Set (RelationalConfiguration L V)} [∀ (n : ℕ), Countable (L.Relations n)] [Countable V] (hA : MeasureTheory.AnalyticSet A) : MeasureTheory.AnalyticSet (⋃ (σ : Equiv.Perm V), σ • A)

On a countable carrier, in a countable relational vocabulary, the saturation of an analytic set of configurations under the logic action is analytic.