Binomial Edge Ideals

What Is A Binomial Edge Ideal?

To a simple graph $G$ on vertices ${1, \dots, n}$, the binomial edge ideal $J_G$ attaches one binomial per edge:

\[J_G \;=\; \langle\, x_i y_j - x_j y_i \;:\; \{i, j\} \in E(G) \,\rangle \;\subseteq\; K[x_1, \dots, x_n, y_1, \dots, y_n].\]

The paper approaches these ideals from three sides: when the given generators already form a Gröbner basis, how the prime decomposition is controlled by the graph, and how the same ideals arise from conditional independence statements in algebraic statistics. Every result on this site links to the Lean file that verifies it.

$f_{12} \,=\, x_1 y_2 - x_2 y_1$

$f_{23} \,=\, x_2 y_3 - x_3 y_2$

$f_{34} \,=\, x_3 y_4 - x_4 y_3$

$J_{P_4} \,=\, \langle\, f_{12},\; f_{23},\; f_{34}\, \rangle$

A path on four vertices, and the three quadratic generators of its binomial edge ideal.

Definitions In Lean

These are the formal counterparts of the objects above. The first three live in BEI/Definitions.lean and the last in BEI/MonomialOrder.lean. The Foundations page tabulates the supporting infrastructure (generators $f_{ij}$, leading-term lemmas, the closure construction).

variable {K : Type*} [Field K] {V : Type*} [LinearOrder V]

def BinomialEdgeVars (V : Type*) := V ⊕ V

def binomialEdgeIdeal (G : SimpleGraph V) :
    Ideal (MvPolynomial (BinomialEdgeVars V) K) :=
  Ideal.span { f | ∃ i j, G.Adj i j ∧ i < j ∧ f = x i * y j - x j * y i }

def IsClosedGraph (G : SimpleGraph V) : Prop :=
  (∀ {i j k : V}, i < j → i < k → j ≠ k → G.Adj i j → G.Adj i k → G.Adj j k) ∧
  (∀ {i j k : V}, i < k → j < k → i ≠ j → G.Adj i k → G.Adj j k → G.Adj i j)

noncomputable def binomialEdgeMonomialOrder :
    MonomialOrder (BinomialEdgeVars V) := MonomialOrder.lex

In order: the index type for the two copies of variables $x_i$, $y_i$ (encoded as $V \oplus V$); the ideal $J_G$; the closed-graph condition that characterizes when the quadratic generators form a Gröbner basis (Theorem 1.1); and the lexicographic monomial order from the paper, $x_1 > \cdots > x_n > y_1 > \cdots > y_n$.

Sections

Foundations Definitions, term order, and Gröbner setup The graph, the polynomial ring, and the lex term order — the objects everything else is built from. Section 1 Closed graphs and quadratic Gröbner bases When do the edge binomials already form a Gröbner basis? A graph-theoretic answer, plus the Cohen–Macaulay criterion. Section 2 Reduced Gröbner basis and radicality The edge binomials give a reduced Gröbner basis, and $J_G$ turns out to be a radical ideal. Section 3 Prime decomposition, dimension, minimal primes Prime decomposition, Krull dimension, and minimal primes — all described directly from the graph. Section 4 Conditional independence ideals and robustness Binomial edge ideals reappear as conditional independence ideals in algebraic statistics.

A Taste Of The Formalization

Each card has the paper’s statement on the left and the formal Lean theorem on the right. Click through to open the Lean file and read the full proof.

Paper

The quadratic generators of $J_G$ form a Gröbner basis for the lexicographic order $x_1 > \cdots > x_n > y_1 > \cdots > y_n$ if and only if $G$ is closed.

Lean

theorem_1_1

theorem theorem_1_1 (G : SimpleGraph V) :
    binomialEdgeMonomialOrder.IsGroebnerBasis (generatorSet (K := K) G)
      (binomialEdgeIdeal (K := K) G) ↔
    IsClosedGraph G :=
  ⟨groebner_implies_closed G, closed_implies_groebner G⟩

View proof in ClosedGraphs.lean

Paper

The binomial edge ideal $J_G$ is radical.

Lean

corollary_2_2

theorem corollary_2_2 (G : SimpleGraph V) :
    (binomialEdgeIdeal (K := K) G).IsRadical := by

View proof in Radical.lean

Paper

The binomial edge ideal decomposes as $J_G = \bigcap_{S \subseteq V(G)} P_S(G)$.

Lean

theorem_3_2

theorem theorem_3_2 (G : SimpleGraph V) :
    binomialEdgeIdeal (K := K) G =
      ⨅ S : Finset V, primeComponent (K := K) G S := by

View proof in PrimeDecomposition.lean

Paper

If $S / J_G$ is Cohen--Macaulay and $G$ has $n$ vertices and $c$ connected components, then $\dim(S / J_G) = n + c$.

Lean

corollary_3_4

theorem corollary_3_4 (G : SimpleGraph V)
    (hCM : IsCohenMacaulayRing
      (MvPolynomial (BinomialEdgeVars V) K ⧸ binomialEdgeIdeal (K := K) G)) :
    ringKrullDim
      (MvPolynomial (BinomialEdgeVars V) K ⧸ binomialEdgeIdeal (K := K) G) =
      ↑(Fintype.card V + numConnectedComponents G)

View proof in Corollary3_4.lean

Paper

For a binary-output robustness specification, the conditional independence ideal equals the binomial edge ideal of the associated union graph.

Lean

ciIdealSpec_eq_binomialEdgeIdeal

theorem ciIdealSpec_eq_binomialEdgeIdeal (stmt : ι → CIStatement Ω) :
    (ciIdealSpec stmt : Ideal (MvPolynomial (BinomialEdgeVars Ω) K)) =
    binomialEdgeIdeal (ciGraphSpec stmt) := by

View proof in CIIdeals.lean

Project Links

Code map Lean files Supporting library Mastodon