Documentation

TauCeti.Combinatorics.Graph.Stallings.Fold.Basic

Folding a pair of equally labelled darts #

A Stallings fold identifies two darts with the same source and label, their reverses, and their target vertices. The resulting labelled graph comes with a surjective morphism from the original graph. This construction also handles loop darts and parallel darts.

The quotient follows I. Kapovich and A. Myasnikov, Stallings foldings and subgroups of free groups, §2, Definition 2.4 and Lemma 2.5.

source
def TauCeti.StallingsGraph.foldAt {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) :
StallingsGraph α

The labelled graph obtained by identifying two equally labelled outgoing darts.

Instances For
    source
    def TauCeti.StallingsGraph.foldHom {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) :
    S.Hom (S.foldAt f₁ f₂ hsrc hlabel)

    The canonical label-preserving morphism into a Stallings fold.

    Instances For
      source
      theorem TauCeti.StallingsGraph.foldHom_mapV_eq_iff {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) (x y : S.graph.V) :
      (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapV x = (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapV y ↔ Relation.EqvGen (fun (a b : S.graph.V) => a = S.graph.tgt f₁ ∧ b = S.graph.tgt f₂) x y

      Two vertices have the same image exactly when the fold relation identifies them.

      source
      theorem TauCeti.StallingsGraph.foldHom_mapE_eq_iff {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) (e e' : S.graph.E) :
      (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapE e = (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapE e' ↔ Relation.EqvGen (fun (a b : S.graph.E) => a = f₁ ∧ b = f₂ ∨ a = S.graph.rev f₁ ∧ b = S.graph.rev f₂) e e'

      Two darts have the same image exactly when the fold relation identifies them.

      source
      theorem TauCeti.StallingsGraph.foldHom_mapE_eq {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) :
      (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapE f₁ = (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapE f₂

      The two selected darts have the same image in the fold.

      source
      theorem TauCeti.StallingsGraph.foldHom_mapV_tgt_eq {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) :
      (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapV (S.graph.tgt f₁) = (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapV (S.graph.tgt f₂)

      The target vertices of the folded darts have the same image.

      source
      theorem TauCeti.StallingsGraph.foldHom_mapV_surjective {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) :
      Function.Surjective (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapV

      Every vertex of the fold comes from the original graph.

      source
      theorem TauCeti.StallingsGraph.connected_foldAt {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) (hS : S.graph.Connected) :
      (S.foldAt f₁ f₂ hsrc hlabel).graph.Connected

      A fold of a connected labelled graph remains connected.

      source
      theorem TauCeti.StallingsGraph.foldHom_mapE_surjective {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) :
      Function.Surjective (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapE

      Every dart of the fold comes from the original graph.

      source
      def TauCeti.StallingsGraph.foldLift {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) {T : StallingsGraph α} (g : S.Hom T) (h : g.graphHom.mapE f₁ = g.graphHom.mapE f₂) :
      (S.foldAt f₁ f₂ hsrc hlabel).Hom T

      A labelled morphism that identifies the folded darts factors through their fold.

      Instances For
        source
        @[simp]
        theorem TauCeti.StallingsGraph.foldLift_mapV_foldHom {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) {T : StallingsGraph α} (g : S.Hom T) (h : g.graphHom.mapE f₁ = g.graphHom.mapE f₂) (x : S.graph.V) :
        (S.foldLift f₁ f₂ hsrc hlabel g h).graphHom.mapV ((S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapV x) = g.graphHom.mapV x

        The lifted vertex map computes on vertices from the original graph.

        source
        @[simp]
        theorem TauCeti.StallingsGraph.foldLift_mapE_foldHom {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) {T : StallingsGraph α} (g : S.Hom T) (h : g.graphHom.mapE f₁ = g.graphHom.mapE f₂) (e : S.graph.E) :
        (S.foldLift f₁ f₂ hsrc hlabel g h).graphHom.mapE ((S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapE e) = g.graphHom.mapE e

        The lifted dart map computes on darts from the original graph.

        source
        @[simp]
        theorem TauCeti.StallingsGraph.foldLift_comp_foldHom {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) {T : StallingsGraph α} (g : S.Hom T) (h : g.graphHom.mapE f₁ = g.graphHom.mapE f₂) :
        (S.foldLift f₁ f₂ hsrc hlabel g h).comp (S.foldHom f₁ f₂ hsrc hlabel) = g

        Composing the fold quotient with its descended morphism recovers the original map.

        source
        theorem TauCeti.StallingsGraph.foldHom_ext {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) {T : StallingsGraph α} {k k' : (S.foldAt f₁ f₂ hsrc hlabel).Hom T} (hkk : k.comp (S.foldHom f₁ f₂ hsrc hlabel) = k'.comp (S.foldHom f₁ f₂ hsrc hlabel)) :
        k = k'

        Morphisms out of a fold agree if they agree after composition with its quotient map.

        source
        theorem TauCeti.StallingsGraph.foldLift_unique {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) {T : StallingsGraph α} (g : S.Hom T) (h : g.graphHom.mapE f₁ = g.graphHom.mapE f₂) (k : (S.foldAt f₁ f₂ hsrc hlabel).Hom T) (hk : k.comp (S.foldHom f₁ f₂ hsrc hlabel) = g) :
        k = S.foldLift f₁ f₂ hsrc hlabel g h

        The lift is the unique morphism whose composite with the quotient map is g.

        source
        instance TauCeti.StallingsGraph.instFiniteVGraphFoldAt {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) [Finite S.graph.V] :
        Finite (S.foldAt f₁ f₂ hsrc hlabel).graph.V

        A fold of a graph with finitely many vertices has finitely many vertices.

        source
        instance TauCeti.StallingsGraph.instFiniteEGraphFoldAt {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) [Finite S.graph.E] :
        Finite (S.foldAt f₁ f₂ hsrc hlabel).graph.E

        A fold of a graph with finitely many darts has finitely many darts.