Bass's determinant formula for the Ihara zeta function

For a finite simple graph with adjacency matrix A, degree matrix D and non-backtracking (Hashimoto) operator B on darts, and u in a field,

(1 - u²)^|V| · det(1 - u B) = (1 - u²)^|E| · det(1 - u A + u² (D - 1)).

The left determinant is the reciprocal of the Ihara zeta function. The proof writes B = Tᵀ S - J with the start and terminus incidence matrices S, T and the dart reversal J, computes det(1 + u J) = (1 - u²)^|E| through the splitting of darts into positively and negatively oriented ones, and applies Sylvester's determinant identity.

Main definitions

• SimpleGraph.reversal, SimpleGraph.hashimoto, SimpleGraph.startInc, SimpleGraph.termInc: the dart reversal, the non-backtracking operator and the start and terminus incidence matrices. The degree matrix is Mathlib's SimpleGraph.degMatrix.
• SimpleGraph.dartEquiv: G.Dart ≃ Bool × {positive darts} for a linear order on V.

Main results

• SimpleGraph.bass_determinant: Bass's determinant formula.

References

• H. Bass, The Ihara–Selberg zeta function of a tree lattice, Internat. J. Math. 3 (1992) 717–797.
• A. Terras, Zeta Functions of Graphs: A Stroll through the Garden, Cambridge University Press, 2011.

def SimpleGraph.reversal {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (R : Type u_2) [CommRing R] : Matrix G.Dart G.Dart R

The dart-reversal permutation matrix J: J d e = 1 iff e = d.symm.

Equations

• G.reversal R = Matrix.of fun (d e : G.Dart) => if e = d.symm then 1 else 0

def SimpleGraph.hashimoto {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (R : Type u_2) [CommRing R] : Matrix G.Dart G.Dart R

The Hashimoto / non-backtracking edge operator B: B d e = 1 iff the head of d is the tail of e and e is not the reverse of d (i.e. d may be followed by e without backtracking).

Equations

• G.hashimoto R = Matrix.of fun (d e : G.Dart) => if d.toProd.2 = e.toProd.1 ∧ e ≠ d.symm then 1 else 0

def SimpleGraph.startInc {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (R : Type u_2) [CommRing R] : Matrix V G.Dart R

Start incidence matrix S: S v d = 1 iff d originates at v.

Equations

• G.startInc R = Matrix.of fun (v : V) (d : G.Dart) => if d.toProd.1 = v then 1 else 0

def SimpleGraph.termInc {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (R : Type u_2) [CommRing R] : Matrix V G.Dart R

Terminus incidence matrix T: T v d = 1 iff d terminates at v.

Equations

• G.termInc R = Matrix.of fun (v : V) (d : G.Dart) => if d.toProd.2 = v then 1 else 0

Incidence layer — step 1 of the proof (all numerically pre-verified)

@[simp]

theorem SimpleGraph.startInc_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] (v : V) (d : G.Dart) : G.startInc R v d = if d.toProd.1 = v then 1 else 0

@[simp]

theorem SimpleGraph.termInc_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] (v : V) (d : G.Dart) : G.termInc R v d = if d.toProd.2 = v then 1 else 0

@[simp]

theorem SimpleGraph.reversal_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] (d e : G.Dart) : G.reversal R d e = if e = d.symm then 1 else 0

@[simp]

theorem SimpleGraph.hashimoto_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] (d e : G.Dart) : G.hashimoto R d e = if d.toProd.2 = e.toProd.1 ∧ e ≠ d.symm then 1 else 0

theorem SimpleGraph.adj_dart_card {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v w : V) : {d : G.Dart | d.toProd.1 = v ∧ d.toProd.2 = w}.card = if G.Adj v w then 1 else 0

Number of darts with prescribed endpoints (v, w) is 1 iff v ~ w.

theorem SimpleGraph.startInc_mul_termInc_transpose {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] : G.startInc R * (G.termInc R).transpose = adjMatrix R G

S Tᵀ = A: darts from v to w realise the adjacency matrix.

theorem SimpleGraph.startInc_mul_startInc_transpose {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] : G.startInc R * (G.startInc R).transpose = degMatrix R G

S Sᵀ = D: the start-incidence Gram matrix is the degree matrix.

theorem SimpleGraph.hashimoto_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] : G.hashimoto R = (G.termInc R).transpose * G.startInc R - G.reversal R

B = Tᵀ S − J: the Hashimoto operator removes backtracking from Tᵀ S.

theorem SimpleGraph.startInc_mul_reversal {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] : G.startInc R * G.reversal R = G.termInc R

S J = T: pre-composing start-incidence with reversal gives terminus-incidence.

theorem SimpleGraph.reversal_transpose {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] : (G.reversal R).transpose = G.reversal R

J is symmetric: reversal is its own transpose (since symm is an involution).

theorem SimpleGraph.reversal_mul_self {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] : G.reversal R * G.reversal R = 1

J² = I: reversal is an involution.

theorem SimpleGraph.termInc_mul_termInc_transpose {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] : G.termInc R * (G.termInc R).transpose = degMatrix R G

T Tᵀ = D: via T = S J, Jᵀ = J, J² = I, and S Sᵀ = D.

theorem SimpleGraph.one_add_smul_reversal_mul {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] (u : R) : (1 + u • G.reversal R) * (1 - u • G.reversal R) = (1 - u ^ 2) • 1

The algebraic heart of det(I + uJ) = (1 - u²)^m: (I + uJ)(I − uJ) = (1 − u²) I, since J² = I.

theorem SimpleGraph.det_one_add_smul_reversal_mul {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] (u : R) : (1 + u • G.reversal R).det * (1 - u • G.reversal R).det = (1 - u ^ 2) ^ Fintype.card G.Dart

Determinant consequence: det(I + uJ) · det(I − uJ) = (1 − u²)^{2m} (here 2m = |Dart|). The individual factor det(I + uJ) = (1 − u²)^m needs the orientation reindex Dart ≃ edges × Fin 2 — the next lemma.

Orientation reindex — toward det(I + uJ) = (1 - u²)^m

With a linear order on the vertices, each edge has a unique "positive" dart (tail < head); a general dart is that positive dart together with a sign bit. This realises Dart ≃ Bool × PosDart, under which J = reversal becomes a block-diagonal of 2×2 swaps — the route to det(I + uJ) = (1 - u²)^m.

def SimpleGraph.IsPos {V : Type u_1} (G : SimpleGraph V) [LinearOrder V] (d : G.Dart) : Prop

A dart is positive when its tail precedes its head.

Equations

• G.IsPos d = (d.toProd.1 < d.toProd.2)

@[instance_reducible]

instance SimpleGraph.instDecidablePredDartIsPos {V : Type u_1} (G : SimpleGraph V) [LinearOrder V] : DecidablePred G.IsPos

Equations

• G.instDecidablePredDartIsPos d = inferInstance

theorem SimpleGraph.isPos_symm_of_not {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [LinearOrder V] {d : G.Dart} (h : ¬G.IsPos d) : G.IsPos d.symm

If a dart is not positive, its reverse is.

def SimpleGraph.dartEquiv {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [LinearOrder V] : G.Dart ≃ Bool × { d : G.Dart // G.IsPos d }

Orientation reindex: a dart is a chosen positive dart plus a sign bit.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.card_posDart {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [LinearOrder V] : Fintype.card { d : G.Dart // G.IsPos d } = G.edgeFinset.card

The positive darts are in bijection with the edges: |PosDart| = |E|. Proof: dartEquiv gives |Dart| = 2·|PosDart|, and the handshake lemma gives |Dart| = 2·|E|; cancel the 2.

theorem SimpleGraph.dart_ne_symm {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [LinearOrder V] (d : G.Dart) : d ≠ d.symm

A dart never equals its own reverse.

@[simp]

theorem SimpleGraph.dartEquiv_symm_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [LinearOrder V] (b : Bool) (p : { d : G.Dart // G.IsPos d }) : G.dartEquiv.symm (b, p) = if b = true then ↑p else (↑p).symm

theorem SimpleGraph.dartEquiv_symm_symm {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [LinearOrder V] (b : Bool) (p : { d : G.Dart // G.IsPos d }) : (G.dartEquiv.symm (b, p)).symm = G.dartEquiv.symm (!b, p)

Reversing a dart flips the orientation bit.

def SimpleGraph.signBlock (R : Type u_2) [CommRing R] (u : R) : Matrix Bool Bool R

The 2×2 sign block [[1,u],[u,1]] (indexed by Bool).

Equations

• SimpleGraph.signBlock R u = Matrix.of fun (b1 b2 : Bool) => if b1 = b2 then 1 else u

@[simp]

theorem SimpleGraph.signBlock_apply (R : Type u_2) [CommRing R] (u : R) (b1 b2 : Bool) : signBlock R u b1 b2 = if b1 = b2 then 1 else u

theorem SimpleGraph.det_signBlock (R : Type u_2) [CommRing R] (u : R) : (signBlock R u).det = 1 - u ^ 2

theorem SimpleGraph.det_one_add_smul_reversal {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] [LinearOrder V] (u : R) : (1 + u • G.reversal R).det = (1 - u ^ 2) ^ G.edgeFinset.card

det(I + uJ) = (1 - u²)^m. Reindex by dartEquiv turns I + uJ into a block-diagonal of 2×2 sign blocks (one per edge); det_blockDiagonal then gives (det signBlock)^|E| = (1 - u²)^|E|.

theorem SimpleGraph.det_one_sub_smul_reversal {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] [LinearOrder V] (u : R) : (1 - u • G.reversal R).det = (1 - u ^ 2) ^ G.edgeFinset.card

det(I − uJ) = (1 − u²)^|E| (same blockDiagonal argument, via u ↦ -u).

theorem SimpleGraph.one_sub_smul_hashimoto {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] (u : R) : 1 - u • G.hashimoto R = 1 + u • G.reversal R - u • ((G.termInc R).transpose * G.startInc R)

I − uB = (I + uJ) − u·TᵀS, from B = TᵀS − J.

theorem SimpleGraph.startInc_mul_one_sub_smul_reversal_mul_termInc {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] (u : R) : G.startInc R * (1 - u • G.reversal R) * (G.termInc R).transpose = adjMatrix R G - u • degMatrix R G

S(I − uJ)Tᵀ = A − uD.

theorem SimpleGraph.bass_determinant {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [Field R] [LinearOrder V] (u : R) : (1 - u ^ 2) ^ Fintype.card V * (1 - u • G.hashimoto R).det = (1 - u ^ 2) ^ G.edgeFinset.card * (1 - u • adjMatrix R G + u ^ 2 • (degMatrix R G - 1)).det

Bass's determinant formula (division-free form, over a field).

(1 - u²)^|V| · det(I - u·B) = (1 - u²)^|E| · det(I - u·A + u²·(D - I)),

with B the Hashimoto operator on darts, A the adjacency matrix, D the degree matrix. Equivalent to det(I - uB) = (1-u²)^{|E|-|V|} det(I - uA + (D-I)u²). Proved over a field (the standard setting); the Sylvester step inverts I + uJ, which is a unit exactly when 1 - u² ≠ 0.