Square of a graph

DefinitionSquare of a graph#✓fully proved

The square of a simple graph \(G\) is the simple graph on the same vertex set in which two distinct vertices \(u\) and \(v\) are adjacent when they are adjacent in \(G\) or have a common neighbor in \(G\), that is, a vertex \(w\) adjacent in \(G\) to both \(u\) and \(v\).

public def square {V : Type*} (G : SimpleGraph V) : SimpleGraph V where
  Adj u v := u ≠ v ∧ (G.Adj u v ∨ ∃ w, G.Adj u w ∧ G.Adj w v)
  symm := ⟨fun _ _ h ↦ ⟨h.1.symm, h.2.elim (fun huv ↦ Or.inl huv.symm)
    (fun ⟨w, huw, hwv⟩ ↦ Or.inr ⟨w, hwv.symm, huw.symm⟩)⟩⟩
  loopless := ⟨fun _ h ↦ h.1 rfl⟩

Used by 12

Used byFleischner's theorem · Strengthened Fleischner theorem · Strong square cycle at a vertex · Characterization of strong square cycles · Characterization of the graph square · Minimum degree in the square of a 2-connected graph · Skipping a vertex of a walk in the graph square · The square of a connected graph is connected · Adjacency in the graph square · Monotonicity of the graph square · Adding edges preserves a Hamiltonian square · A cyclic listing by square adjacencies gives a Hamiltonian square

TheoremAdjacency in the graph square#✓fully proved

For a simple graph \(G\) and vertices \(u\) and \(v\), the vertices \(u\) and \(v\) are adjacent in the square of \(G\) if and only if \(u \ne v\) and either \(u\) and \(v\) are adjacent in \(G\) or there is a vertex \(w\) with \(u\) adjacent to \(w\) and \(w\) adjacent to \(v\) in \(G\).

@[simp]
public theorem square_adj {V : Type*} (G : SimpleGraph V) (u v : V) :
    G.square.Adj u v ↔ u ≠ v ∧ (G.Adj u v ∨ ∃ w, G.Adj u w ∧ G.Adj w v)

Uses 1 · Used by 2

Statement usesSquare of a graph

Used byStrengthened Fleischner theorem · Characterization of the graph square

TheoremMonotonicity of the graph square#✓fully proved

Let \(G\) and \(H\) be simple graphs on the same vertex set such that every edge of \(G\) is an edge of \(H\). Then every edge of the square of \(G\) is an edge of the square of \(H\).

public theorem square_mono {V : Type*} {G H : SimpleGraph V} (hGH : G ≤ H) :
    G.square ≤ H.square

Uses 1 · Used by 1

Statement usesSquare of a graph

Used byAdding edges preserves a Hamiltonian square

TheoremThe square of a connected graph is connected#✓fully proved

If a simple graph \(G\) is connected, then the square of \(G\) is connected.

public theorem Connected.square {V : Type*} {G : SimpleGraph V} (hG : G.Connected) :
    G.square.Connected

Uses 1

Statement usesSquare of a graph

TheoremAdding edges preserves a Hamiltonian square#✓fully proved

Let \(G\) and \(H\) be simple graphs on the same finite vertex set such that every edge of \(G\) is an edge of \(H\). If the square of \(G\) is Hamiltonian, then the square of \(H\) is Hamiltonian.

public theorem IsHamiltonian.square_mono {V : Type*} [Fintype V] [DecidableEq V]
    {G H : SimpleGraph V}
    (hGH : G ≤ H) (hG : G.square.IsHamiltonian) : H.square.IsHamiltonian

Uses 2

Statement usesSquare of a graph

Proof usesMonotonicity of the graph square

TheoremCharacterization of the graph square#✓fully proved

Let \(G\) and \(H\) be simple graphs on the same vertex set. Then \(H\) equals the square of \(G\) if and only if, for all vertices \(u\) and \(v\), the vertices \(u\) and \(v\) are adjacent in \(H\) exactly when \(u \ne v\) and either \(u\) and \(v\) are adjacent in \(G\) or there is a vertex \(w\) with \(u\) adjacent to \(w\) and \(w\) adjacent to \(v\) in \(G\).

public theorem eq_square_iff {V : Type*} {G H : SimpleGraph V} :
    H = G.square ↔
      ∀ u v, H.Adj u v ↔ u ≠ v ∧ (G.Adj u v ∨ ∃ w, G.Adj u w ∧ G.Adj w v)

Uses 2 · Used by 1

Statement usesSquare of a graph

Proof usesAdjacency in the graph square

Used byFleischner's theorem

TheoremSkipping a vertex of a walk in the graph square#✓fully proved

Let \(G\) be a simple graph and let \(u, w, v, x_1, \dots, x_k\) (with \(k \ge 0\)) be a sequence of vertices in which consecutive vertices are adjacent in \(G\). If \(u \ne v\), then in the sequence \(u, v, x_1, \dots, x_k\) consecutive vertices are adjacent in the square of \(G\).

public theorem isChain_square_of_isChain_cons_cons {V : Type*} {G : SimpleGraph V}
    {u w v : V} {l : List V} (hchain : List.IsChain G.Adj (u :: w :: v :: l))
    (huv : u ≠ v) : List.IsChain G.square.Adj (u :: v :: l)

Uses 1

Statement usesSquare of a graph

TheoremA cyclic listing by square adjacencies gives a Hamiltonian square#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\), and let \(v_0, v_1, \dots, v_n\) be vertices with \(n \ge 3\) and \(v_0 = v_n\), such that \(v_1, \dots, v_n\) are pairwise distinct and every vertex of \(V\) is among them. If for each \(i < n\) the vertices \(v_i\) and \(v_{i+1}\) are distinct and either adjacent in \(G\) or have a common neighbor in \(G\), then the square of \(G\) is Hamiltonian.

public theorem IsHamiltonian.square_of_cyclic_list {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) (l : List V) (hne : l ≠ [])
    (hclosed : l.head hne = l.getLast hne)
    (hsteps : l.IsChain fun u v ↦
      u ≠ v ∧ (G.Adj u v ∨ ∃ w, G.Adj u w ∧ G.Adj w v))
    (hnodup : l.tail.Nodup) (hmem : ∀ v, v ∈ l.tail)
    (hthree : 3 ≤ l.length - 1) : G.square.IsHamiltonian

Uses 2

Statement usesSquare of a graph

Proof usesA cyclic listing of the vertices gives a Hamiltonian cycle

TheoremMinimum degree in the square of a 2-connected graph#✓fully proved

In a 2-vertex-connected simple graph on a finite vertex set with at least five vertices, every vertex has at least four neighbors in the square of the graph.

public theorem IsVertexConnected.four_le_square_degree
    {V : Type*} [Fintype V] {G : SimpleGraph V}
    [DecidableRel G.square.Adj] (hG : G.IsVertexConnected 2)
    (hcard : 5 ≤ Fintype.card V) (v : V) : 4 ≤ G.square.degree v

Uses 4

Statement uses\(k\)-vertex-connected graph · Square of a graph

Proof usesDeleting fewer than \(k\) vertices from a \(k\)-vertex-connected graph · Degrees in a 2-vertex-connected graph are at least two

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.