inc_matrix2.lean

import combinatorics.simple_graph.basic
import combinatorics.simple_graph.adj_matrix
import linear_algebra.matrix

open finset
open_locale big_operators matrix

@[simp]
lemma ite_mul_ite_zero_right
  {R : Type*} [mul_zero_class R] {P Q : Prop} [decidable P] [decidable Q] (a b : R):
  (ite P a 0) * (ite Q b 0) = ite (P ∧ Q) (a * b) 0 :=
by simp [←ite_and]

namespace simple_graph
variables {V : Type*} (G : simple_graph V) [fintype V] [decidable_eq V] [decidable_rel G.adj]
variables (R : Type*) [ring R]

lemma edge_eq_of_mem_incidence_sets {i j : V} {e : sym2 V} (hne : i ≠ j)
  (hi : e ∈ G.incidence_set i) (hj : e ∈ G.incidence_set j) :
  e = ⟦(i, j)⟧ :=
begin
  refine quotient.ind (λ p hi hj, _) e hi hj,
  rcases p with ⟨v, w⟩,
  rw ←sym2.elems_iff_eq hne,
  exact ⟨hi.2, hj.2⟩,
end

lemma mem_incidence_sets_iff_of_adj {i j : V} {e : sym2 V} (h : G.adj i j) :
  e ∈ G.incidence_set i ∧ e ∈ G.incidence_set j ↔ e = ⟦(i, j)⟧ :=
begin
  split,
  { rintro ⟨hi, hj⟩,
    exact G.edge_eq_of_mem_incidence_sets (G.ne_of_adj h) hi hj, },
  { rintro rfl,
    rw [mem_incidence_set, sym2.eq_swap, mem_incidence_set],
    exact ⟨h, G.sym h⟩ },
end

def inc_matrix : matrix V (sym2 V) R
| i e := if e ∈ G.incidence_set i then 1 else 0

@[simp]
lemma inc_matrix_apply {i : V} {e : sym2 V} :
  G.inc_matrix R i e = if e ∈ G.incidence_set i then 1 else 0 := rfl

--  ∑ e, G.inc_matrix R i e * G.inc_matrix R j e = (1 : R)
lemma adj_sum_of_mul_inc_one {i j : V} (H_adj : G.adj i j) :
  (G.inc_matrix R ⬝ (G.inc_matrix R)ᵀ) i j = (1 : R) :=
begin
  simp only [matrix.mul_apply, matrix.transpose_apply,
    G.mem_incidence_sets_iff_of_adj H_adj, inc_matrix_apply, mul_one, sum_boole,
    ite_mul_ite_zero_right],
  rw ←nat.cast_one,
  congr,
  convert_to _ = finset.card {⟦(i, j)⟧},
  { rw finset.card_singleton },
  { apply congr_arg finset.card,
    ext e,
    simp only [mem_filter, and_iff_right_iff_imp, mem_edge_finset, mem_singleton],
    rintro rfl,
    exact finset.mem_univ _ },
end

theorem inc_matrix_mul_non_adj {i j : V} {e : sym2 V}
  (Hne : i ≠ j) (H_non_adj : ¬ G.adj i j) :
  G.inc_matrix R i e * G.inc_matrix R j e = 0 :=
begin
  simp only [matrix.mul_apply, matrix.transpose_apply,
    inc_matrix_apply, and_imp, mul_one,
    ite_mul_ite_zero_right, ite_eq_right_iff, one_ne_zero],
  intros h h',
  exfalso,
  have := G.edge_eq_of_mem_incidence_sets Hne h h',
  rw [this, mem_incidence_set] at h,
  exact H_non_adj h,
end

@[simp]
lemma card_incidence_finset_eq_degree [decidable_eq V] (v : V) :
  (G.incidence_finset v).card = G.degree v :=
begin
  convert G.card_incidence_set_eq_degree v using 1,
  apply set.to_finset_card,
end

lemma degree_equals_sum_of_incidence_row {i : V} :
  ∑ e, G.inc_matrix R i e = (G.degree i : R) :=
begin
  simp only [inc_matrix_apply, sum_boole],
  apply congr_arg,
  rw ←card_incidence_finset_eq_degree,
  apply congr_arg finset.card,
  ext e,
  simp,
end

lemma inc_matrix_mul_diag {i : V} :
  (G.inc_matrix R ⬝ (G.inc_matrix R)ᵀ) i i = G.degree i :=
begin
  rw ←degree_equals_sum_of_incidence_row,
  simp only [matrix.mul_apply, matrix.transpose_apply,
    inc_matrix_apply, and_self, mul_one,
    ite_mul_ite_zero_right],
  congr,
  ext,
  congr,
end

theorem inc_matrix_mul_transpose :
  G.inc_matrix R ⬝ (G.inc_matrix R)ᵀ = λ i j,
    if i = j then G.degree i else if G.adj i j then 1 else 0 :=
begin
  ext i j,
  split_ifs with h h',
  { subst j,
    rw G.inc_matrix_mul_diag, },
  { rw G.adj_sum_of_mul_inc_one _ h', },
  { simp only [matrix.mul_apply, matrix.transpose_apply, G.inc_matrix_mul_non_adj _ h h', sum_const_zero], },
end

end simple_graph