The Möbius function of the lattice of graphs on a fixed vertex set

The simple graphs on a finite vertex set V form a Boolean lattice, isomorphic through the edge set to the lattice of subsets of the non-diagonal pairs Sym2 V. Its Möbius function is therefore the signed count (-1)^{e(H) - e(F)} on an interval [F, H], where e(·) counts edges. The two lemmas here are the cancellation laws that drive Möbius inversion over graphs, as in the transform between a graph parameter and its "contains exactly" coefficients.

Main results

• SimpleGraph.sum_neg_one_pow_ncard_edgeSet_sub_left — the signed sum ∑_{F ≤ G ≤ H} (-1)^{e(G) - e(F)} is 1 if F = H and 0 otherwise;
• SimpleGraph.sum_neg_one_pow_ncard_edgeSet_sub_right — the same for (-1)^{e(H) - e(G)}.

They are the graph counterparts of Finset.sum_Icc_neg_one_pow_card_sub_card_left and Finset.sum_Icc_neg_one_pow_card_sub_card_right, to which SimpleGraph.sum_filter_le_le_eq_sum_Icc_edgeFinset identifies them.

In matrix form, the two cancellation laws say that the zeta matrix Z(G, H) = [G ≤ H] of the lattice and its Möbius matrix M(G, H) = [G ≤ H] (-1)^{e(H) - e(G)} are inverse to each other, on either side. Expanding a function of graphs in the "contains" basis is multiplication by Z, and recovering its "contains exactly" coefficients is multiplication by M.

Main definitions

• SimpleGraph.zetaMatrix — the zeta matrix of the lattice of graphs on V;
• SimpleGraph.mobiusMatrix — its Möbius matrix.

Main results

• SimpleGraph.mobiusMatrix_mul_zetaMatrix and SimpleGraph.zetaMatrix_mul_mobiusMatrix — the two matrices are inverse to each other.

@[simp]

theorem SimpleGraph.sum_neg_one_pow_ncard_edgeSet_sub_left {V : Type u_1} {R : Type u_2} [Fintype V] [DecidableEq V] [Ring R] (F H : SimpleGraph V) [DecidablePred fun (G : SimpleGraph V) => F ≤ G ∧ G ≤ H] [Decidable (F = H)] : ∑ G : SimpleGraph V with F ≤ G ∧ G ≤ H, (-1) ^ (G.edgeSet.ncard - F.edgeSet.ncard) = if F = H then 1 else 0

The Möbius function of the lattice of graphs, measured from the bottom. The signed sum ∑_{F ≤ G ≤ H} (-1)^{e(G) - e(F)} is 1 if F = H and 0 otherwise.

@[simp]

theorem SimpleGraph.sum_neg_one_pow_ncard_edgeSet_sub_right {V : Type u_1} {R : Type u_2} [Fintype V] [DecidableEq V] [Ring R] (F H : SimpleGraph V) [DecidablePred fun (G : SimpleGraph V) => F ≤ G ∧ G ≤ H] [Decidable (F = H)] : ∑ G : SimpleGraph V with F ≤ G ∧ G ≤ H, (-1) ^ (H.edgeSet.ncard - G.edgeSet.ncard) = if F = H then 1 else 0

The Möbius function of the lattice of graphs, measured from the top. The signed sum ∑_{F ≤ G ≤ H} (-1)^{e(H) - e(G)} is 1 if F = H and 0 otherwise.

The zeta and Möbius matrices

noncomputable def SimpleGraph.zetaMatrix (V : Type u_1) (R : Type u_2) [Zero R] [One R] : Matrix (SimpleGraph V) (SimpleGraph V) R

The zeta matrix of the lattice of graphs on V: its (G, H) entry is 1 when G ≤ H and 0 otherwise.

Equations

• SimpleGraph.zetaMatrix V R = Matrix.of fun (G H : SimpleGraph V) => if G ≤ H then 1 else 0

noncomputable def SimpleGraph.mobiusMatrix (V : Type u_1) (R : Type u_2) [Ring R] : Matrix (SimpleGraph V) (SimpleGraph V) R

The Möbius matrix of the lattice of graphs on V: its (G, H) entry is the Möbius function (-1)^{e(H) - e(G)} of the interval [G, H] when G ≤ H, and 0 otherwise. It is the inverse of SimpleGraph.zetaMatrix.

Equations

• SimpleGraph.mobiusMatrix V R = Matrix.of fun (G H : SimpleGraph V) => if G ≤ H then (-1) ^ (H.edgeSet.ncard - G.edgeSet.ncard) else 0

@[simp]

theorem SimpleGraph.zetaMatrix_apply {V : Type u_1} {R : Type u_2} [Zero R] [One R] (G H : SimpleGraph V) [Decidable (G ≤ H)] : zetaMatrix V R G H = if G ≤ H then 1 else 0

The entries of the zeta matrix.

@[simp]

theorem SimpleGraph.mobiusMatrix_apply {V : Type u_1} {R : Type u_2} [Ring R] (G H : SimpleGraph V) [Decidable (G ≤ H)] : mobiusMatrix V R G H = if G ≤ H then (-1) ^ (H.edgeSet.ncard - G.edgeSet.ncard) else 0

The entries of the Möbius matrix.

@[simp]

theorem SimpleGraph.mobiusMatrix_mul_zetaMatrix {V : Type u_1} {R : Type u_2} [Fintype V] [DecidableEq V] [Ring R] [DecidableEq (SimpleGraph V)] : mobiusMatrix V R * zetaMatrix V R = 1

Möbius inversion, matrix form. The Möbius matrix is a left inverse of the zeta matrix: this is the cancellation law SimpleGraph.sum_neg_one_pow_ncard_edgeSet_sub_left.

@[simp]

theorem SimpleGraph.zetaMatrix_mul_mobiusMatrix {V : Type u_1} {R : Type u_2} [Fintype V] [DecidableEq V] [Ring R] [DecidableEq (SimpleGraph V)] : zetaMatrix V R * mobiusMatrix V R = 1

Möbius inversion, matrix form. The Möbius matrix is a right inverse of the zeta matrix: this is the cancellation law SimpleGraph.sum_neg_one_pow_ncard_edgeSet_sub_right.