Products of labelled graphs

The product of two based labelled Serre graphs pairs darts carrying the same signed letter. Its closed paths project to closed paths in both factors. For folded factors, paths with the same reduced label combine in the product, so it accepts exactly the subgroup intersection. Foldedness and finiteness are preserved by the product.

The construction is the fibre product over the labelled rose used in Stallings' subgroup intersection method.

References

• I. Kapovich and A. Myasnikov, Stallings foldings and subgroups of free groups, Section 9, Proposition 9.4.

def TauCeti.StallingsGraph.prod {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) : StallingsGraph α

The based fibre product of labelled graphs: vertices are pairs and darts are pairs with identical signed labels.

@[simp]

theorem TauCeti.StallingsGraph.prod_base {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) : (S.prod T).base = (S.base, T.base)

@[simp]

theorem TauCeti.StallingsGraph.prod_label {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) (e : (S.prod T).graph.E) : (S.prod T).label e = S.label (↑e).1

@[simp]

theorem TauCeti.StallingsGraph.prod_src {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) (e : (S.prod T).graph.E) : (S.prod T).graph.src e = (S.graph.src (↑e).1, T.graph.src (↑e).2)

@[simp]

theorem TauCeti.StallingsGraph.prod_rev {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) (e : (S.prod T).graph.E) : ↑((S.prod T).graph.rev e) = (S.graph.rev (↑e).1, T.graph.rev (↑e).2)

@[simp]

theorem TauCeti.StallingsGraph.prod_tgt {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) (e : (S.prod T).graph.E) : (S.prod T).graph.tgt e = (S.graph.tgt (↑e).1, T.graph.tgt (↑e).2)

def TauCeti.StallingsGraph.prodFst {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) : (S.prod T).Hom S

The first projection preserves the base point and labels.

def TauCeti.StallingsGraph.prodSnd {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) : (S.prod T).Hom T

The second projection preserves the base point and labels.

@[simp]

theorem TauCeti.StallingsGraph.prodFst_mapV {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) (p : (S.prod T).graph.V) : (S.prodFst T).graphHom.mapV p = p.1

@[simp]

theorem TauCeti.StallingsGraph.prodSnd_mapV {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) (p : (S.prod T).graph.V) : (S.prodSnd T).graphHom.mapV p = p.2

@[simp]

theorem TauCeti.StallingsGraph.prodFst_mapE {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) (e : (S.prod T).graph.E) : (S.prodFst T).graphHom.mapE e = (↑e).1

@[simp]

theorem TauCeti.StallingsGraph.prodSnd_mapE {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) (e : (S.prod T).graph.E) : (S.prodSnd T).graphHom.mapE e = (↑e).2

def TauCeti.StallingsGraph.prodLift {α : Type u} {R : StallingsGraph α} {S : StallingsGraph α} {T : StallingsGraph α} (f : R.Hom S) (g : R.Hom T) : R.Hom (S.prod T)

Pair two morphisms with a common source into the labelled fibre product.

@[simp]

theorem TauCeti.StallingsGraph.prodLift_mapV {α : Type u} {R : StallingsGraph α} {S : StallingsGraph α} {T : StallingsGraph α} (f : R.Hom S) (g : R.Hom T) (a : R.graph.V) : (prodLift f g).graphHom.mapV a = (f.graphHom.mapV a, g.graphHom.mapV a)

@[simp]

theorem TauCeti.StallingsGraph.prodLift_mapE {α : Type u} {R : StallingsGraph α} {S : StallingsGraph α} {T : StallingsGraph α} (f : R.Hom S) (g : R.Hom T) (e : R.graph.E) : ↑((prodLift f g).graphHom.mapE e) = (f.graphHom.mapE e, g.graphHom.mapE e)

@[simp]

theorem TauCeti.StallingsGraph.prodFst_comp_prodLift {α : Type u} {R : StallingsGraph α} {S : StallingsGraph α} {T : StallingsGraph α} (f : R.Hom S) (g : R.Hom T) : (S.prodFst T).comp (prodLift f g) = f

@[simp]

theorem TauCeti.StallingsGraph.prodSnd_comp_prodLift {α : Type u} {R : StallingsGraph α} {S : StallingsGraph α} {T : StallingsGraph α} (f : R.Hom S) (g : R.Hom T) : (S.prodSnd T).comp (prodLift f g) = g

theorem TauCeti.StallingsGraph.prodLift_unique {α : Type u} {R : StallingsGraph α} {S : StallingsGraph α} {T : StallingsGraph α} (h : R.Hom (S.prod T)) : prodLift ((S.prodFst T).comp h) ((S.prodSnd T).comp h) = h

A map into the product is determined by its two projections.

instance TauCeti.StallingsGraph.instFiniteVGraphProd {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) [Finite S.graph.V] [Finite T.graph.V] : Finite (S.prod T).graph.V

instance TauCeti.StallingsGraph.instFiniteEGraphProd {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) [Finite S.graph.E] [Finite T.graph.E] : Finite (S.prod T).graph.E

theorem TauCeti.StallingsGraph.prod_subgroup_le {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) (a : S.graph.V) (b : T.graph.V) : (S.prod T).subgroup (a, b) ≤ S.subgroup a ⊓ T.subgroup b

Every word read at a vertex pair is read at each coordinate.

theorem TauCeti.StallingsGraph.exists_prod_path_of_word_eq {α : Type u} (S : StallingsGraph α) (T : StallingsGraph α) {a b : S.graph.V} {c d : T.graph.V} (p : S.graph.Path a b) (q : T.graph.Path c d) (h : S.word p = T.word q) : ∃ (r : (S.prod T).graph.Path (a, c) (b, d)), (S.prodFst T).graphHom.toPrefunctor.mapPath r = p ∧ (S.prodSnd T).graphHom.toPrefunctor.mapPath r = q

Paths with the same sequence of signed labels pair to a path in the product.

theorem TauCeti.StallingsGraph.prod_subgroup {α : Type u} {S : StallingsGraph α} {T : StallingsGraph α} (hS : S.IsFolded) (hT : T.IsFolded) (a : S.graph.V) (b : T.graph.V) : (S.prod T).subgroup (a, b) = S.subgroup a ⊓ T.subgroup b

The product of folded labelled graphs reads exactly the intersection of their accepted subgroups, at every pair of vertices.

theorem TauCeti.StallingsGraph.IsFolded.prod {α : Type u} {S : StallingsGraph α} {T : StallingsGraph α} (hS : S.IsFolded) (hT : T.IsFolded) : (S.prod T).IsFolded

A product of folded labelled graphs is folded.

theorem TauCeti.StallingsGraph.prod_subgroup_of_hom {α : Type u} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) : (S.prod T).subgroup (S.prod T).base = S.subgroup S.base

A morphism into the second factor makes the product accept exactly the first subgroup.

theorem TauCeti.StallingsGraph.prod_subgroup_of_hom_right {α : Type u} {S : StallingsGraph α} {T : StallingsGraph α} (f : T.Hom S) : (S.prod T).subgroup (S.prod T).base = T.subgroup T.base

A morphism into the first factor makes the product accept exactly the second subgroup.

theorem TauCeti.StallingsGraph.prod_rose_subgroup {α : Type u} (S : StallingsGraph α) : (S.prod (rose α)).subgroup (S.prod (rose α)).base = S.subgroup S.base

The rose imposes no additional restriction on accepted words.

theorem TauCeti.StallingsGraph.rose_prod_subgroup {α : Type u} (S : StallingsGraph α) : ((rose α).prod S).subgroup ((rose α).prod S).base = S.subgroup S.base

A rose in the first factor imposes no additional restriction on accepted words.