k-labeled graphs and their gluing

A k-labeled graph is a finite simple graph together with an ordered k-tuple of distinct vertices. Gluing two of them identifies corresponding labeled vertices and takes the union of the edge sets; the identified vertices keep their labels, so the result is again a k-labeled graph and gluing iterates. This is Lovász–Szegedy's product F₁F₂ of k-labeled graphs, the algebra underlying connection matrices and reflection positivity.

Main definitions

• TauCeti.DenseGraphLimits.LabeledGraph is the k-labeled graph;
• TauCeti.DenseGraphLimits.LabeledGraph.glue glues two of them along their labels;
• TauCeti.DenseGraphLimits.LabeledGraph.glueInl and TauCeti.DenseGraphLimits.LabeledGraph.glueInr are the two vertex maps into the gluing;
• TauCeti.DenseGraphLimits.LabeledGraph.forgetLabels is the underlying unlabeled graph;
• TauCeti.DenseGraphLimits.LabeledGraph.fullyLabeled labels every vertex of a graph on Fin n by its own index;
• TauCeti.DenseGraphLimits.LabeledGraph.labelSumUnlabeledEquiv and TauCeti.DenseGraphLimits.LabeledGraph.glueEquiv are the coordinates splitting the vertices of a labeled graph, and of a gluing, into labels and unlabeled vertices.

Main results

• TauCeti.DenseGraphLimits.LabeledGraph.glue_graph identifies the glued graph as the supremum of the two mapped sources, so no edge is created that neither source carries;
• TauCeti.DenseGraphLimits.LabeledGraph.glueInl_eq_glueInr_iff says the two sides meet exactly at corresponding labels, and TauCeti.DenseGraphLimits.LabeledGraph.glue_surjective that they cover the gluing: together they present the vertex set as the pushout;
• TauCeti.DenseGraphLimits.LabeledGraph.glue_card is the resulting vertex count n₁ + n₂ - k;
• TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_inl, TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_inr and TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_inl_inr are the adjacency eliminators, and TauCeti.DenseGraphLimits.LabeledGraph.not_glue_adj_of_unlabeled records that unlabeled vertices of the two sides are never joined;
• TauCeti.DenseGraphLimits.LabeledGraph.forgetLabels_def is the defining law for unlabeling, by which a dependent value f G.forgetLabels.1 G.forgetLabels.2 is evaluated;
• TauCeti.DenseGraphLimits.LabeledGraph.glueCommIso is the commutativity of the gluing algebra, the isomorphism between the two orders of a gluing that makes connection matrices symmetric, and TauCeti.DenseGraphLimits.LabeledGraph.glueCommIso_label says it retains the labels, so it is an isomorphism of k-labeled graphs and commutativity survives a further gluing;
• TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_label says two labels of a gluing are joined exactly when they are joined on one side, and TauCeti.DenseGraphLimits.LabeledGraph.glueInl_labelSumUnlabeledEquiv and TauCeti.DenseGraphLimits.LabeledGraph.glueInr_labelSumUnlabeledEquiv express the two vertex maps into a gluing in coordinates;
• TauCeti.DenseGraphLimits.LabeledGraph.glueFullyLabeledIso says gluing two fully labeled graphs overlays them.

Implementation

The vertex set of a gluing is built as the concrete pushout carrier Fin k ⊕ (G₁.Unlabeled ⊕ G₂.Unlabeled) — the shared labels, then the private vertices of each side — and transported to a Fin-representative along Fintype.equivFin, since the structure stores its vertex set as Fin n. Writing the carrier in this symmetric shape is what makes commutativity a swap of the two summands rather than a bespoke bijection.

Both adjacency eliminators are stated in their honest form. Two labeled vertices of the left side can be joined by an edge contributed by the right side, so the naive Adj (glueInl a) (glueInl b) ↔ G₁.graph.Adj a b is false; the correct statement carries the extra disjunct, which collapses as soon as one of the two vertices is unlabeled (glue_adj_inl_of_unlabeled).

References

• L. Lovász, B. Szegedy, Limits of dense graph sequences, JCTB 96 (2006), 933–957, Section 2 — k-labeled graphs, their product, and connection matrices.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Chapter 6.

structure TauCeti.DenseGraphLimits.LabeledGraph (k : ℕ) : Type

A k-labeled graph: a finite simple graph on Fin n together with an ordered k-tuple of distinct labeled vertices. These are the objects of the gluing algebra behind connection matrices.

• n : ℕ

  The number of vertices.

• graph : SimpleGraph (Fin self.n)

  The underlying simple graph.

• label : Fin k → Fin self.n

  The labeled vertices, in order.

• label_injective : Function.Injective self.label

  The labeled vertices are distinct.

theorem TauCeti.DenseGraphLimits.LabeledGraph.le_n {k : ℕ} (G : LabeledGraph k) : k ≤ G.n

A labeled graph has at least as many vertices as labels.

@[reducible, inline]

abbrev TauCeti.DenseGraphLimits.LabeledGraph.Unlabeled {k : ℕ} (G : LabeledGraph k) : Type

The vertices of a labeled graph that carry no label — the ones a gluing keeps private to its side.

Equations

• G.Unlabeled = { a : Fin G.n // ∀ (i : Fin k), G.label i ≠ a }

@[instance_reducible]

instance TauCeti.DenseGraphLimits.LabeledGraph.instFintypeUnlabeled {k : ℕ} (G : LabeledGraph k) : Fintype G.Unlabeled

The unlabeled vertices of a labeled graph inherit a finite type from Fin G.n, of which they are a subtype.

Equations

• G.instFintypeUnlabeled = Subtype.fintype fun (a : Fin G.n) => ∀ (i : Fin k), G.label i ≠ a

theorem TauCeti.DenseGraphLimits.LabeledGraph.card_unlabeled {k : ℕ} (G : LabeledGraph k) : Fintype.card G.Unlabeled = G.n - k

The number of unlabeled vertices.

noncomputable def TauCeti.DenseGraphLimits.LabeledGraph.glue {k : ℕ} (G₁ G₂ : LabeledGraph k) : LabeledGraph k

Gluing. Glue two k-labeled graphs by identifying corresponding labeled vertices and taking the union of the two edge sets. The identified vertices keep their labels — and stay distinct — so the result is again a k-labeled graph and gluing iterates. This is Lovász–Szegedy's product F₁F₂.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.DenseGraphLimits.LabeledGraph.glueInl {k : ℕ} (G₁ G₂ : LabeledGraph k) : Fin G₁.n ↪ Fin (G₁.glue G₂).n

The vertex map of the left factor into the gluing.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.DenseGraphLimits.LabeledGraph.glueInr {k : ℕ} (G₁ G₂ : LabeledGraph k) : Fin G₂.n ↪ Fin (G₁.glue G₂).n

The vertex map of the right factor into the gluing.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glue_graph {k : ℕ} (G₁ G₂ : LabeledGraph k) : (G₁.glue G₂).graph = SimpleGraph.map (⇑(G₁.glueInl G₂)) G₁.graph ⊔ SimpleGraph.map (⇑(G₁.glueInr G₂)) G₂.graph

The glued graph is exactly the supremum of the two mapped sources: gluing creates no edge that neither side carries.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueInl_eq_glueInr_iff {k : ℕ} (G₁ G₂ : LabeledGraph k) (a : Fin G₁.n) (b : Fin G₂.n) : (G₁.glueInl G₂) a = (G₁.glueInr G₂) b ↔ ∃ (i : Fin k), a = G₁.label i ∧ b = G₂.label i

No other identifications: the two sides meet exactly at corresponding labels.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueInl_label {k : ℕ} (G₁ G₂ : LabeledGraph k) : (G₁.glue G₂).label = ⇑(G₁.glueInl G₂) ∘ G₁.label

The labels of the gluing are the images of the left labels.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueInr_label {k : ℕ} (G₁ G₂ : LabeledGraph k) : (G₁.glue G₂).label = ⇑(G₁.glueInr G₂) ∘ G₂.label

The labels of the gluing are the images of the right labels.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glue_surjective {k : ℕ} (G₁ G₂ : LabeledGraph k) (v : Fin (G₁.glue G₂).n) : (∃ (a : Fin G₁.n), v = (G₁.glueInl G₂) a) ∨ ∃ (b : Fin G₂.n), v = (G₁.glueInr G₂) b

Every vertex of the gluing comes from one of the two sides.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glue_card {k : ℕ} (G₁ G₂ : LabeledGraph k) : (G₁.glue G₂).n = G₁.n + G₂.n - k

The vertex count of a gluing. The two sides share exactly their k labels.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_inl {k : ℕ} (G₁ G₂ : LabeledGraph k) (a b : Fin G₁.n) : (G₁.glue G₂).graph.Adj ((G₁.glueInl G₂) a) ((G₁.glueInl G₂) b) ↔ G₁.graph.Adj a b ∨ ∃ (i : Fin k) (j : Fin k), a = G₁.label i ∧ b = G₁.label j ∧ G₂.graph.Adj (G₂.label i) (G₂.label j)

Adjacency on the left side. A left edge survives the gluing, and the only edges the gluing adds between two left vertices are the ones the right side contributes between labels.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_inr {k : ℕ} (G₁ G₂ : LabeledGraph k) (a b : Fin G₂.n) : (G₁.glue G₂).graph.Adj ((G₁.glueInr G₂) a) ((G₁.glueInr G₂) b) ↔ G₂.graph.Adj a b ∨ ∃ (i : Fin k) (j : Fin k), a = G₂.label i ∧ b = G₂.label j ∧ G₁.graph.Adj (G₁.label i) (G₁.label j)

Adjacency on the right side, the mirror of glue_adj_inl.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_inl_inr {k : ℕ} (G₁ G₂ : LabeledGraph k) (a : Fin G₁.n) (b : Fin G₂.n) : (G₁.glue G₂).graph.Adj ((G₁.glueInl G₂) a) ((G₁.glueInr G₂) b) ↔ (∃ (j : Fin k), b = G₂.label j ∧ G₁.graph.Adj a (G₁.label j)) ∨ ∃ (i : Fin k), a = G₁.label i ∧ G₂.graph.Adj (G₂.label i) b

Adjacency across the two sides. A left and a right vertex are joined only through a label: either the right vertex is a label and the left side carries the edge, or the left vertex is a label and the right side does.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_inl_of_adj {k : ℕ} (G₁ G₂ : LabeledGraph k) {a b : Fin G₁.n} (h : G₁.graph.Adj a b) : (G₁.glue G₂).graph.Adj ((G₁.glueInl G₂) a) ((G₁.glueInl G₂) b)

Gluing preserves the edges of the left side.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_inr_of_adj {k : ℕ} (G₁ G₂ : LabeledGraph k) {a b : Fin G₂.n} (h : G₂.graph.Adj a b) : (G₁.glue G₂).graph.Adj ((G₁.glueInr G₂) a) ((G₁.glueInr G₂) b)

Gluing preserves the edges of the right side.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_inl_of_unlabeled {k : ℕ} (G₁ G₂ : LabeledGraph k) {a : Fin G₁.n} (ha : ∀ (i : Fin k), G₁.label i ≠ a) (b : Fin G₁.n) : (G₁.glue G₂).graph.Adj ((G₁.glueInl G₂) a) ((G₁.glueInl G₂) b) ↔ G₁.graph.Adj a b

At an unlabeled left vertex the gluing reflects left adjacency faithfully: the extra disjunct of glue_adj_inl needs both endpoints to be labels.

theorem TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_inr_of_unlabeled {k : ℕ} (G₁ G₂ : LabeledGraph k) {a : Fin G₂.n} (ha : ∀ (i : Fin k), G₂.label i ≠ a) (b : Fin G₂.n) : (G₁.glue G₂).graph.Adj ((G₁.glueInr G₂) a) ((G₁.glueInr G₂) b) ↔ G₂.graph.Adj a b

At an unlabeled right vertex the gluing reflects right adjacency faithfully.

theorem TauCeti.DenseGraphLimits.LabeledGraph.not_glue_adj_of_unlabeled {k : ℕ} (G₁ G₂ : LabeledGraph k) {a : Fin G₁.n} {b : Fin G₂.n} (ha : ∀ (i : Fin k), G₁.label i ≠ a) (hb : ∀ (i : Fin k), G₂.label i ≠ b) : ¬(G₁.glue G₂).graph.Adj ((G₁.glueInl G₂) a) ((G₁.glueInr G₂) b)

No cross-edges are smuggled in: gluing never joins an unlabeled vertex of one side to an unlabeled vertex of the other.

def TauCeti.DenseGraphLimits.LabeledGraph.forgetLabels {k : ℕ} (G : LabeledGraph k) : (m : ℕ) × SimpleGraph (Fin m)

Unlabeling. The underlying finite simple graph of a k-labeled graph, labels forgotten — the object a graph parameter evaluates in a connection-matrix entry.

Equations

• G.forgetLabels = ⟨G.n, G.graph⟩

theorem TauCeti.DenseGraphLimits.LabeledGraph.forgetLabels_def {k : ℕ} (G : LabeledGraph k) : G.forgetLabels = ⟨G.n, G.graph⟩

Elimination law for unlabeling: forgetting the labels of G leaves the pair of its vertex count and its graph. Both projections are read off from this law, and it is the form a dependent occurrence f G.forgetLabels.1 G.forgetLabels.2 is rewritten by, since the two projections can only be replaced simultaneously: the type of the second mentions the first.

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.forgetLabels_fst {k : ℕ} (G : LabeledGraph k) : G.forgetLabels.fst = G.n

Unlabeling keeps the vertex count.

Commutativity of the gluing

noncomputable def TauCeti.DenseGraphLimits.LabeledGraph.glueCommIso {k : ℕ} (G₁ G₂ : LabeledGraph k) : (G₁.glue G₂).graph ≃g (G₂.glue G₁).graph

Commutativity of the gluing algebra. The two orders of a gluing are isomorphic, so a graph parameter that is isomorphism invariant takes the same value on both — this is what makes connection matrices symmetric.

Equations

• G₁.glueCommIso G₂ = { toEquiv := TauCeti.DenseGraphLimits.LabeledGraph.glueCommEquiv✝ G₁ G₂, map_rel_iff' := ⋯ }

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueCommIso_label {k : ℕ} (G₁ G₂ : LabeledGraph k) (i : Fin k) : (G₁.glueCommIso G₂) ((G₁.glue G₂).label i) = (G₂.glue G₁).label i

Commutativity retains the labels. glueCommIso carries the i-th label of one order of a gluing to the i-th label of the other, so it is an isomorphism of k-labeled graphs and not merely of the underlying graphs: commutativity may therefore be used inside a further gluing.

Coordinates

The vertices of a k-labeled graph split into its labels and its unlabeled vertices, and the vertices of a gluing split into the shared labels and the unlabeled vertices of the two sides. These splittings are the coordinates in which a vertex assignment of a gluing is a labeled part together with one private part for each side.

noncomputable def TauCeti.DenseGraphLimits.LabeledGraph.labelSumUnlabeledEquiv {k : ℕ} (G : LabeledGraph k) : Fin k ⊕ G.Unlabeled ≃ Fin G.n

The vertices of a k-labeled graph are its k labels together with its unlabeled vertices.

Equations

• G.labelSumUnlabeledEquiv = ((Equiv.ofInjective G.label ⋯).sumCongr (Equiv.subtypeEquivRight ⋯)).trans (Equiv.sumCompl fun (x : Fin G.n) => x ∈ Set.range G.label)

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.labelSumUnlabeledEquiv_inl {k : ℕ} (G : LabeledGraph k) (i : Fin k) : G.labelSumUnlabeledEquiv (Sum.inl i) = G.label i

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.labelSumUnlabeledEquiv_inr {k : ℕ} (G : LabeledGraph k) (a : G.Unlabeled) : G.labelSumUnlabeledEquiv (Sum.inr a) = ↑a

noncomputable def TauCeti.DenseGraphLimits.LabeledGraph.glueEquiv {k : ℕ} (G₁ G₂ : LabeledGraph k) : Fin k ⊕ G₁.Unlabeled ⊕ G₂.Unlabeled ≃ Fin (G₁.glue G₂).n

The vertices of a gluing are the shared labels together with the unlabeled vertices of each side.

Equations

• G₁.glueEquiv G₂ = TauCeti.DenseGraphLimits.LabeledGraph.glueIndex✝ G₁ G₂

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueEquiv_inl {k : ℕ} (G₁ G₂ : LabeledGraph k) (i : Fin k) : (G₁.glueEquiv G₂) (Sum.inl i) = (G₁.glue G₂).label i

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueEquiv_inr_inl {k : ℕ} (G₁ G₂ : LabeledGraph k) (a : G₁.Unlabeled) : (G₁.glueEquiv G₂) (Sum.inr (Sum.inl a)) = (G₁.glueInl G₂) ↑a

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueEquiv_inr_inr {k : ℕ} (G₁ G₂ : LabeledGraph k) (b : G₂.Unlabeled) : (G₁.glueEquiv G₂) (Sum.inr (Sum.inr b)) = (G₁.glueInr G₂) ↑b

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueInl_labelSumUnlabeledEquiv {k : ℕ} (G₁ G₂ : LabeledGraph k) (s : Fin k ⊕ G₁.Unlabeled) : (G₁.glueInl G₂) (G₁.labelSumUnlabeledEquiv s) = (G₁.glueEquiv G₂) (Sum.map id Sum.inl s)

In coordinates, the left vertex map of a gluing sends the labels to the shared labels and the unlabeled vertices to the private left summand.

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueInr_labelSumUnlabeledEquiv {k : ℕ} (G₁ G₂ : LabeledGraph k) (s : Fin k ⊕ G₂.Unlabeled) : (G₁.glueInr G₂) (G₂.labelSumUnlabeledEquiv s) = (G₁.glueEquiv G₂) (Sum.map id Sum.inr s)

In coordinates, the right vertex map of a gluing sends the labels to the shared labels and the unlabeled vertices to the private right summand.

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.glue_adj_label {k : ℕ} (G₁ G₂ : LabeledGraph k) (i j : Fin k) : (G₁.glue G₂).graph.Adj ((G₁.glue G₂).label i) ((G₁.glue G₂).label j) ↔ G₁.graph.Adj (G₁.label i) (G₁.label j) ∨ G₂.graph.Adj (G₂.label i) (G₂.label j)

Adjacency between labels. Two labels of a gluing are joined exactly when they are joined on one of the two sides.

Fully labeled graphs

def TauCeti.DenseGraphLimits.LabeledGraph.fullyLabeled {n : ℕ} (G : SimpleGraph (Fin n)) : LabeledGraph n

The fully labeled graph: a graph G on Fin n with every vertex labeled, by its own index. Gluing two fully labeled graphs overlays them (glueFullyLabeledIso), so the connection matrices of the fully labeled graphs on Fin n record a parameter on the suprema G ⊔ G'.

Equations

• TauCeti.DenseGraphLimits.LabeledGraph.fullyLabeled G = { n := n, graph := G, label := id, label_injective := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.fullyLabeled_n {n : ℕ} (G : SimpleGraph (Fin n)) : (fullyLabeled G).n = n

A fully labeled graph on Fin n has n vertices.

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.forgetLabels_fullyLabeled {n : ℕ} (G : SimpleGraph (Fin n)) : (fullyLabeled G).forgetLabels = ⟨n, G⟩

Forgetting the labels of a fully labeled graph returns the graph.

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.val_fullyLabeled_label {n : ℕ} (G : SimpleGraph (Fin n)) (i : Fin n) : ↑((fullyLabeled G).label i) = ↑i

Every vertex of a fully labeled graph is labeled by its own index.

noncomputable def TauCeti.DenseGraphLimits.LabeledGraph.glueFullyLabeledIso {n : ℕ} (G G' : SimpleGraph (Fin n)) : G ⊔ G' ≃g ((fullyLabeled G).glue (fullyLabeled G')).graph

Gluing two fully labeled graphs overlays them: the left vertex map is an isomorphism from G ⊔ G' onto the gluing, since every vertex of the right side is labeled and so is identified with a vertex of the left side.

Equations

• One or more equations did not get rendered due to their size.