Relational configurations

A relational configuration on a vertex type V interprets the relational part of a one-sorted first-order language L: it is a truth value for every atom R(v₁, …, vₙ), an n-ary relation symbol of L together with an n-tuple of vertices. Tuple entries may repeat, so a configuration also records the value of R(v, v) and the like; nothing here assumes distinct coordinates.

Configurations carry the product σ-algebra, with one Boolean coordinate per atom. Pulling a configuration back along a map of vertex types f : V → W reads each atom of V at its image atom of W. This restriction is measurable and functorial: restriction along the identity is the identity, and restriction along a composite is the composite of the restrictions in the opposite order.

Functoriality makes restriction along inverses a left action of the permutations of V by relabelling vertices, and each permutation acts measurably. Over the vertex set ℕ, the finitely supported permutations TauCeti.FinitaryPerm act in the same way; this is the action under which laws of random structures on ℕ are invariant or ergodic.

The function symbols of L are permitted and play no role. A structure of L determines a configuration by deciding its relations (ofStructure).

Main definitions

• TauCeti.RelationalConfiguration.Atom L V — a relation symbol of L with a tuple of vertices;
• TauCeti.RelationalConfiguration L V — a truth value for every atom;
• TauCeti.RelationalConfiguration.restrict — pulling a configuration back along a vertex map;
• FirstOrder.Language.LHom.onAtom — renaming the relation symbol of an atom along a language map;
• TauCeti.RelationalConfiguration.instMulActionPerm — permutations of V relabel configurations on V;
• TauCeti.RelationalConfiguration.instMulActionFinitaryPerm — finitely supported permutations of ℕ relabel configurations over ℕ;
• TauCeti.RelationalConfiguration.ofStructure — the configuration of an L-structure.

Main results

• TauCeti.RelationalConfiguration.measurable_iff — a map into configurations is measurable exactly when each atom coordinate is;
• TauCeti.RelationalConfiguration.measurable_restrict — restriction is measurable;
• TauCeti.RelationalConfiguration.restrict_id and TauCeti.RelationalConfiguration.restrict_comp — restriction is functorial;
• TauCeti.RelationalConfiguration.instMeasurableConstSMulPerm and TauCeti.RelationalConfiguration.instMeasurableConstSMulFinitaryPerm — each relabelling is measurable.

def TauCeti.RelationalConfiguration.Atom (L : FirstOrder.Language) (V : Type u_1) : Type (max u_1 u_3)

An atom of the language L over the vertex type V: an n-ary relation symbol together with an n-tuple of vertices, whose entries may repeat.

def TauCeti.RelationalConfiguration (L : FirstOrder.Language) (V : Type u_1) : Type (max u_1 u_3)

A relational configuration of L on V: a truth value for every atom.

Atoms

def TauCeti.RelationalConfiguration.atom {L : FirstOrder.Language} {V : Type u_1} {n : ℕ} (R : L.Relations n) (x : Fin n → V) : Atom L V

The atom with relation symbol R and argument tuple x.

theorem TauCeti.RelationalConfiguration.Atom.induction_atom {L : FirstOrder.Language} {V : Type u_1} {motive : Atom L V → Prop} (h : ∀ {n : ℕ} (R : L.Relations n) (x : Fin n → V), motive (atom R x)) (a : Atom L V) : motive a

Every atom is atom R x for its relation symbol and tuple.

def TauCeti.RelationalConfiguration.Atom.map {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} (f : V → W) (a : Atom L V) : Atom L W

Relabel the arguments of an atom along a vertex map.

@[simp]

theorem TauCeti.RelationalConfiguration.Atom.map_atom {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} (f : V → W) {n : ℕ} (R : L.Relations n) (x : Fin n → V) : map f (atom R x) = atom R (f ∘ x)

@[simp]

theorem TauCeti.RelationalConfiguration.Atom.map_id {L : FirstOrder.Language} {V : Type u_1} (a : Atom L V) : map id a = a

theorem TauCeti.RelationalConfiguration.Atom.map_comp {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} {X : Type u_3} (g : W → X) (f : V → W) (a : Atom L V) : map (g ∘ f) a = map g (map f a)

def FirstOrder.Language.LHom.onAtom {L : Language} {V : Type u_1} {L' : Language} (g : L →ᴸ L') (a : TauCeti.RelationalConfiguration.Atom L V) : TauCeti.RelationalConfiguration.Atom L' V

Rename the relation symbol of an atom along a language map, keeping its arguments.

@[simp]

theorem FirstOrder.Language.LHom.onAtom_atom {L : Language} {V : Type u_1} {L' : Language} (g : L →ᴸ L') {n : ℕ} (R : L.Relations n) (x : Fin n → V) : g.onAtom (TauCeti.RelationalConfiguration.atom R x) = TauCeti.RelationalConfiguration.atom (g.onRelation R) x

theorem FirstOrder.Language.LHom.onAtom_map {L : Language} {V : Type u_1} {W : Type u_2} {L' : Language} (g : L →ᴸ L') (f : V → W) (a : TauCeti.RelationalConfiguration.Atom L V) : g.onAtom (TauCeti.RelationalConfiguration.Atom.map f a) = TauCeti.RelationalConfiguration.Atom.map f (g.onAtom a)

Renaming the relation symbol of an atom commutes with relabelling its arguments.

@[simp]

theorem FirstOrder.Language.LHom.id_onAtom {L : Language} {V : Type u_1} (a : TauCeti.RelationalConfiguration.Atom L V) : (LHom.id L).onAtom a = a

theorem FirstOrder.Language.LHom.comp_onAtom {L : Language} {V : Type u_1} {L' : Language} {L'' : Language} (g : L' →ᴸ L'') (f : L →ᴸ L') (a : TauCeti.RelationalConfiguration.Atom L V) : (g.comp f).onAtom a = g.onAtom (f.onAtom a)

theorem TauCeti.RelationalConfiguration.Atom.exists_forall_map_val {L : FirstOrder.Language} (J : Finset (Atom L ℕ)) : ∃ (n : ℕ), ∀ a ∈ J, ∃ (b : Atom L (Fin n)), map Fin.val b = a

Every finite set of atoms over ℕ has its vertices below some bound n, so its atoms are relabelled from atoms of Fin n.

Configurations

def TauCeti.RelationalConfiguration.eval {L : FirstOrder.Language} {V : Type u_1} (c : RelationalConfiguration L V) (a : Atom L V) : Bool

The value of a configuration at the atom R(x).

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

Evaluation reads the underlying Boolean function at an atom.

def TauCeti.RelationalConfiguration.mk {L : FirstOrder.Language} {V : Type u_1} (c : Atom L V → Bool) : RelationalConfiguration L V

Build a configuration from its value at every atom. A bare function on atoms only unfolds to a configuration, so this gives it the configuration type, with eval_mk to rewrite with.

@[simp]

theorem TauCeti.RelationalConfiguration.eval_mk {L : FirstOrder.Language} {V : Type u_1} (c : Atom L V → Bool) (a : Atom L V) : (mk c).eval a = c a

theorem TauCeti.RelationalConfiguration.ext {L : FirstOrder.Language} {V : Type u_1} {c d : RelationalConfiguration L V} (h : ∀ (a : Atom L V), c.eval a = d.eval a) : c = d

Configurations are determined by their values at atoms.

theorem TauCeti.RelationalConfiguration.ext_iff {L : FirstOrder.Language} {V : Type u_1} {c d : RelationalConfiguration L V} : c = d ↔ ∀ (a : Atom L V), c.eval a = d.eval a

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

A language with countably many relation symbols of each arity has countably many atoms over a countable vertex type.

@[instance_reducible]

instance TauCeti.RelationalConfiguration.instMeasurableSpace {L : FirstOrder.Language} {V : Type u_1} : MeasurableSpace (RelationalConfiguration L V)

Configurations carry the product σ-algebra, one Boolean coordinate per atom.

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

Reading off one atom is measurable.

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

Cylinders are measurable even when the language or carrier is uncountable.

theorem TauCeti.RelationalConfiguration.measurable_mk {L : FirstOrder.Language} {V : Type u_1} : Measurable mk

Building a configuration from its values at atoms is measurable.

theorem TauCeti.RelationalConfiguration.measurable_iff {L : FirstOrder.Language} {V : Type u_1} {Ω : Type u_4} [MeasurableSpace Ω] {F : Ω → RelationalConfiguration L V} : Measurable F ↔ ∀ (a : Atom L V), Measurable fun (ω : Ω) => (F ω).eval a

A map into configurations is measurable exactly when each atom coordinate is.

Restriction

def TauCeti.RelationalConfiguration.restrict {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} (f : V → W) (c : RelationalConfiguration L W) : RelationalConfiguration L V

Pull a configuration back along a vertex map: the atom R(x) of V takes the value of the atom R(f ∘ x) of W.

@[simp]

theorem TauCeti.RelationalConfiguration.eval_restrict {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} (f : V → W) (c : RelationalConfiguration L W) (a : Atom L V) : (restrict f c).eval a = c.eval (Atom.map f a)

@[simp]

theorem TauCeti.RelationalConfiguration.restrict_id {L : FirstOrder.Language} {V : Type u_1} (c : RelationalConfiguration L V) : restrict id c = c

theorem TauCeti.RelationalConfiguration.restrict_comp {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} {X : Type u_3} (g : W → X) (f : V → W) (c : RelationalConfiguration L X) : restrict (g ∘ f) c = restrict f (restrict g c)

Restriction along a composite is the composite of the restrictions, in the opposite order.

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

Restriction is measurable: each atom coordinate of the restriction is an atom coordinate of the source.

Extension by false

theorem TauCeti.RelationalConfiguration.Atom.map_injective {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} {f : V → W} (hf : Function.Injective f) : Function.Injective (map f)

Relabelling atoms along an injective vertex map is injective.

noncomputable def TauCeti.RelationalConfiguration.extend {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} (f : V → W) (c : RelationalConfiguration L V) : RelationalConfiguration L W

Extend a configuration along a vertex map f : V → W: an atom of W relabelled from an atom of V takes the value of such an atom, and every other atom is false. Along an injective map the relabelled atom is unique (eval_extend_map), so restriction undoes extension (restrict_extend).

theorem TauCeti.RelationalConfiguration.eval_extend {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} (f : V → W) (c : RelationalConfiguration L V) (a : Atom L W) : (extend f c).eval a = Function.extend (Atom.map f) c.eval (fun (x : Atom L W) => false) a

The value of an extension at an atom, through Function.extend.

@[simp]

theorem TauCeti.RelationalConfiguration.eval_extend_map {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} {f : V → W} (hf : Function.Injective f) (c : RelationalConfiguration L V) (a : Atom L V) : (extend f c).eval (Atom.map f a) = c.eval a

Along an injective map, the relabelled atom R(f ∘ x) of the extension takes the value of the atom R(x).

theorem TauCeti.RelationalConfiguration.eval_extend_of_forall_ne {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} {f : V → W} (c : RelationalConfiguration L V) {a : Atom L W} (ha : ∀ (b : Atom L V), Atom.map f b ≠ a) : (extend f c).eval a = false

An atom of W that is not relabelled from an atom of V is false in the extension.

@[simp]

theorem TauCeti.RelationalConfiguration.restrict_extend {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} {f : V → W} (hf : Function.Injective f) (c : RelationalConfiguration L V) : restrict f (extend f c) = c

Along an injective map, restriction undoes extension.

theorem TauCeti.RelationalConfiguration.measurable_extend {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} (f : V → W) : Measurable (extend f)

Extension is measurable: each atom coordinate of the extension is an atom coordinate of the source or constantly false.

Configurations of structures

noncomputable def TauCeti.RelationalConfiguration.ofStructure (L : FirstOrder.Language) (V : Type u_4) [L.Structure V] : RelationalConfiguration L V

The configuration of an L-structure: an atom holds exactly when its relation does.

@[simp]

theorem TauCeti.RelationalConfiguration.eval_ofStructure {L : FirstOrder.Language} {V : Type u_1} [L.Structure V] {n : ℕ} (R : L.Relations n) (x : Fin n → V) : (ofStructure L V).eval (atom R x) = decide (FirstOrder.Language.Structure.RelMap R x)

Relabelling by permutations

@[instance_reducible]

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

Permutations of V relabel configurations on V: σ acts by restriction along σ⁻¹, so that relabelling is a left action.

theorem TauCeti.RelationalConfiguration.perm_smul_def {L : FirstOrder.Language} {V : Type u_1} (σ : Equiv.Perm V) (c : RelationalConfiguration L V) : σ • c = restrict (⇑σ⁻¹) c

Relabelling by σ is restriction along σ⁻¹.

@[simp]

theorem TauCeti.RelationalConfiguration.eval_perm_smul {L : FirstOrder.Language} {V : Type u_1} (σ : Equiv.Perm V) (c : RelationalConfiguration L V) (a : Atom L V) : (σ • c).eval a = c.eval (Atom.map (⇑(Equiv.symm σ)) a)

Relabelling by σ reads every atom at its relabelling along σ⁻¹.

@[instance_reducible]

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

Relabelling by permutations is a left action on configurations.

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

Each relabelling by a permutation is measurable.

Finitary relabelling of configurations over ℕ

@[instance_reducible]

instance TauCeti.RelationalConfiguration.instSMulFinitaryPerm {L : FirstOrder.Language} : SMul FinitaryPerm (RelationalConfiguration L ℕ)

Finitely supported permutations of ℕ relabel configurations over ℕ: g acts by restriction along g⁻¹, so that relabelling is a left action.

theorem TauCeti.RelationalConfiguration.finitaryPerm_smul_def {L : FirstOrder.Language} (g : FinitaryPerm) (c : RelationalConfiguration L ℕ) : g • c = restrict (⇑g.toPerm⁻¹) c

Relabelling by g is restriction along g⁻¹.

@[simp]

theorem TauCeti.RelationalConfiguration.eval_finitaryPerm_smul {L : FirstOrder.Language} (g : FinitaryPerm) (c : RelationalConfiguration L ℕ) (a : Atom L ℕ) : (g • c).eval a = c.eval (Atom.map (⇑g.toPerm⁻¹) a)

Relabelling by g reads every atom at its relabelling along g⁻¹.

theorem TauCeti.RelationalConfiguration.finitaryPerm_smul_eq_toPerm_smul {L : FirstOrder.Language} (g : FinitaryPerm) (c : RelationalConfiguration L ℕ) : g • c = g.toPerm • c

Finitary relabelling by g is relabelling by the underlying permutation of ℕ.

@[instance_reducible]

instance TauCeti.RelationalConfiguration.instMulActionFinitaryPerm {L : FirstOrder.Language} : MulAction FinitaryPerm (RelationalConfiguration L ℕ)

Finitary relabelling is a left action on configurations over ℕ.

instance TauCeti.RelationalConfiguration.instMeasurableConstSMulFinitaryPerm {L : FirstOrder.Language} : MeasurableConstSMul FinitaryPerm (RelationalConfiguration L ℕ)

Each finitary relabelling of configurations over ℕ is measurable.