Zero-divisor graph

AbbreviationNonzero zero divisors#✓fully proved

For a commutative ring \(R\), this is the set of elements \(r \in R\) with \(r \neq 0\) such that \(sr = 0\) for some nonzero \(s \in R\), that is, the nonzero zero divisors of \(R\). They are the vertices of the zero-divisor graph of \(R\).

public abbrev Vertex (R : Type u) [CommRing R] :
    Type u := { r : R // r ≠ 0 ∧ r ∉ nonZeroDivisors R }

Used by 3

Used byAdjacency in the zero-divisor graph · Vertices are the nonzero zero divisors · The zero-divisor graph

DefinitionThe zero-divisor graph#✓fully proved

For a commutative ring \(R\), the zero-divisor graph of \(R\) is the simple graph whose vertices are the nonzero zero divisors of \(R\), in which two distinct vertices \(v\) and \(w\) are adjacent exactly when \(vw = 0\).

public def zeroDivisorGraph (R : Type u) [CommRing R] :
    SimpleGraph (Vertex R) :=
  SimpleGraph.fromRel fun v w : Vertex R => (v : R) * (w : R) = 0

Uses 1 · Used by 1

Statement usesNonzero zero divisors

Used byAdjacency in the zero-divisor graph

TheoremVertices are the nonzero zero divisors#✓fully proved

Let \(R\) be a commutative ring. An element \(r \in R\) is a vertex of the zero-divisor graph of \(R\) if and only if \(r \neq 0\) and \(r\) is a zero divisor, that is, \(sr = 0\) for some nonzero \(s \in R\).

public theorem exists_vertex_iff (R : Type u) [CommRing R] (r : R) :
    (∃ v : Vertex R, (v : R) = r) ↔ (r ≠ 0 ∧ r ∉ nonZeroDivisors R)

Uses 1

Statement usesNonzero zero divisors

TheoremAdjacency in the zero-divisor graph#✓fully proved

Let \(R\) be a commutative ring. Two vertices \(v\) and \(w\) of the zero-divisor graph of \(R\) are adjacent if and only if \(v \neq w\) and \(vw = 0\).

public theorem adj_iff (R : Type u) [CommRing R]
    {v w : Vertex R} :
    (zeroDivisorGraph R).Adj v w ↔ v ≠ w ∧ (v : R) * (w : R) = 0

Uses 2

Statement usesNonzero zero divisors · The zero-divisor graph

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.