Cycle covers

StructureCycles in a graph#✓fully proved

A cycle in a simple graph \(G\) consists of a base vertex \(v\) of \(G\) together with a closed walk \(v = v_0, v_1, \dots, v_n = v\) in \(G\) such that \(n \ge 1\), the \(n\) edges \(v_{k-1} v_k\) of the walk are pairwise distinct, and the vertices \(v_1, \dots, v_n\) are pairwise distinct. In a simple graph this forces \(n \ge 3\).

The base vertex and the direction of traversal are part of the data, so a single cycle subgraph of \(G\) arises from several such cycles.

structure Cycle (G : SimpleGraph V) where
  base : V
  walk : G.Walk base base
  isCycle : walk.IsCycle

Used by 4

Used byEdges of a cycle · Cycle covers · Length of a cycle · Total length of a multiset of cycles

DefinitionEdges of a cycle#✓fully proved

The edges of a cycle \(c\) in a simple graph form the list of the edges of its closed walk, in the order in which \(c\) traverses them starting from its base vertex; each edge is the unordered pair of its two endpoints.

def Cycle.edges {G : SimpleGraph V} (c : Cycle G) : List (Sym2 V) :=
  c.walk.edges

Uses 1 · Used by 1

Statement usesCycles in a graph

Used byCycle covers

DefinitionLength of a cycle#✓fully proved

The length of a cycle in a simple graph is the number of edges of its closed walk.

def Cycle.length {G : SimpleGraph V} (c : Cycle G) : ℕ :=
  c.walk.length

Uses 1 · Used by 1

Statement usesCycles in a graph

Used byTotal length of a multiset of cycles

DefinitionCycle covers#✓fully proved

Let \(G\) be a finite simple graph. A finite multiset \(C\) of cycles in \(G\) is a cycle cover of \(G\) when every edge of \(G\) is an edge of at least one cycle in \(C\).

def IsCycleCover (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
    (C : Multiset (Cycle G)) : Prop :=
  ∀ e ∈ G.edgeFinset, ∃ c ∈ C, e ∈ c.edges

Uses 2

Statement usesCycles in a graph · Edges of a cycle

DefinitionTotal length of a multiset of cycles#✓fully proved

The total length of a finite multiset \(C\) of cycles in a simple graph is the sum of the lengths of the cycles in \(C\), each counted with its multiplicity.

def totalLength {G : SimpleGraph V} (C : Multiset (Cycle G)) : ℕ :=
  (C.map Cycle.length).sum

Uses 2

Statement usesCycles in a graph · Length of a cycle

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.