feat(ring_theory/determinant): determinants (#404)

* clean up determinant PR

* remove unnecessary type annotations

* update copyright

* add additive version of prod_attach_univ

data/equiv/basic.lean

@@ -647,6 +647,12 @@ equiv.ext _ _ (λ x, begin
   split_ifs; simp
 end)
 
+@[simp] lemma swap_mul_self {α : Type*} [decidable_eq α] (i j : α) : swap i j * swap i j = 1 :=
+equiv.swap_swap i j
+
+@[simp] lemma swap_apply_self {α : Type*} [decidable_eq α] (i j a : α) : swap i j (swap i j a) = a :=
+by rw [← perm.mul_apply, swap_mul_self, perm.one_apply]
+
 /-- Augment an equivalence with a prescribed mapping `f a = b` -/
 def set_value (f : α ≃ β) (a : α) (b : β) : α ≃ β :=
 (swap a (f.symm b)).trans f

data/fintype.lean

@@ -61,6 +61,15 @@ instance decidable_eq_equiv_fintype [fintype α] [decidable_eq β] :
   decidable_eq (α ≃ β) :=
 λ a b, decidable_of_iff (a.1 = b.1) ⟨λ h, equiv.ext _ _ (congr_fun h), congr_arg _⟩
 
+instance decidable_injective_fintype [fintype α] [decidable_eq α] [decidable_eq β] :
+  decidable_pred (injective : (α → β) → Prop) := λ x, by unfold injective; apply_instance
+
+instance decidable_surjective_fintype [fintype α] [decidable_eq α] [fintype β] [decidable_eq β] :
+  decidable_pred (surjective : (α → β) → Prop) := λ x, by unfold surjective; apply_instance
+
+instance decidable_bijective_fintype [fintype α] [decidable_eq α] [fintype β] [decidable_eq β] :
+  decidable_pred (bijective : (α → β) → Prop) := λ x, by unfold bijective; apply_instance
+
 /-- Construct a proof of `fintype α` from a universal multiset -/
 def of_multiset [decidable_eq α] (s : multiset α)
   (H : ∀ x : α, x ∈ s) : fintype α :=
@@ -454,6 +463,11 @@ begin
   simp [this], exact setoid.refl _
 end
 
+@[simp, to_additive finset.sum_attach_univ]
+lemma finset.prod_attach_univ [fintype α] [comm_monoid β] (f : {a : α // a ∈ @univ α _} → β) :
+  univ.attach.prod (λ x, f x) = univ.prod (λ x, f ⟨x, (mem_univ _)⟩) :=
+prod_bij (λ x _, x.1) (λ _ _, mem_univ _) (λ _ _ , by simp) (by simp) (λ b _, ⟨⟨b, mem_univ _⟩, by simp⟩)
+
 section equiv
 
 open list equiv equiv.perm

group_theory/perm.lean

@@ -601,4 +601,10 @@ calc sign f = sign (swap x (f x) * (swap x (f x) * f)) :
       simp [pow_add]
 using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ f, f.support.card)⟩]}
 
-end equiv.perm
+end equiv.perm
+
+@[to_additive finset.sum_univ_perm]
+lemma finset.prod_univ_perm [fintype α] [comm_monoid β] {f : α → β} (σ : perm α) :
+  (univ : finset α).prod f = univ.prod (λ z, f (σ z)) :=
+eq.symm $ prod_bij (λ z _, σ z) (λ _ _, mem_univ _) (λ _ _, rfl)
+  (λ _ _ _ _ H, σ.bijective.1 H) (λ b _, ⟨σ⁻¹ b, mem_univ _, by simp⟩)

ring_theory/determinant.lean

@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Chris Hughes
+-/
+import group_theory.subgroup group_theory.perm ring_theory.matrix
+
+universes u v
+open equiv equiv.perm finset function
+
+namespace matrix
+
+variables {n : Type u} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R]
+
+definition det (M : matrix n n R) : R :=
+univ.sum (λ (σ : perm n), sign σ * univ.prod (λ i, M (σ i) i))
+
+@[simp] lemma det_diagonal {d : n → R} : det (diagonal d) = univ.prod d :=
+begin
+  refine (finset.sum_eq_single 1 _ _).trans _,
+  { intros σ h1 h2,
+    cases not_forall.1 (mt (equiv.ext _ _) h2) with x h3,
+    convert ring.mul_zero _,
+    apply finset.prod_eq_zero,
+    { change x ∈ _, simp },
+    exact if_neg h3 },
+  { simp },
+  { simp }
+end
+
+@[simp] lemma det_zero (h : nonempty n) : det (0 : matrix n n R) = 0 :=
+by rw [← diagonal_zero, det_diagonal, finset.prod_const, ← fintype.card,
+  zero_pow (fintype.card_pos_iff.2 h)]
+
+@[simp] lemma det_one : det (1 : matrix n n R) = 1 :=
+by rw [← diagonal_one]; simp [-diagonal_one]
+
+lemma det_mul_aux {M N : matrix n n R} {p : n → n} (H : ¬bijective p) :
+  univ.sum (λ σ : perm n, (sign σ : R) * (univ.prod (λ x, M (σ x) (p x) * N (p x) x))) = 0 :=
+let ⟨i, hi⟩ := classical.not_forall.1 (mt fintype.injective_iff_bijective.1 H) in
+let ⟨j, hij'⟩ := classical.not_forall.1 hi in
+have hij : p i = p j ∧ i ≠ j, from not_imp.1 hij',
+sum_involution
+  (λ σ _, σ * swap i j)
+  (λ σ _,
+    have ∀ a, p (swap i j a) = p a := λ a, by simp only [swap_apply_def]; split_ifs; cc,
+    have univ.prod (λ x, M (σ x) (p x)) = univ.prod (λ x, M ((σ * swap i j) x) (p x)),
+      from prod_bij (λ a _, swap i j a) (λ _ _, mem_univ _) (by simp [this])
+        (λ _ _ _ _ h, (swap i j).bijective.1 h)
+        (λ b _, ⟨swap i j b, mem_univ _, by simp⟩),
+    by simp [sign_mul, this, sign_swap hij.2, prod_mul_distrib])
+  (λ σ _ _ h, hij.2 (σ.bijective.1 $ by conv {to_lhs, rw ← h}; simp))
+  (λ _ _, mem_univ _)
+  (λ _ _, equiv.ext _ _ $ by simp)
+
+@[simp] lemma det_mul (M N : matrix n n R) : det (M * N) = det M * det N :=
+calc det (M * N) = univ.sum (λ σ : perm n, (univ.pi (λ a, univ)).sum
+    (λ (p : Π (a : n), a ∈ univ → n), sign σ *
+    univ.attach.prod (λ i, M (σ i.1) (p i.1 (mem_univ _)) * N (p i.1 (mem_univ _)) i.1))) :
+  by simp only [det, mul_val', prod_sum, mul_sum]
+... = univ.sum (λ σ : perm n, univ.sum
+    (λ p : n → n, sign σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) :
+  sum_congr rfl (λ σ _, sum_bij
+    (λ f h i, f i (mem_univ _)) (λ _ _, mem_univ _)
+    (by simp) (by simp [funext_iff]) (λ b _, ⟨λ i hi, b i, by simp⟩))
+... = univ.sum (λ p : n → n, univ.sum
+    (λ σ : perm n, sign σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) :
+  finset.sum_comm
+... = ((@univ (n → n) _).filter bijective ∪ univ.filter (λ p : n → n, ¬bijective p)).sum
+    (λ p : n → n, univ.sum (λ σ : perm n, sign σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) :
+  finset.sum_congr (finset.ext.2 (by simp; tauto)) (λ _ _, rfl)
+... = ((@univ (n → n) _).filter bijective).sum (λ p : n → n, univ.sum
+    (λ σ : perm n, sign σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) +
+    (univ.filter (λ p : n → n, ¬bijective p)).sum (λ p : n → n, univ.sum
+    (λ σ : perm n, sign σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) :
+  finset.sum_union (by simp [finset.ext]; tauto)
+... = ((@univ (n → n) _).filter bijective).sum (λ p : n → n, univ.sum
+    (λ σ : perm n, sign σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) +
+    (univ.filter (λ p : n → n, ¬bijective p)).sum (λ p, 0) :
+  (add_left_inj _).2 (finset.sum_congr rfl $ λ p h, det_mul_aux (mem_filter.1 h).2)
+... = ((@univ (n → n) _).filter bijective).sum (λ p : n → n, univ.sum
+    (λ σ : perm n, sign σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) : by simp
+... = (@univ (perm n) _).sum (λ τ, univ.sum
+    (λ σ : perm n, sign σ * univ.prod (λ i, M (σ i) (τ i) * N (τ i) i))) :
+  sum_bij (λ p h, equiv.of_bijective (mem_filter.1 h).2) (λ _ _, mem_univ _)
+    (λ _ _, rfl) (λ _ _ _ _ h, by injection h)
+    (λ b _, ⟨b, mem_filter.2 ⟨mem_univ _, b.bijective⟩, eq_of_to_fun_eq rfl⟩)
+... = univ.sum (λ σ : perm n, univ.sum (λ τ : perm n,
+    (univ.prod (λ i, N (σ i) i) * sign τ) * univ.prod (λ j, M (τ j) (σ j)))) :
+  by simp [mul_sum, det, mul_comm, mul_left_comm, prod_mul_distrib, mul_assoc]
+... = univ.sum (λ σ : perm n, univ.sum (λ τ : perm n,
+    (univ.prod (λ i, N (σ i) i) * (sign σ * sign τ)) *
+    univ.prod (λ i, M (τ i) i))) :
+  sum_congr rfl (λ σ _, sum_bij (λ τ _, τ * σ⁻¹) (λ _ _, mem_univ _)
+    (λ τ _,
+      have univ.prod (λ j, M (τ j) (σ j)) = univ.prod (λ j, M ((τ * σ⁻¹) j) j),
+        by rw prod_univ_perm σ⁻¹; simp [mul_apply],
+      have h : (sign σ * sign (τ * σ⁻¹) : R) = sign τ :=
+        calc (sign σ * sign (τ * σ⁻¹) : R) = sign ((τ * σ⁻¹) * σ) :
+          by rw [mul_comm, sign_mul (τ * σ⁻¹)]; simp [sign_mul]
+        ... = sign τ : by simp,
+      by rw h; simp [this, mul_comm, mul_assoc, mul_left_comm])
+    (λ _ _ _ _, (mul_right_inj _).1) (λ τ _, ⟨τ * σ, by simp⟩))
+... = det M * det N : by simp [det, mul_assoc, mul_sum, mul_comm, mul_left_comm]
+#print det_mul
+end matrix