Documentation

TauCeti.Combinatorics.SimpleGraph.ComponentRoot

Roots and paths to them in the connected components of a graph #

Every connected component of a simple graph has a representative vertex, and every vertex of the graph is joined to the representative of its component by a walk. Choosing these once for all, as the representatives themselves are not canonical, gives a root for every vertex together with a root path from that root to the vertex. Two adjacent vertices lie in the same connected component, so they have the same root.

These choices are the scaffolding for the statements which integrate a quantity along a path from a root in every connected component: the product of the values of a 1-cochain along the root path of a vertex, or the product of transition factors along it.

Main definitions #

Main results #

source
noncomputable def SimpleGraph.componentRoot {V : Type u} (G : SimpleGraph V) (v : V) :
V

The chosen root of the connected component of a vertex.

Equations
Instances For
    source
    theorem SimpleGraph.reachable_componentRoot {V : Type u} (G : SimpleGraph V) (v : V) :
    G.Reachable (G.componentRoot v) v

    The root of the connected component of a vertex reaches it.

    source
    noncomputable def SimpleGraph.componentPath {V : Type u} (G : SimpleGraph V) (v : V) :
    G.Walk (G.componentRoot v) v

    A chosen walk from the root of the connected component of a vertex to that vertex.

    Equations
    Instances For
      source
      theorem SimpleGraph.isPath_componentPath {V : Type u} (G : SimpleGraph V) (v : V) :
      (G.componentPath v).IsPath

      The chosen walk from the root of a connected component to a vertex is a path.

      source
      theorem SimpleGraph.componentRoot_eq_of_adj {V : Type u} (G : SimpleGraph V) {v w : V} (h : G.Adj v w) :
      G.componentRoot w = G.componentRoot v

      The roots of adjacent vertices are the same.