feat(Combinatorics/SimpleGraph/AdjMatrix): adjacency matrix API (leanprover-community#34601)

Author: themathqueen

Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

@@ -11,6 +11,7 @@ public import Mathlib.LinearAlgebra.Matrix.Trace
 public import Mathlib.LinearAlgebra.Matrix.Hadamard
 
 import Mathlib.Algebra.GroupWithZero.Idempotent
+import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 
 /-!
 # Adjacency Matrices
@@ -46,7 +47,7 @@ open Matrix
 
 open Finset SimpleGraph
 
-variable {V α : Type*}
+variable {α V : Type*}
 
 namespace Matrix
 
@@ -63,6 +64,8 @@ namespace IsAdjMatrix
 
 variable {A : Matrix V V α}
 
+@[simp] protected theorem zero [Zero α] [One α] : (0 : Matrix V V α).IsAdjMatrix where
+
 @[simp]
 theorem apply_diag_ne [MulZeroOneClass α] [Nontrivial α] (h : IsAdjMatrix A) (i : V) :
     ¬A i i = 1 := by simp [h.apply_diag i]
@@ -88,19 +91,22 @@ instance [MulZeroOneClass α] [Nontrivial α] [DecidableEq α] (h : IsAdjMatrix
   simp only [toGraph]
   infer_instance
 
+@[simp] theorem hadamard_self [MulZeroOneClass α] {A : Matrix V V α} (hA : A.IsAdjMatrix) :
+    A ⊙ A = A := by ext i j; have := hA.zero_or_one i j; aesop
+
 end IsAdjMatrix
 
 theorem isAdjMatrix_iff_hadamard [DecidableEq V] [MonoidWithZero α]
     [IsLeftCancelMulZero α] {A : Matrix V V α} :
     A.IsAdjMatrix ↔ (A ⊙ A = A ∧ A.IsSymm ∧ 1 ⊙ A = 0) := by
   simp only [hadamard_self_eq_self_iff, IsIdempotentElem.iff_eq_zero_or_one,
-    one_hadamard_eq_zero_iff, funext_iff, diag]
-  exact ⟨fun ⟨h1, h2, h3⟩ ↦ ⟨h1, h2, h3⟩, fun ⟨h1, h2, h3⟩ ↦ ⟨h1, h2, h3⟩⟩
+    one_hadamard_eq_zero_iff, funext_iff, diag, Pi.zero_apply]
+  grind [IsAdjMatrix]
 
 /-- For `A : Matrix V V α`, `A.compl` is supposed to be the adjacency matrix of
 the complement graph of the graph induced by `A.adjMatrix`. -/
 def compl [Zero α] [One α] [DecidableEq α] [DecidableEq V] (A : Matrix V V α) : Matrix V V α :=
-  fun i j => ite (i = j) 0 (ite (A i j = 0) 1 0)
+  of fun i j ↦ if i = j then 0 else if A i j = 0 then 1 else 0
 
 section Compl
 
@@ -111,8 +117,7 @@ theorem compl_apply_diag [Zero α] [One α] (i : V) : A.compl i i = 0 := by simp
 
 @[simp]
 theorem compl_apply [Zero α] [One α] (i j : V) : A.compl i j = 0 ∨ A.compl i j = 1 := by
-  unfold compl
-  split_ifs <;> simp
+  grind [compl, of]
 
 @[simp]
 theorem isSymm_compl [Zero α] [One α] (h : A.IsSymm) : A.compl.IsSymm := by
@@ -123,6 +128,13 @@ theorem isSymm_compl [Zero α] [One α] (h : A.IsSymm) : A.compl.IsSymm := by
 theorem isAdjMatrix_compl [Zero α] [One α] (h : A.IsSymm) : IsAdjMatrix A.compl :=
   { symm := by simp [h] }
 
+theorem IsAdjMatrix.compl_inj [Zero α] [One α] {A B : Matrix V V α}
+    (hA : A.IsAdjMatrix) (hB : B.IsAdjMatrix) : A.compl = B.compl ↔ A = B :=
+  ⟨fun h ↦ ext fun i j ↦ by grind [of, congr($h i j), compl, IsAdjMatrix], fun h ↦ h ▸ rfl⟩
+
+@[simp] theorem IsAdjMatrix.compl_compl [Zero α] [One α] {A : Matrix V V α} (hA : A.IsAdjMatrix) :
+    A.compl.compl = A := by ext; grind [of, compl, IsAdjMatrix]
+
 namespace IsAdjMatrix
 
 variable {A}
@@ -169,10 +181,12 @@ theorem isSymm_adjMatrix [Zero α] [One α] : (G.adjMatrix α).IsSymm :=
 
 variable (α)
 
+@[simp] theorem diag_adjMatrix [Zero α] [One α] : (G.adjMatrix α).diag = 0 := by ext; simp
+
 /-- The adjacency matrix of `G` is an adjacency matrix. -/
 @[simp]
-theorem isAdjMatrix_adjMatrix [Zero α] [One α] : (G.adjMatrix α).IsAdjMatrix :=
-  { zero_or_one := fun i j => by by_cases h : G.Adj i j <;> simp [h] }
+theorem isAdjMatrix_adjMatrix [Zero α] [One α] : (G.adjMatrix α).IsAdjMatrix where
+  zero_or_one := by grind [adjMatrix_apply]
 
 /-- The graph induced by the adjacency matrix of `G` is `G` itself. -/
 theorem toGraph_adjMatrix_eq [MulZeroOneClass α] [Nontrivial α] :
@@ -181,18 +195,58 @@ theorem toGraph_adjMatrix_eq [MulZeroOneClass α] [Nontrivial α] :
   simp only [IsAdjMatrix.toGraph_adj, adjMatrix_apply, ite_eq_left_iff, zero_ne_one]
   apply Classical.not_not
 
-variable {α}
+theorem compl_adjMatrix_eq_adjMatrix_compl [DecidableEq V] [DecidableEq α] [Zero α] [One α] :
+    (G.adjMatrix α).compl = Gᶜ.adjMatrix α := by aesop (add simp [Matrix.compl])
+
+set_option backward.isDefEq.respectTransparency false in
+variable {G} in
+theorem IsCompl.adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraph [DecidableEq V] [AddZeroClass α]
+    [One α] {H : SimpleGraph V} [DecidableRel H.Adj] (h : IsCompl G H) :
+    G.adjMatrix α + H.adjMatrix α = (completeGraph V).adjMatrix α := calc
+  _ = G.adjMatrix α + Gᶜ.adjMatrix α := by have := h.compl_eq; subst this; congr
+  _ = _ := by aesop (add simp Matrix.compl)
+
+@[simp] theorem adjMatrix_add_compl_adjMatrix_eq_adjMatrix_completeGraph [DecidableEq V]
+    [DecidableEq α] [AddZeroClass α] [One α] :
+    G.adjMatrix α + (G.adjMatrix α).compl = (completeGraph V).adjMatrix α :=
+  G.compl_adjMatrix_eq_adjMatrix_compl α ▸
+    isCompl_compl.adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraph α
 
 /-- The sum of the identity, the adjacency matrix, and its complement is the all-ones matrix. -/
-theorem one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes [DecidableEq V] [DecidableEq α]
-    [AddMonoidWithOne α] : 1 + G.adjMatrix α + (G.adjMatrix α).compl = Matrix.of fun _ _ ↦ 1 := by
-  ext i j
-  unfold Matrix.compl
-  rw [of_apply, add_apply, adjMatrix_apply, add_apply, adjMatrix_apply, one_apply]
-  by_cases h : G.Adj i j
-  · aesop
-  · split_ifs <;> simp_all
+theorem one_add_adjMatrix_add_compl_adjMatrix_eq_of_one [DecidableEq V] [DecidableEq α]
+    [AddMonoid α] [One α] : 1 + G.adjMatrix α + (G.adjMatrix α).compl = of 1 := by
+  aesop (add simp [add_assoc])
+
+@[deprecated (since := "2026-01-30")] alias one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes :=
+  one_add_adjMatrix_add_compl_adjMatrix_eq_of_one
+
+variable (V)
+
+@[simp] theorem compl_adjMatrix_completeGraph [Zero α] [One α] [DecidableEq α] [DecidableEq V] :
+    ((completeGraph V).adjMatrix α).compl = 0 := by aesop (add simp Matrix.compl)
+
+@[simp] theorem _root_.Matrix.compl_zero [Zero α] [One α] [DecidableEq α] [DecidableEq V] :
+    (0 : Matrix V V α).compl = (completeGraph V).adjMatrix α := by simp [← IsAdjMatrix.compl_inj]
+
+theorem adjMatrix_completeGraph_eq_of_one_sub_one [AddGroup α] [One α] [DecidableEq V] :
+    (completeGraph V).adjMatrix α = of 1 - 1 := by ext; simp [one_apply, sub_ite]
+
+theorem _root_.Matrix.compl_zero_eq_of_one_sub_one [AddGroup α] [One α] [DecidableEq V]
+    [DecidableEq α] : (0 : Matrix V V α).compl = of 1 - 1 := by
+  simp [adjMatrix_completeGraph_eq_of_one_sub_one]
+
+@[simp] theorem _root_.Matrix.compl_of_one_sub_one [AddGroup α] [One α] [DecidableEq V]
+    [DecidableEq α] : (of 1 - 1 : Matrix V V α).compl = 0 := by
+  simp [← adjMatrix_completeGraph_eq_of_one_sub_one]
+
+variable {V}
+
+theorem adjMatrix_hadamard_self [MulZeroOneClass α] :
+    G.adjMatrix α ⊙ G.adjMatrix α = G.adjMatrix α := by simp
 
+variable {α}
+
+section fintype
 variable [Fintype V]
 
 @[simp]
@@ -235,6 +289,13 @@ theorem trace_adjMatrix [AddCommMonoid α] [One α] : Matrix.trace (G.adjMatrix
 theorem adjMatrix_mul_self_apply_self [NonAssocSemiring α] (i : V) :
     (G.adjMatrix α * G.adjMatrix α) i i = degree G i := by simp [filter_true_of_mem]
 
+variable (R) in
+/-- The number of all darts in a simple finite graph is equal to the dot product of
+`G.adjMatrix α *ᵥ 1` and `1`. -/
+theorem natCast_card_dart_eq_dotProduct [NonAssocSemiring α] :
+    (Fintype.card G.Dart : α) = adjMatrix α G *ᵥ 1 ⬝ᵥ 1 := by
+  simp [G.dart_card_eq_sum_degrees, dotProduct_one]
+
 variable {G}
 
 theorem adjMatrix_mulVec_const_apply [NonAssocSemiring α] {a : α} {v : V} :
@@ -266,8 +327,46 @@ theorem adjMatrix_pow_apply_eq_card_walk [DecidableEq V] [Semiring α] (n : ℕ)
 
 theorem dotProduct_mulVec_adjMatrix [NonAssocSemiring α] (x y : V → α) :
     x ⬝ᵥ G.adjMatrix α *ᵥ y = ∑ i : V, ∑ j : V, if G.Adj i j then x i * y j else 0 := by
-  simp only [dotProduct, mulVec, adjMatrix_apply, ite_mul, one_mul, zero_mul, mul_sum, mul_ite,
-    mul_zero]
+  simp [dotProduct, mulVec, mul_sum]
+
+end fintype
+
+section hadamard
+variable (α) [DecidableEq V] [MulZeroOneClass α]
+
+open Matrix
+
+@[simp] theorem adjMatrix_hadamard_diagonal (d : V → α) :
+    G.adjMatrix α ⊙ diagonal d = 0 := by simp [hadamard_diagonal]
+
+@[simp] theorem diagonal_hadamard_adjMatrix (d : V → α) :
+    diagonal d ⊙ G.adjMatrix α = 0 := by simp [diagonal_hadamard]
+
+@[simp] theorem adjMatrix_hadamard_natCast [NatCast α] (a : ℕ) :
+    G.adjMatrix α ⊙ a.cast = 0 := adjMatrix_hadamard_diagonal _ _ _
+
+@[simp] theorem natCast_hadamard_adjMatrix [NatCast α] (a : ℕ) :
+    a.cast ⊙ G.adjMatrix α = 0 := diagonal_hadamard_adjMatrix _ _ _
+
+@[simp] theorem adjMatrix_hadamard_ofNat [NatCast α] (a : ℕ) [a.AtLeastTwo] :
+    G.adjMatrix α ⊙ ofNat(a) = 0 := adjMatrix_hadamard_diagonal _ _ _
+
+@[simp] theorem ofNat_hadamard_adjMatrix [NatCast α] (a : ℕ) [a.AtLeastTwo] :
+    ofNat(a) ⊙ G.adjMatrix α = 0 := diagonal_hadamard_adjMatrix _ _ _
+
+@[simp] theorem adjMatrix_hadamard_intCast [IntCast α] (a : ℤ) :
+    G.adjMatrix α ⊙ a.cast = 0 := adjMatrix_hadamard_diagonal _ _ _
+
+@[simp] theorem intCast_hadamard_adjMatrix [IntCast α] (a : ℤ) :
+    a.cast ⊙ G.adjMatrix α = 0 := diagonal_hadamard_adjMatrix _ _ _
+
+@[simp] theorem adjMatrix_hadamard_one :
+    G.adjMatrix α ⊙ 1 = 0 := adjMatrix_hadamard_diagonal _ _ _
+
+@[simp] theorem one_hadamard_adjMatrix :
+    1 ⊙ G.adjMatrix α = 0 := diagonal_hadamard_adjMatrix _ _ _
+
+end hadamard
 
 end SimpleGraph