Strongly regular graphs

Main definitions

• G.IsSRGWith n k ℓ μ (see SimpleGraph.IsSRGWith) is a structure for a SimpleGraph satisfying the following conditions:
  • The cardinality of the vertex set is n
  • G is a regular graph with degree k
  • The number of common neighbors between any two adjacent vertices in G is ℓ
  • The number of common neighbors between any two nonadjacent vertices in G is μ

Main theorems

• IsSRGWith.compl: the complement of a strongly regular graph is strongly regular.
• IsSRGWith.param_eq: k * (k - ℓ - 1) = (n - k - 1) * μ when 0 < n.
• IsSRGWith.matrix_eq: let A and C be G's and Gᶜ's adjacency matrices respectively and I be the identity matrix, then A ^ 2 = k • I + ℓ • A + μ • C.

structure SimpleGraph.IsSRGWith {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (n : ℕ) (k : ℕ) (ℓ : ℕ) (μ : ℕ) : Prop

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] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : ℕ} {k : ℕ} {ℓ : ℕ} {μ : ℕ} {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] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : ℕ} {k : ℕ} {ℓ : ℕ} {μ : ℕ} {v : V} {w : V} (h : G.IsSRGWith n k ℓ μ) (hne : v ≠ w) (ha : ¬G.Adj v w) : (G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - μ

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] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : ℕ} {k : ℕ} {ℓ : ℕ} {μ : ℕ} {v : V} {w : V} (h : G.IsSRGWith n k ℓ μ) (ha : G.Adj v w) : (G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - ℓ

theorem SimpleGraph.compl_neighborFinset_sdiff_inter_eq {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {v : V} {w : V} : (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) = ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})

theorem SimpleGraph.sdiff_compl_neighborFinset_inter_eq {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {v : V} {w : V} (h : G.Adj v w) : ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v}) = (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

theorem SimpleGraph.IsSRGWith.compl_is_regular {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : ℕ} {k : ℕ} {ℓ : ℕ} {μ : ℕ} (h : G.IsSRGWith n k ℓ μ) : Gᶜ.IsRegularOfDegree (n - k - 1)

theorem SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_adj_compl {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : ℕ} {k : ℕ} {ℓ : ℕ} {μ : ℕ} (h : G.IsSRGWith n k ℓ μ) {v : V} {w : V} (ha : Gᶜ.Adj v w) : Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2

theorem SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_not_adj_compl {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : ℕ} {k : ℕ} {ℓ : ℕ} {μ : ℕ} (h : G.IsSRGWith n k ℓ μ) {v : V} {w : V} (hn : v ≠ w) (hna : ¬Gᶜ.Adj v w) : Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - ℓ)

theorem SimpleGraph.IsSRGWith.compl {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : ℕ} {k : ℕ} {ℓ : ℕ} {μ : ℕ} (h : G.IsSRGWith n k ℓ μ) : Gᶜ.IsSRGWith n (n - k - 1) (n - (2 * k - μ) - 2) (n - (2 * k - ℓ))

The complement of a strongly regular graph is strongly regular.

theorem SimpleGraph.IsSRGWith.param_eq {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : ℕ} {k : ℕ} {ℓ : ℕ} {μ : ℕ} (h : G.IsSRGWith n k ℓ μ) (hn : 0 < n) : k * (k - ℓ - 1) = (n - k - 1) * μ

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] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : ℕ} {k : ℕ} {ℓ : ℕ} {μ : ℕ} {α : 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.