[Merged by Bors] - feat: matrix equality of strongly regular graphs

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

@@ -2406,6 +2406,17 @@ theorem set_walk_length_succ_eq (u v : V) (n : ℕ) :
 
 variable (G) [DecidableEq V]
 
+/-- Walks of length two from `u` to `v` correspond bijectively to common neighbours of `u` and `v`.
+Note that `u` and `v` may be the same. -/
+@[simps]
+def subtypeWalkLengthEqTwoEquivCommonNeighbors (u v : V) :
+    {p : G.Walk u v // p.length = 2} ≃ G.commonNeighbors u v where
+  toFun p := ⟨p.val.getVert 1, match p with
+    | ⟨.cons _ (.cons _ .nil), hp⟩ => ⟨‹G.Adj u _›, ‹G.Adj _ v›.symm⟩⟩
+  invFun w := ⟨w.prop.1.toWalk.concat w.prop.2.symm, rfl⟩
+  left_inv | ⟨.cons _ (.cons _ .nil), hp⟩ => by rfl
+  right_inv _ := rfl
+
 section LocallyFinite
 
 variable [LocallyFinite G]
@@ -2458,6 +2469,9 @@ instance fintypeSetWalkLength (u v : V) (n : ℕ) : Fintype {p : G.Walk u v | p.
     rw [← Finset.mem_coe, coe_finsetWalkLength_eq]
 #align simple_graph.fintype_set_walk_length SimpleGraph.fintypeSetWalkLength
 
+instance fintypeSubtypeWalkLength (u v : V) (n : ℕ) : Fintype {p : G.Walk u v // p.length = n} :=
+  fintypeSetWalkLength G u v n
+
 theorem set_walk_length_toFinset_eq (n : ℕ) (u v : V) :
     {p : G.Walk u v | p.length = n}.toFinset = G.finsetWalkLength n u v := by
   ext p

Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

@@ -1,11 +1,12 @@
 /-
 Copyright (c) 2021 Alena Gusakov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Alena Gusakov
+Authors: Alena Gusakov, Jeremy Tan
 -/
+import Mathlib.Combinatorics.DoubleCounting
+import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
 import Mathlib.Combinatorics.SimpleGraph.Basic
 import Mathlib.Data.Set.Finite
-import Mathlib.Combinatorics.DoubleCounting
 
 #align_import combinatorics.simple_graph.strongly_regular from "leanprover-community/mathlib"@"2b35fc7bea4640cb75e477e83f32fbd538920822"
 
@@ -21,9 +22,12 @@ import Mathlib.Combinatorics.DoubleCounting
   * 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 `μ`
 
-## TODO
-- Prove that if `I` is the identity matrix and `J` is the all-one matrix,
-  then the adj matrix `A` of SRG obeys relation `A^2 = kI + ℓA + μ(J - I - A)`
+## 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`.
 -/
 
 
@@ -206,4 +210,22 @@ theorem IsSRGWith.param_eq (h : G.IsSRGWith n k ℓ μ) (hn : 0 < n) :
       ← Set.toFinset_card]
     congr!
 
+/-- 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. -/
+theorem IsSRGWith.matrix_eq [Semiring α] (h : G.IsSRGWith n k ℓ μ) :
+    G.adjMatrix α ^ 2 = k • (1 : Matrix V V α) + ℓ • G.adjMatrix α + μ • Gᶜ.adjMatrix α := by
+  ext v w
+  simp only [adjMatrix_pow_apply_eq_card_walk, Set.coe_setOf, Matrix.add_apply, Matrix.smul_apply,
+    adjMatrix_apply, compl_adj]
+  rw [Fintype.card_congr (G.subtypeWalkLengthEqTwoEquivCommonNeighbors v w)]
+  obtain rfl | hij := eq_or_ne v w
+  · rw [← Set.toFinset_card]
+    simp [commonNeighbors, ← neighborFinset_def, h.regular v]
+  · simp only [Matrix.one_apply_ne' hij.symm, ne_eq, hij]
+    by_cases ha : G.Adj v w <;> conv_rhs => simp [ha]
+    · rw [h.of_adj v w ha]
+    · rw [h.of_not_adj v w hij ha]
+
 end SimpleGraph