feat(combinatorics/simple_graph/inc_matrix): Incidence matrix (#10867)

Define the incidence matrix of a simple graph and prove the basics, including some stuff about matrix multiplication.

Co-authored-by: Gabriel Moise <gabriel.moise@stcatz.ox.ac.uk>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>



Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Author: YaelDillies

src/algebra/ring/basic.lean

@@ -269,6 +269,11 @@ lemma ite_mul_zero_right {α : Type*} [mul_zero_class α] (P : Prop) [decidable
   ite P (a * b) 0 = a * ite P b 0 :=
 by { by_cases h : P; simp [h], }
 
+lemma ite_and_mul_zero {α : Type*} [mul_zero_class α]
+  (P Q : Prop) [decidable P] [decidable Q] (a b : α) :
+  ite (P ∧ Q) (a * b) 0 = ite P a 0 * ite Q b 0 :=
+by simp only [←ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]
+
 /-- An element `a` of a semiring is even if there exists `k` such `a = 2*k`. -/
 def even (a : α) : Prop := ∃ k, a = 2*k
 

src/combinatorics/simple_graph/basic.lean

@@ -428,7 +428,7 @@ lemma incidence_set_inter_incidence_set_subset (h : a ≠ b) :
   G.incidence_set a ∩ G.incidence_set b ⊆ {⟦(a, b)⟧} :=
 λ e he, (sym2.mem_and_mem_iff h).1 ⟨he.1.2, he.2.2⟩
 
-lemma incidence_set_inter_incidence_set (h : G.adj a b) :
+lemma incidence_set_inter_incidence_set_of_adj (h : G.adj a b) :
   G.incidence_set a ∩ G.incidence_set b = {⟦(a, b)⟧} :=
 begin
   refine (G.incidence_set_inter_incidence_set_subset $ h.ne).antisymm _,
@@ -442,6 +442,14 @@ lemma adj_of_mem_incidence_set (h : a ≠ b) (ha : e ∈ G.incidence_set a)
 by rwa [←mk_mem_incidence_set_left_iff,
   ←set.mem_singleton_iff.1 $ G.incidence_set_inter_incidence_set_subset h ⟨ha, hb⟩]
 
+lemma incidence_set_inter_incidence_set_of_not_adj (h : ¬ G.adj a b) (hn : a ≠ b) :
+  G.incidence_set a ∩ G.incidence_set b = ∅ :=
+begin
+  simp_rw [set.eq_empty_iff_forall_not_mem, set.mem_inter_eq, not_and],
+  intros u ha hb,
+  exact h (G.adj_of_mem_incidence_set hn ha hb),
+end
+
 instance decidable_mem_incidence_set [decidable_eq V] [decidable_rel G.adj] (v : V) :
   decidable_pred (∈ G.incidence_set v) := λ e, and.decidable
 
@@ -687,6 +695,11 @@ lemma card_incidence_set_eq_degree [decidable_eq V] :
   fintype.card (G.incidence_set v) = G.degree v :=
 by { rw fintype.card_congr (G.incidence_set_equiv_neighbor_set v), simp }
 
+@[simp]
+lemma card_incidence_finset_eq_degree [decidable_eq V] :
+  (G.incidence_finset v).card = G.degree v :=
+by { rw ← G.card_incidence_set_eq_degree, apply set.to_finset_card }
+
 @[simp]
 lemma mem_incidence_finset [decidable_eq V] (e : sym2 V) :
   e ∈ G.incidence_finset v ↔ e ∈ G.incidence_set v :=

src/combinatorics/simple_graph/inc_matrix.lean

@@ -0,0 +1,187 @@
+/-
+Copyright (c) 2021 Gabriel Moise. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Moise, Yaël Dillies, Kyle Miller
+-/
+import combinatorics.simple_graph.basic
+import data.matrix.basic
+
+/-!
+# Incidence matrix of a simple graph
+
+This file defines the unoriented incidence matrix of a simple graph.
+
+## Main definitions
+
+* `simple_graph.inc_matrix`: `G.inc_matrix R` is the incidence matrix of `G` over the ring `R`.
+
+## Main results
+
+* `simple_graph.inc_matrix_mul_transpose_diag`: The diagonal entries of the product of
+  `G.inc_matrix R` and its transpose are the degrees of the vertices.
+* `simple_graph.inc_matrix_mul_transpose`: Gives a complete description of the product of
+  `G.inc_matrix R` and its transpose; the diagonal is the degrees of each vertex, and the
+  off-diagonals are 1 or 0 depending on whether or not the vertices are adjacent.
+* `simple_graph.inc_matrix_transpose_mul_diag`: The diagonal entries of the product of the
+  transpose of `G.inc_matrix R` and `G.inc_matrix R` are `2` or `0` depending on whether or
+  not the unordered pair is an edge of `G`.
+
+## Implementation notes
+
+The usual definition of an incidence matrix has one row per vertex and one column per edge.
+However, this definition has columns indexed by all of `sym2 α`, where `α` is the vertex type.
+This appears not to change the theory, and for simple graphs it has the nice effect that every
+incidence matrix for each `simple_graph α` has the same type.
+
+## TODO
+
+* Define the oriented incidence matrices for oriented graphs.
+* Define the graph Laplacian of a simple graph using the oriented incidence matrix from an
+  arbitrary orientation of a simple graph.
+-/
+
+noncomputable theory
+
+open finset matrix simple_graph sym2
+open_locale big_operators matrix
+
+namespace simple_graph
+variables (R : Type*) {α : Type*} (G : simple_graph α)
+
+/-- `G.inc_matrix R` is the `α × sym2 α` matrix whose `(a, e)`-entry is `1` if `e` is incident to
+`a` and `0` otherwise. -/
+def inc_matrix [has_zero R] [has_one R] : matrix α (sym2 α) R :=
+λ a, (G.incidence_set a).indicator 1
+
+variables {R}
+
+lemma inc_matrix_apply [has_zero R] [has_one R] {a : α} {e : sym2 α} :
+  G.inc_matrix R a e = (G.incidence_set a).indicator 1 e := rfl
+
+/-- Entries of the incidence matrix can be computed given additional decidable instances. -/
+lemma inc_matrix_apply' [has_zero R] [has_one R] [decidable_eq α] [decidable_rel G.adj]
+  {a : α} {e : sym2 α} :
+  G.inc_matrix R a e = if e ∈ G.incidence_set a then 1 else 0 :=
+by convert rfl
+
+section mul_zero_one_class
+variables [mul_zero_one_class R] {a b : α} {e : sym2 α}
+
+lemma inc_matrix_apply_mul_inc_matrix_apply :
+  G.inc_matrix R a e * G.inc_matrix R b e = (G.incidence_set a ∩ G.incidence_set b).indicator 1 e :=
+begin
+  simp only [inc_matrix, set.indicator_apply, ←ite_and_mul_zero,
+    pi.one_apply, mul_one, set.mem_inter_eq],
+  congr,
+end
+
+lemma inc_matrix_apply_mul_inc_matrix_apply_of_not_adj (hab : a ≠ b) (h : ¬ G.adj a b) :
+  G.inc_matrix R a e * G.inc_matrix R b e = 0 :=
+begin
+  rw [inc_matrix_apply_mul_inc_matrix_apply, set.indicator_of_not_mem],
+  rw [G.incidence_set_inter_incidence_set_of_not_adj h hab],
+  exact set.not_mem_empty e,
+end
+
+lemma inc_matrix_of_not_mem_incidence_set (h : e ∉ G.incidence_set a) :
+  G.inc_matrix R a e = 0 :=
+by rw [inc_matrix_apply, set.indicator_of_not_mem h]
+
+lemma inc_matrix_of_mem_incidence_set (h : e ∈ G.incidence_set a) : G.inc_matrix R a e = 1 :=
+by rw [inc_matrix_apply, set.indicator_of_mem h, pi.one_apply]
+
+variables [nontrivial R]
+
+lemma inc_matrix_apply_eq_zero_iff : G.inc_matrix R a e = 0 ↔ e ∉ G.incidence_set a :=
+begin
+  simp only [inc_matrix_apply, set.indicator_apply_eq_zero, pi.one_apply, one_ne_zero],
+  exact iff.rfl,
+end
+
+lemma inc_matrix_apply_eq_one_iff : G.inc_matrix R a e = 1 ↔ e ∈ G.incidence_set a :=
+by { convert one_ne_zero.ite_eq_left_iff, assumption }
+
+end mul_zero_one_class
+
+section non_assoc_semiring
+variables [fintype α] [non_assoc_semiring R] {a b : α} {e : sym2 α}
+
+lemma sum_inc_matrix_apply [decidable_eq α] [decidable_rel G.adj] :
+  ∑ e, G.inc_matrix R a e = G.degree a :=
+by simp [inc_matrix_apply', sum_boole, set.filter_mem_univ_eq_to_finset]
+
+lemma inc_matrix_mul_transpose_diag [decidable_eq α] [decidable_rel G.adj] :
+  (G.inc_matrix R ⬝ (G.inc_matrix R)ᵀ) a a = G.degree a :=
+begin
+  rw ←sum_inc_matrix_apply,
+  simp [matrix.mul_apply, inc_matrix_apply', ←ite_and_mul_zero],
+end
+
+lemma sum_inc_matrix_apply_of_mem_edge_set : e ∈ G.edge_set → ∑ a, G.inc_matrix R a e = 2 :=
+begin
+  classical,
+  refine e.ind _,
+  intros a b h,
+  rw mem_edge_set at h,
+  rw [←nat.cast_two, ←card_doubleton h.ne],
+  simp only [inc_matrix_apply', sum_boole, mk_mem_incidence_set_iff, h, true_and],
+  congr' 2,
+  ext e,
+  simp only [mem_filter, mem_univ, true_and, mem_insert, mem_singleton],
+end
+
+lemma sum_inc_matrix_apply_of_not_mem_edge_set (h : e ∉ G.edge_set) : ∑ a, G.inc_matrix R a e = 0 :=
+sum_eq_zero $ λ a _, G.inc_matrix_of_not_mem_incidence_set $ λ he, h he.1
+
+lemma inc_matrix_transpose_mul_diag [decidable_rel G.adj] :
+  ((G.inc_matrix R)ᵀ ⬝ G.inc_matrix R) e e = if e ∈ G.edge_set then 2 else 0 :=
+begin
+  classical,
+  simp only [matrix.mul_apply, inc_matrix_apply', transpose_apply, ←ite_and_mul_zero,
+    one_mul, sum_boole, and_self],
+  split_ifs with h,
+  { revert h,
+    refine e.ind _,
+    intros v w h,
+    rw [←nat.cast_two, ←card_doubleton (G.ne_of_adj h)],
+    simp [mk_mem_incidence_set_iff, G.mem_edge_set.mp h],
+    congr' 2,
+    ext u,
+    simp, },
+  { revert h,
+    refine e.ind _,
+    intros v w h,
+    simp [mk_mem_incidence_set_iff, G.mem_edge_set.not.mp h], },
+end
+
+end non_assoc_semiring
+
+section semiring
+variables [fintype (sym2 α)] [semiring R] {a b : α} {e : sym2 α}
+
+lemma inc_matrix_mul_transpose_apply_of_adj (h : G.adj a b) :
+  (G.inc_matrix R ⬝ (G.inc_matrix R)ᵀ) a b = (1 : R) :=
+begin
+  simp_rw [matrix.mul_apply, matrix.transpose_apply, inc_matrix_apply_mul_inc_matrix_apply,
+    set.indicator_apply, pi.one_apply, sum_boole],
+  convert nat.cast_one,
+  convert card_singleton ⟦(a, b)⟧,
+  rw [←coe_eq_singleton, coe_filter_univ],
+  exact G.incidence_set_inter_incidence_set_of_adj h,
+end
+
+lemma inc_matrix_mul_transpose [fintype α] [decidable_eq α] [decidable_rel G.adj] :
+  G.inc_matrix R ⬝ (G.inc_matrix R)ᵀ = λ a b,
+    if a = b then G.degree a else if G.adj a b then 1 else 0 :=
+begin
+  ext a b,
+  split_ifs with h h',
+  { subst b,
+    convert G.inc_matrix_mul_transpose_diag },
+  { exact G.inc_matrix_mul_transpose_apply_of_adj h' },
+  { simp only [matrix.mul_apply, matrix.transpose_apply,
+    G.inc_matrix_apply_mul_inc_matrix_apply_of_not_adj h h', sum_const_zero] }
+end
+
+end semiring
+end simple_graph

src/data/finset/card.lean

@@ -33,7 +33,7 @@ open function multiset nat
 variables {α β : Type*}
 
 namespace finset
-variables {s t : finset α} {a : α}
+variables {s t : finset α} {a b : α}
 
 /-- `s.card` is the number of elements of `s`, aka its cardinality. -/
 def card (s : finset α) : ℕ := s.1.card
@@ -88,6 +88,9 @@ begin
   { rw [card_insert_of_not_mem h, if_neg h] }
 end
 
+@[simp] lemma card_doubleton (h : a ≠ b) : ({a, b} : finset α).card = 2 :=
+by rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton]
+
 @[simp] lemma card_erase_of_mem : a ∈ s → (s.erase a).card = s.card - 1 := card_erase_of_mem
 @[simp] lemma card_erase_add_one : a ∈ s → (s.erase a).card + 1 = s.card := card_erase_add_one
 
@@ -463,8 +466,8 @@ begin
     simp_rw [card_eq_one],
     rintro ⟨a, _, hab, rfl, b, rfl⟩,
     exact ⟨a, b, not_mem_singleton.1 hab, rfl⟩ },
-  { rintro ⟨x, y, hxy, rfl⟩,
-    simp only [hxy, card_insert_of_not_mem, not_false_iff, mem_singleton, card_singleton] }
+  { rintro ⟨x, y, h, rfl⟩,
+    exact card_doubleton h }
 end
 
 lemma card_eq_three [decidable_eq α] :

src/data/fintype/basic.lean

@@ -209,6 +209,9 @@ lemma univ_filter_mem_range (f : α → β) [fintype β]
   finset.univ.filter (λ y, y ∈ set.range f) = finset.univ.image f :=
 univ_filter_exists f
 
+lemma coe_filter_univ (p : α → Prop) [decidable_pred p] : (univ.filter p : set α) = {x | p x} :=
+by rw [coe_filter, coe_univ, set.sep_univ]
+
 /-- A special case of `finset.sup_eq_supr` that omits the useless `x ∈ univ` binder. -/
 lemma sup_univ_eq_supr [complete_lattice β] (f : α → β) : finset.univ.sup f = supr f :=
 (sup_eq_supr _ f).trans $ congr_arg _ $ funext $ λ a, supr_pos (mem_univ _)
@@ -668,6 +671,10 @@ end
   disjoint s.to_finset t.to_finset ↔ disjoint s t :=
 ⟨λ h x hx, h (by simpa using hx), λ h x hx, h (by simpa using hx)⟩
 
+lemma filter_mem_univ_eq_to_finset [fintype α] (s : set α) [fintype s] [decidable_pred (∈ s)] :
+  finset.univ.filter (∈ s) = s.to_finset :=
+by { ext, simp only [mem_filter, finset.mem_univ, true_and, mem_to_finset] }
+
 end set
 
 lemma finset.card_univ [fintype α] : (finset.univ : finset α).card = fintype.card α :=

src/linear_algebra/affine_space/combination.lean

@@ -543,8 +543,7 @@ begin
     rw [centroid_def,
         affine_combination_eq_weighted_vsub_of_point_vadd_of_sum_eq_one _ _ _
           (sum_centroid_weights_eq_one_of_cast_card_ne_zero _ hc) (p i₁)],
-    simp [h],
-    norm_num }
+    simp [h] }
 end
 
 /-- The centroid of two points indexed by `fin 2`, expressed directly