Strongly regular graphs #
Main definitions #
G.IsSRGWith n k ℓ μ(seeSimpleGraph.IsSRGWith) is a structure for aSimpleGraphsatisfying the following conditions:- The cardinality of the vertex set is
n Gis a regular graph with degreek- The number of common neighbors between any two adjacent vertices in
Gisℓ - The number of common neighbors between any two nonadjacent vertices in
Gisμ
- The cardinality of the vertex set is
Main theorems #
IsSRGWith.compl: the complement of a strongly regular graph is strongly regular.IsSRGWith.param_eq:k * (k - ℓ - 1) = (n - k - 1) * μwhen0 < n.IsSRGWith.matrix_eq: letAandCbeG's andGᶜ's adjacency matrices respectively andIbe the identity matrix, thenA ^ 2 = k • I + ℓ • A + μ • C.
structure
SimpleGraph.IsSRGWith
{V : Type u}
[Fintype V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(n : ℕ)
(k : ℕ)
(ℓ : ℕ)
(μ : ℕ)
:
A graph is strongly regular with parameters n k ℓ μ if
- its vertex set has cardinality
n - it is regular with degree
k - every pair of adjacent vertices has
ℓcommon neighbors - every pair of nonadjacent vertices has
μcommon neighbors
- card : Fintype.card V = n
- regular : G.IsRegularOfDegree k
- of_adj : ∀ (v w : V), G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = ℓ
- of_not_adj : Pairwise fun (v w : V) => ¬G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = μ
theorem
SimpleGraph.IsSRGWith.card
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
(self : G.IsSRGWith n k ℓ μ)
:
Fintype.card V = n
theorem
SimpleGraph.IsSRGWith.regular
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
(self : G.IsSRGWith n k ℓ μ)
:
G.IsRegularOfDegree k
theorem
SimpleGraph.IsSRGWith.of_adj
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
(self : G.IsSRGWith n k ℓ μ)
(v : V)
(w : V)
:
G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = ℓ
theorem
SimpleGraph.IsSRGWith.of_not_adj
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
(self : G.IsSRGWith n k ℓ μ)
:
Pairwise fun (v w : V) => ¬G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = μ
theorem
SimpleGraph.bot_strongly_regular
{V : Type u}
[Fintype V]
{ℓ : ℕ}
:
⊥.IsSRGWith (Fintype.card V) 0 ℓ 0
Empty graphs are strongly regular. Note that ℓ can take any value
for empty graphs, since there are no pairs of adjacent vertices.
theorem
SimpleGraph.IsSRGWith.top
{V : Type u}
[Fintype V]
{μ : ℕ}
[DecidableEq V]
:
⊤.IsSRGWith (Fintype.card V) (Fintype.card V - 1) (Fintype.card V - 2) μ
Complete graphs are strongly regular. Note that μ can take any value
for complete graphs, since there are no distinct pairs of non-adjacent vertices.
theorem
SimpleGraph.IsSRGWith.card_neighborFinset_union_eq
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
[DecidableEq V]
{v : V}
{w : V}
(h : G.IsSRGWith n k ℓ μ)
:
(G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - Fintype.card ↑(G.commonNeighbors v w)
theorem
SimpleGraph.IsSRGWith.card_neighborFinset_union_of_not_adj
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
[DecidableEq V]
{v : V}
{w : V}
(h : G.IsSRGWith n k ℓ μ)
(hne : v ≠ w)
(ha : ¬G.Adj v w)
:
Assuming G is strongly regular, 2*(k + 1) - m in G is the number of vertices that are
adjacent to either v or w when ¬G.Adj v w. So it's the cardinality of
G.neighborSet v ∪ G.neighborSet w.
theorem
SimpleGraph.IsSRGWith.card_neighborFinset_union_of_adj
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
[DecidableEq V]
{v : V}
{w : V}
(h : G.IsSRGWith n k ℓ μ)
(ha : G.Adj v w)
:
theorem
SimpleGraph.compl_neighborFinset_sdiff_inter_eq
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[DecidableEq V]
{v : V}
{w : V}
:
theorem
SimpleGraph.sdiff_compl_neighborFinset_inter_eq
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[DecidableEq V]
{v : V}
{w : V}
(h : G.Adj v w)
:
theorem
SimpleGraph.IsSRGWith.compl_is_regular
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
[DecidableEq V]
(h : G.IsSRGWith n k ℓ μ)
:
theorem
SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_adj_compl
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
[DecidableEq V]
(h : G.IsSRGWith n k ℓ μ)
{v : V}
{w : V}
(ha : Gᶜ.Adj v w)
:
theorem
SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_not_adj_compl
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
[DecidableEq V]
(h : G.IsSRGWith n k ℓ μ)
{v : V}
{w : V}
(hn : v ≠ w)
(hna : ¬Gᶜ.Adj v w)
:
theorem
SimpleGraph.IsSRGWith.compl
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
[DecidableEq V]
(h : G.IsSRGWith n k ℓ μ)
:
The complement of a strongly regular graph is strongly regular.
theorem
SimpleGraph.IsSRGWith.param_eq
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
{V : Type u}
[Fintype V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(h : G.IsSRGWith n k ℓ μ)
(hn : 0 < n)
:
The parameters of a strongly regular graph with at least one vertex satisfy
k * (k - ℓ - 1) = (n - k - 1) * μ.
theorem
SimpleGraph.IsSRGWith.matrix_eq
{V : Type u}
[Fintype V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
{n : ℕ}
{k : ℕ}
{ℓ : ℕ}
{μ : ℕ}
[DecidableEq V]
{α : Type u_1}
[Semiring α]
(h : G.IsSRGWith n k ℓ μ)
:
SimpleGraph.adjMatrix α G ^ 2 = k • 1 + ℓ • SimpleGraph.adjMatrix α G + μ • SimpleGraph.adjMatrix α Gᶜ
Let A and C be the adjacency matrices of a strongly regular graph with parameters n k ℓ μ
and its complement respectively and I be the identity matrix,
then A ^ 2 = k • I + ℓ • A + μ • C. C is equivalent to the expression J - I - A
more often found in the literature, where J is the all-ones matrix.