Associativity of labeled-graph gluing

The product of labeled graphs identifies equally numbered labels and retains all other vertices. Its two three-factor parenthesizations are isomorphic by the equivalence that fixes each vertex of each factor. The isomorphism preserves the labels, so it can be used inside further gluings. This supplies associativity for the gluing algebra used by connection matrices.

References

• L. Lovász and B. Szegedy, Limits of dense graph sequences, JCTB 96 (2006), Section 2.

noncomputable def TauCeti.DenseGraphLimits.LabeledGraph.glueAssocIso {k : ℕ} (A B C : LabeledGraph k) : ((A.glue B).glue C).graph ≃g (A.glue (B.glue C)).graph

Gluing three labeled graphs is associative up to a label-preserving graph isomorphism.

Equations

• A.glueAssocIso B C = { toEquiv := TauCeti.DenseGraphLimits.LabeledGraph.glueAssocEquiv✝ A B C, map_rel_iff' := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueAssocIso_label {k : ℕ} (A B C : LabeledGraph k) (i : Fin k) : (A.glueAssocIso B C) (((A.glue B).glue C).label i) = (A.glue (B.glue C)).label i

The associativity isomorphism fixes the label with each index.

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueAssocIso_inl_inl {k : ℕ} (A B C : LabeledGraph k) (a : Fin A.n) : (A.glueAssocIso B C) (((A.glue B).glueInl C) ((A.glueInl B) a)) = (A.glueInl (B.glue C)) a

Reassociation fixes vertices coming from the first factor.

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueAssocIso_inl_inr {k : ℕ} (A B C : LabeledGraph k) (b : Fin B.n) : (A.glueAssocIso B C) (((A.glue B).glueInl C) ((A.glueInr B) b)) = (A.glueInr (B.glue C)) ((B.glueInl C) b)

Reassociation fixes vertices coming from the middle factor.

@[simp]

theorem TauCeti.DenseGraphLimits.LabeledGraph.glueAssocIso_inr {k : ℕ} (A B C : LabeledGraph k) (c : Fin C.n) : (A.glueAssocIso B C) (((A.glue B).glueInr C) c) = (A.glueInr (B.glue C)) ((B.glueInr C) c)

Reassociation fixes vertices coming from the final factor.