Simple graphs as relational configurations

The language of graphs, FirstOrder.Language.graph, has a single binary relation symbol adj. A relational configuration of it is a truth value for every atom adj(u, v), including the diagonal atoms adj(v, v). The configurations that are symmetric and false on the diagonal are exactly the simple graphs: this file identifies SimpleGraph V with them as a measurable equivalence, and shows that pulling a graph back along a vertex map corresponds to restricting its configuration. Forgetting the simple-graph conditions, a configuration is just its array of truth values on the adjacency atoms (TauCeti.RelationalConfiguration.adjArrayEquiv), and the array of a simple graph is its adjacency array.

Main definitions

• TauCeti.RelationalConfiguration.IsSimpleGraph — a configuration of the language of graphs is symmetric and irreflexive;
• SimpleGraph.toRelationalConfiguration — the configuration of a simple graph;
• SimpleGraph.relationalConfigurationEquiv — the measurable equivalence between simple graphs and symmetric irreflexive configurations;
• TauCeti.RelationalConfiguration.adjArrayEquiv — the measurable equivalence between configurations of the language of graphs and Bool-valued arrays.

Main results

• SimpleGraph.measurableEmbedding_toRelationalConfiguration — on a countable vertex type, the encoding is a measurable embedding onto the simple-graph configurations (SimpleGraph.range_toRelationalConfiguration);
• SimpleGraph.map_comap_toRelationalConfiguration — a law on configurations concentrated on simple graphs is the encoding of its pullback to simple graphs;
• SimpleGraph.toRelationalConfiguration_comap — encoding a pulled-back graph is restricting its encoding; for laws, SimpleGraph.map_comap_comap_toRelationalConfiguration — pulling back to simple graphs commutes with restriction;
• TauCeti.RelationalConfiguration.IsSimpleGraph.restrict — restriction preserves symmetry and irreflexivity, also along non-injective vertex maps;
• SimpleGraph.adjArrayEquiv_toRelationalConfiguration — the array of the configuration of a simple graph is its adjacency array;
• SimpleGraph.relationalConfigurationEquiv_comap and SimpleGraph.relationalConfigurationEquiv_symm_restrict — the equivalence commutes with restriction in both directions.

def TauCeti.RelationalConfiguration.adjAtom {V : Type u_1} (u v : V) : Atom FirstOrder.Language.graph V

The adjacency atom adj(u, v).

@[simp]

theorem TauCeti.RelationalConfiguration.adjAtom_map {V : Type u_1} {W : Type u_2} (f : V → W) (u v : V) : Atom.map f (adjAtom u v) = adjAtom (f u) (f v)

theorem TauCeti.RelationalConfiguration.Atom.induction_adjAtom {V : Type u_1} {motive : Atom FirstOrder.Language.graph V → Prop} (h : ∀ (u v : V), motive (adjAtom u v)) (a : Atom FirstOrder.Language.graph V) : motive a

Every atom of the language of graphs is an adjacency atom.

def TauCeti.RelationalConfiguration.IsSimpleGraph {V : Type u_1} (c : RelationalConfiguration FirstOrder.Language.graph V) : Prop

A configuration of the language of graphs is a simple graph when adjacency is symmetric and false on the diagonal.

theorem TauCeti.RelationalConfiguration.isSimpleGraph_iff {V : Type u_1} {c : RelationalConfiguration FirstOrder.Language.graph V} : c.IsSimpleGraph ↔ (∀ (u v : V), c.eval (adjAtom u v) = c.eval (adjAtom v u)) ∧ ∀ (v : V), c.eval (adjAtom v v) = false

A configuration is a simple graph exactly when adjacency is symmetric and false on the diagonal.

def TauCeti.RelationalConfiguration.toSimpleGraph {V : Type u_1} (c : RelationalConfiguration FirstOrder.Language.graph V) (hc : c.IsSimpleGraph) : SimpleGraph V

The simple graph of a symmetric irreflexive configuration.

@[simp]

theorem TauCeti.RelationalConfiguration.toSimpleGraph_adj {V : Type u_1} (c : RelationalConfiguration FirstOrder.Language.graph V) (hc : c.IsSimpleGraph) (u v : V) : (c.toSimpleGraph hc).Adj u v ↔ c.eval (adjAtom u v) = true

theorem TauCeti.RelationalConfiguration.IsSimpleGraph.restrict {V : Type u_1} {W : Type u_2} {c : RelationalConfiguration FirstOrder.Language.graph W} (hc : c.IsSimpleGraph) (f : V → W) : (RelationalConfiguration.restrict f c).IsSimpleGraph

Restriction preserves symmetry and irreflexivity. The vertex map need not be injective: a pair of distinct vertices with the same image reads a diagonal atom, which is false.

theorem TauCeti.RelationalConfiguration.measurableSet_setOf_isSimpleGraph {V : Type u_1} [Countable V] : MeasurableSet {c : RelationalConfiguration FirstOrder.Language.graph V | c.IsSimpleGraph}

On a countable vertex type, the simple-graph configurations form a measurable set: a countable intersection of conditions on one or two atoms.

theorem TauCeti.RelationalConfiguration.ae_isSimpleGraph_map_restrict {V : Type u_1} {W : Type u_2} [Countable V] (f : V → W) {μ : MeasureTheory.Measure (RelationalConfiguration FirstOrder.Language.graph W)} (hμ : ∀ᵐ (c : RelationalConfiguration FirstOrder.Language.graph W) ∂μ, c.IsSimpleGraph) : ∀ᵐ (c : RelationalConfiguration FirstOrder.Language.graph V) ∂MeasureTheory.Measure.map (restrict f) μ, c.IsSimpleGraph

Restricting a law concentrated on simple graphs gives a law concentrated on simple graphs.

Configurations as arrays

noncomputable def TauCeti.RelationalConfiguration.adjArrayEquiv {V : Type u_1} : RelationalConfiguration FirstOrder.Language.graph V ≃ᵐ (V × V → Bool)

Configurations of the language of graphs are Bool-valued arrays: a configuration is determined by its truth values on the adjacency atoms adj(u, v), one for each ordered pair of vertices, and these truth values can be prescribed freely.

@[simp]

theorem TauCeti.RelationalConfiguration.adjArrayEquiv_apply {V : Type u_1} (c : RelationalConfiguration FirstOrder.Language.graph V) (p : V × V) : adjArrayEquiv c p = c.eval (adjAtom p.1 p.2)

The array of a configuration records its truth value on each adjacency atom.

@[simp]

theorem TauCeti.RelationalConfiguration.eval_adjArrayEquiv_symm_adjAtom {V : Type u_1} (x : V × V → Bool) (u v : V) : (adjArrayEquiv.symm x).eval (adjAtom u v) = x (u, v)

The configuration of an array takes the prescribed truth value on each adjacency atom.

noncomputable def SimpleGraph.toRelationalConfiguration {V : Type u_1} (G : SimpleGraph V) : TauCeti.RelationalConfiguration FirstOrder.Language.graph V

The configuration of a simple graph, read off its first-order structure.

@[simp]

theorem SimpleGraph.eval_toRelationalConfiguration_adjAtom {V : Type u_1} (G : SimpleGraph V) (u v : V) : G.toRelationalConfiguration.eval (TauCeti.RelationalConfiguration.adjAtom u v) = decide (G.Adj u v)

@[simp]

theorem SimpleGraph.toStructure_toRelationalConfiguration {V : Type u_1} (G : SimpleGraph V) : G.toRelationalConfiguration.toStructure = G.structure

The configuration of a simple graph decodes to the graph's structure.

theorem SimpleGraph.isSimpleGraph_toRelationalConfiguration {V : Type u_1} (G : SimpleGraph V) : G.toRelationalConfiguration.IsSimpleGraph

noncomputable def SimpleGraph.relationalConfigurationEquiv {V : Type u_1} : SimpleGraph V ≃ᵐ { c : TauCeti.RelationalConfiguration FirstOrder.Language.graph V // c.IsSimpleGraph }

Simple graphs are the symmetric irreflexive configurations of the language of graphs, as a measurable equivalence.

theorem SimpleGraph.measurable_toRelationalConfiguration {V : Type u_1} : Measurable toRelationalConfiguration

Encoding a simple graph as a configuration is measurable.

@[simp]

theorem SimpleGraph.coe_relationalConfigurationEquiv {V : Type u_1} (G : SimpleGraph V) : ↑(relationalConfigurationEquiv G) = G.toRelationalConfiguration

@[simp]

theorem SimpleGraph.relationalConfigurationEquiv_symm_apply {V : Type u_1} (c : { c : TauCeti.RelationalConfiguration FirstOrder.Language.graph V // c.IsSimpleGraph }) : relationalConfigurationEquiv.symm c = (↑c).toSimpleGraph ⋯

@[simp]

theorem SimpleGraph.range_toRelationalConfiguration {V : Type u_1} : Set.range toRelationalConfiguration = {c : TauCeti.RelationalConfiguration FirstOrder.Language.graph V | c.IsSimpleGraph}

The configurations of simple graphs are exactly the simple-graph configurations.

theorem SimpleGraph.measurableEmbedding_toRelationalConfiguration {V : Type u_1} [Countable V] : MeasurableEmbedding toRelationalConfiguration

On a countable vertex type, encoding simple graphs as configurations is a measurable embedding, so laws on simple graphs are the laws on configurations concentrated on simple graphs.

theorem SimpleGraph.ae_isSimpleGraph_map_toRelationalConfiguration {V : Type u_1} [Countable V] (μ : MeasureTheory.Measure (SimpleGraph V)) : ∀ᵐ (c : TauCeti.RelationalConfiguration FirstOrder.Language.graph V) ∂MeasureTheory.Measure.map toRelationalConfiguration μ, c.IsSimpleGraph

The encoding of a law on simple graphs is concentrated on simple graphs.

theorem SimpleGraph.map_comap_toRelationalConfiguration {V : Type u_1} [Countable V] {μ : MeasureTheory.Measure (TauCeti.RelationalConfiguration FirstOrder.Language.graph V)} (hμ : ∀ᵐ (c : TauCeti.RelationalConfiguration FirstOrder.Language.graph V) ∂μ, c.IsSimpleGraph) : MeasureTheory.Measure.map toRelationalConfiguration (MeasureTheory.Measure.comap toRelationalConfiguration μ) = μ

A law on configurations concentrated on simple graphs is the encoding of its pullback to simple graphs.

theorem SimpleGraph.isProbabilityMeasure_comap_toRelationalConfiguration {V : Type u_1} [Countable V] {μ : MeasureTheory.Measure (TauCeti.RelationalConfiguration FirstOrder.Language.graph V)} [MeasureTheory.IsProbabilityMeasure μ] (hμ : ∀ᵐ (c : TauCeti.RelationalConfiguration FirstOrder.Language.graph V) ∂μ, c.IsSimpleGraph) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap toRelationalConfiguration μ)

The pullback to simple graphs of a probability law concentrated on simple graphs is a probability law.

@[simp]

theorem SimpleGraph.adjArrayEquiv_toRelationalConfiguration {V : Type u_1} (G : SimpleGraph V) : TauCeti.RelationalConfiguration.adjArrayEquiv G.toRelationalConfiguration = G.adjArray

The array of the configuration of a simple graph is its adjacency array.

Compatibility with restriction

theorem SimpleGraph.toRelationalConfiguration_comap {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph W) : (SimpleGraph.comap f G).toRelationalConfiguration = TauCeti.RelationalConfiguration.restrict f G.toRelationalConfiguration

Encoding commutes with restriction: the configuration of a pulled-back graph is the restriction of the configuration.

theorem SimpleGraph.toRelationalConfiguration_comp_comap {V : Type u_1} {W : Type u_2} (f : V → W) : toRelationalConfiguration ∘ SimpleGraph.comap f = TauCeti.RelationalConfiguration.restrict f ∘ toRelationalConfiguration

Encoding commutes with restriction, as an identity of maps.

theorem SimpleGraph.map_comap_comap_toRelationalConfiguration {V : Type u_1} {W : Type u_2} [Countable V] [Countable W] (f : V → W) {μ : MeasureTheory.Measure (TauCeti.RelationalConfiguration FirstOrder.Language.graph W)} (hμ : ∀ᵐ (c : TauCeti.RelationalConfiguration FirstOrder.Language.graph W) ∂μ, c.IsSimpleGraph) : MeasureTheory.Measure.map (SimpleGraph.comap f) (MeasureTheory.Measure.comap toRelationalConfiguration μ) = MeasureTheory.Measure.comap toRelationalConfiguration (MeasureTheory.Measure.map (TauCeti.RelationalConfiguration.restrict f) μ)

For laws concentrated on simple graphs, pulling back to simple graphs commutes with restriction.

theorem SimpleGraph.relationalConfigurationEquiv_comap {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph W) : relationalConfigurationEquiv (SimpleGraph.comap f G) = ⟨TauCeti.RelationalConfiguration.restrict f ↑(relationalConfigurationEquiv G), ⋯⟩

theorem SimpleGraph.relationalConfigurationEquiv_symm_restrict {V : Type u_1} {W : Type u_2} (f : V → W) (c : { c : TauCeti.RelationalConfiguration FirstOrder.Language.graph W // c.IsSimpleGraph }) : relationalConfigurationEquiv.symm ⟨TauCeti.RelationalConfiguration.restrict f ↑c, ⋯⟩ = SimpleGraph.comap f (relationalConfigurationEquiv.symm c)

Decoding commutes with restriction.