-
-
Save kmill/7f876df1d581047cd8dc56ffafa291d0 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment