feat(linear_algebra): determinant of matrix.block_diagonal (#4300)

This PR shows the determinant of `matrix.block_diagonal` is the product of the determinant of each subblock.

The only contributing permutations in the expansion of the determinant are those which map each block to the same block. Each of those permutations has the form `equiv.prod_congr_left σ`. Using `equiv.perm.extend` and `equiv.prod_congr_right`, we can compute the sign of `equiv.prod_congr_left σ`, and with a bit of algebraic manipulation we reach the conclusion.

Author: Vierkantor

src/algebra/big_operators/basic.lean

@@ -1034,6 +1034,16 @@ end comm_group_with_zero
 
 end finset
 
+namespace list
+
+@[to_additive] lemma prod_to_finset {M : Type*} [decidable_eq α] [comm_monoid M]
+  (f : α → M) : ∀ {l : list α} (hl : l.nodup), l.to_finset.prod f = (l.map f).prod
+| [] _ := by simp
+| (a :: l) hl := let ⟨not_mem, hl⟩ := list.nodup_cons.mp hl in
+  by simp [finset.prod_insert (mt list.mem_to_finset.mp not_mem), prod_to_finset hl]
+
+end list
+
 namespace multiset
 variables [decidable_eq α]
 
@@ -1090,3 +1100,15 @@ begin
 end
 
 end multiset
+
+@[simp, norm_cast] lemma nat.coe_prod {R : Type*} [comm_semiring R]
+  (f : α → ℕ) (s : finset α) : (↑∏ i in s, f i : R) = ∏ i in s, f i :=
+(nat.cast_ring_hom R).map_prod _ _
+
+@[simp, norm_cast] lemma int.coe_prod {R : Type*} [comm_ring R]
+  (f : α → ℤ) (s : finset α) : (↑∏ i in s, f i : R) = ∏ i in s, f i :=
+(int.cast_ring_hom R).map_prod _ _
+
+@[simp, norm_cast] lemma units.coe_prod {M : Type*} [comm_monoid M]
+  (f : α → units M) (s : finset α) : (↑∏ i in s, f i : M) = ∏ i in s, f i :=
+(units.coe_hom M).map_prod _ _

src/data/equiv/basic.lean

@@ -758,6 +758,93 @@ def sigma_equiv_prod_of_equiv {α β} {β₁ : α → Sort*} (F : Π a, β₁ a
 
 end
 
+section prod_congr
+
+variables {α₁ β₁ β₂ : Type*} (e : α₁ → β₁ ≃ β₂)
+
+/-- A family of equivalences `Π (a : α₁), β₁ ≃ β₂` generates an equivalence
+between `β₁ × α₁` and `β₂ × α₁`. -/
+def prod_congr_left : β₁ × α₁ ≃ β₂ × α₁ :=
+{ to_fun := λ ab, ⟨e ab.2 ab.1, ab.2⟩,
+  inv_fun := λ ab, ⟨(e ab.2).symm ab.1, ab.2⟩,
+  left_inv := by { rintros ⟨a, b⟩, simp },
+  right_inv := by { rintros ⟨a, b⟩, simp } }
+
+@[simp] lemma prod_congr_left_apply (b : β₁) (a : α₁) :
+prod_congr_left e (b, a) = (e a b, a) := rfl
+
+lemma prod_congr_refl_right (e : β₁ ≃ β₂) :
+  prod_congr e (equiv.refl α₁) = prod_congr_left (λ _, e) :=
+by { ext ⟨a, b⟩ : 1, simp }
+
+/-- A family of equivalences `Π (a : α₁), β₁ ≃ β₂` generates an equivalence
+between `α₁ × β₁` and `α₁ × β₂`. -/
+def prod_congr_right : α₁ × β₁ ≃ α₁ × β₂ :=
+{ to_fun := λ ab, ⟨ab.1, e ab.1 ab.2⟩,
+  inv_fun := λ ab, ⟨ab.1, (e ab.1).symm ab.2⟩,
+  left_inv := by { rintros ⟨a, b⟩, simp },
+  right_inv := by { rintros ⟨a, b⟩, simp } }
+
+@[simp] lemma prod_congr_right_apply (a : α₁) (b : β₁) :
+  prod_congr_right e (a, b) = (a, e a b) := rfl
+
+lemma prod_congr_refl_left (e : β₁ ≃ β₂) :
+  prod_congr (equiv.refl α₁) e = prod_congr_right (λ _, e) :=
+by { ext ⟨a, b⟩ : 1, simp }
+
+@[simp] lemma prod_congr_left_trans_prod_comm :
+  (prod_congr_left e).trans (prod_comm _ _) = (prod_comm _ _).trans (prod_congr_right e) :=
+by { ext ⟨a, b⟩ : 1, simp }
+
+@[simp] lemma prod_congr_right_trans_prod_comm :
+  (prod_congr_right e).trans (prod_comm _ _) = (prod_comm _ _).trans (prod_congr_left e) :=
+by { ext ⟨a, b⟩ : 1, simp }
+
+lemma sigma_congr_right_sigma_equiv_prod :
+  (sigma_congr_right e).trans (sigma_equiv_prod α₁ β₂) =
+    (sigma_equiv_prod α₁ β₁).trans (prod_congr_right e) :=
+by { ext ⟨a, b⟩ : 1, simp }
+
+lemma sigma_equiv_prod_sigma_congr_right :
+  (sigma_equiv_prod α₁ β₁).symm.trans (sigma_congr_right e) =
+    (prod_congr_right e).trans (sigma_equiv_prod α₁ β₂).symm :=
+by { ext ⟨a, b⟩ : 1, simp }
+
+end prod_congr
+
+namespace perm
+
+variables {α₁ β₁ β₂ : Type*} [decidable_eq α₁] (a : α₁) (e : perm β₁)
+
+/-- `prod_extend_right a e` extends `e : perm β` to `perm (α × β)` by sending `(a, b)` to
+`(a, e b)` and keeping the other `(a', b)` fixed. -/
+def prod_extend_right : perm (α₁ × β₁) :=
+{ to_fun := λ ab, if ab.fst = a then (a, e ab.snd) else ab,
+  inv_fun := λ ab, if ab.fst = a then (a, e⁻¹ ab.snd) else ab,
+  left_inv := by { rintros ⟨k', x⟩, simp only, split_ifs with h; simp [h] },
+  right_inv := by { rintros ⟨k', x⟩, simp only, split_ifs with h; simp [h] } }
+
+@[simp] lemma prod_extend_right_apply_eq (b : β₁) :
+  prod_extend_right a e (a, b) = (a, e b) := if_pos rfl
+
+lemma prod_extend_right_apply_ne {a a' : α₁} (h : a' ≠ a) (b : β₁) :
+  prod_extend_right a e (a', b) = (a', b) := if_neg h
+
+lemma eq_of_prod_extend_right_ne {e : perm β₁} {a a' : α₁} {b : β₁}
+  (h : prod_extend_right a e (a', b) ≠ (a', b)) : a' = a :=
+by { contrapose! h, exact prod_extend_right_apply_ne _ h _ }
+
+@[simp] lemma fst_prod_extend_right (ab : α₁ × β₁) :
+  (prod_extend_right a e ab).fst = ab.fst :=
+begin
+  rw [prod_extend_right, coe_fn_mk],
+  split_ifs with h,
+  { rw h },
+  { refl }
+end
+
+end perm
+
 section
 /-- The type of functions to a product `α × β` is equivalent to the type of pairs of functions
 `γ → α` and `γ → β`. -/

src/data/fintype/basic.lean

@@ -783,6 +783,11 @@ instance pfun_fintype (p : Prop) [decidable p] (α : p → Type*)
 if hp : p then fintype.of_equiv (α hp) ⟨λ a _, a, λ f, f hp, λ _, rfl, λ _, rfl⟩
           else ⟨singleton (λ h, (hp h).elim), by simp [hp, function.funext_iff]⟩
 
+@[simp] lemma finset.univ_pi_univ {α : Type*} {β : α → Type*}
+  [decidable_eq α] [fintype α] [∀a, fintype (β a)] :
+  finset.univ.pi (λ a : α, (finset.univ : finset (β a))) = finset.univ :=
+by { ext, simp }
+
 lemma mem_image_univ_iff_mem_range
   {α β : Type*} [fintype α] [decidable_eq β] {f : α → β} {b : β} :
   b ∈ univ.image f ↔ b ∈ set.range f :=

src/group_theory/perm/sign.lean

@@ -576,7 +576,7 @@ calc sign f = sign (@subtype_perm _ f (λ x, f x ≠ x) (by simp)) :
 
 def is_cycle (f : perm β) := ∃ x, f x ≠ x ∧ ∀ y, f y ≠ y → ∃ i : ℤ, (f ^ i) x = y
 
-lemma is_cycle_swap {x y : α} (hxy : x ≠ y) : is_cycle (swap x y) :=
+lemma is_cycle_swap {α : Type*} [decidable_eq α] {x y : α} (hxy : x ≠ y) : is_cycle (swap x y) :=
 ⟨y, by rwa swap_apply_right,
   λ a (ha : ite (a = x) y (ite (a = y) x a) ≠ a),
     if hya : y = a then ⟨0, hya⟩
@@ -595,7 +595,7 @@ let ⟨a, ha⟩ := hg.2 x hx in
 let ⟨b, hb⟩ := hg.2 y hy in
 ⟨b - a, by rw [← ha, ← mul_apply, ← gpow_add, sub_add_cancel, hb]⟩
 
-lemma is_cycle_swap_mul_aux₁ : ∀ (n : ℕ) {b x : α} {f : perm α}
+lemma is_cycle_swap_mul_aux₁ {α : Type*} [decidable_eq α] : ∀ (n : ℕ) {b x : α} {f : perm α}
   (hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
   ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
 | 0         := λ b x f hb h, ⟨0, h⟩
@@ -614,7 +614,7 @@ lemma is_cycle_swap_mul_aux₁ : ∀ (n : ℕ) {b x : α} {f : perm α}
     ⟨i + 1, by rw [add_comm, gpow_add, mul_apply, hi, gpow_one, mul_apply, apply_inv_self,
         swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (ne.symm hfbx)]⟩
 
-lemma is_cycle_swap_mul_aux₂ : ∀ (n : ℤ) {b x : α} {f : perm α}
+lemma is_cycle_swap_mul_aux₂ {α : Type*} [decidable_eq α] : ∀ (n : ℤ) {b x : α} {f : perm α}
   (hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
   ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
 | (n : ℕ) := λ b x f, is_cycle_swap_mul_aux₁ n
@@ -636,7 +636,8 @@ lemma is_cycle_swap_mul_aux₂ : ∀ (n : ℤ) {b x : α} {f : perm α}
       mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x, gpow_add, gpow_one,
       mul_apply, mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx')]⟩
 
-lemma eq_swap_of_is_cycle_of_apply_apply_eq_self {f : perm α} (hf : is_cycle f) {x : α}
+lemma eq_swap_of_is_cycle_of_apply_apply_eq_self {α : Type*} [decidable_eq α]
+  {f : perm α} (hf : is_cycle f) {x : α}
   (hfx : f x ≠ x) (hffx : f (f x) = x) : f = swap x (f x) :=
 equiv.ext $ λ y,
 let ⟨z, hz⟩ := hf in
@@ -653,7 +654,7 @@ else begin
   { rw [← hj, hji] at hfyx, cc }
 end
 
-lemma is_cycle_swap_mul {f : perm α} (hf : is_cycle f) {x : α}
+lemma is_cycle_swap_mul {α : Type*} [decidable_eq α] {f : perm α} (hf : is_cycle f) {x : α}
   (hx : f x ≠ x) (hffx : f (f x) ≠ x) : is_cycle (swap x (f x) * f) :=
 ⟨f x, by simp only [swap_apply_def, mul_apply];
         split_ifs; simp [injective.eq_iff f.injective] at *; cc,
@@ -664,14 +665,14 @@ lemma is_cycle_swap_mul {f : perm α} (hf : is_cycle f) {x : α}
     ... =  y : by rwa [← gpow_add, sub_add_cancel],
   is_cycle_swap_mul_aux₂ (i - 1) hy hi⟩
 
-@[simp] lemma support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support = {x, y} :=
+@[simp] lemma support_swap {x y : α} (hxy : x ≠ y) : (swap x y).support = {x, y} :=
 finset.ext $ λ a, by simp [swap_apply_def]; split_ifs; cc
 
-lemma card_support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support.card = 2 :=
+lemma card_support_swap {x y : α} (hxy : x ≠ y) : (swap x y).support.card = 2 :=
 show (swap x y).support.card = finset.card ⟨x::y::0, by simp [hxy]⟩,
 from congr_arg card $ by rw [support_swap hxy]; simp [*, finset.ext_iff]; cc
 
-lemma sign_cycle [fintype α] : ∀ {f : perm α} (hf : is_cycle f),
+lemma sign_cycle : ∀ {f : perm α} (hf : is_cycle f),
   sign f = -(-1) ^ f.support.card
 | f := λ hf,
 let ⟨x, hx⟩ := hf in
@@ -698,6 +699,72 @@ calc sign f = sign (swap x (f x) * (swap x (f x) * f)) :
       pow_one, units.neg_mul_neg]
 using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ f, f.support.card)⟩]}
 
+/-- If we apply `prod_extend_right a (σ a)` for all `a : α` in turn,
+we get `prod_congr_right σ`. -/
+lemma prod_prod_extend_right {α : Type*} [decidable_eq α] (σ : α → perm β)
+  {l : list α} (hl : l.nodup) (mem_l : ∀ a, a ∈ l) :
+  (l.map (λ a, prod_extend_right a (σ a))).prod = prod_congr_right σ :=
+begin
+  ext ⟨a, b⟩ : 1,
+  -- We'll use induction on the list of elements,
+  -- but we have to keep track of whether we already passed `a` in the list.
+  suffices : (a ∈ l ∧ (l.map (λ a, prod_extend_right a (σ a))).prod (a, b) = (a, σ a b)) ∨
+             (a ∉ l ∧ (l.map (λ a, prod_extend_right a (σ a))).prod (a, b) = (a, b)),
+  { obtain ⟨_, prod_eq⟩ := or.resolve_right this (not_and.mpr (λ h _, h (mem_l a))),
+    rw [prod_eq, prod_congr_right_apply] },
+  clear mem_l,
+
+  induction l with a' l ih,
+  { refine or.inr ⟨list.not_mem_nil _, _⟩,
+    rw [list.map_nil, list.prod_nil, one_apply] },
+
+  rw [list.map_cons, list.prod_cons, mul_apply],
+  rcases ih (list.nodup_cons.mp hl).2 with ⟨mem_l, prod_eq⟩ | ⟨not_mem_l, prod_eq⟩; rw prod_eq,
+  { refine or.inl ⟨list.mem_cons_of_mem _ mem_l, _⟩,
+    rw prod_extend_right_apply_ne _ (λ (h : a = a'), (list.nodup_cons.mp hl).1 (h ▸ mem_l)) },
+  by_cases ha' : a = a',
+  { rw ← ha' at *,
+    refine or.inl ⟨l.mem_cons_self a, _⟩,
+    rw prod_extend_right_apply_eq },
+  { refine or.inr ⟨λ h, not_or ha' not_mem_l ((list.mem_cons_iff _ _ _).mp h), _⟩,
+    rw prod_extend_right_apply_ne _ ha' },
+end
+
+section
+
+open_locale classical
+
+lemma sign_prod_extend_right [fintype β] (a : α) (σ : perm β) :
+  (prod_extend_right a σ).sign = σ.sign :=
+sign_bij (λ (ab : α × β) _, ab.snd)
+  (λ ⟨a', b⟩ hab hab', by simp [eq_of_prod_extend_right_ne hab])
+  (λ ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ hab₁ hab₂ h,
+    by simpa [eq_of_prod_extend_right_ne hab₁, eq_of_prod_extend_right_ne hab₂] using h)
+  (λ y hy, ⟨(a, y), by simpa, by simp⟩)
+
+lemma sign_prod_congr_right [fintype β] (σ : α → perm β) :
+  sign (prod_congr_right σ) = ∏ k, (σ k).sign :=
+begin
+  obtain ⟨l, hl, mem_l⟩ := fintype.exists_univ_list α,
+  have l_to_finset : l.to_finset = finset.univ,
+  { apply eq_top_iff.mpr,
+    intros b _,
+    exact list.mem_to_finset.mpr (mem_l b) },
+  rw [← prod_prod_extend_right σ hl mem_l, sign.map_list_prod,
+      list.map_map, ← l_to_finset, list.prod_to_finset _ hl],
+  simp_rw ← λ a, sign_prod_extend_right a (σ a)
+end
+
+lemma sign_prod_congr_left [fintype β] (σ : α → perm β) :
+  sign (prod_congr_left σ) = ∏ k, (σ k).sign :=
+begin
+  refine (sign_eq_sign_of_equiv _ _ (prod_comm β α) _).trans (sign_prod_congr_right σ),
+  rintro ⟨b, α⟩,
+  refl
+end
+
+end
+
 end sign
 
 end equiv.perm

src/linear_algebra/determinant.lean

@@ -269,4 +269,68 @@ begin
   simp [update_column_transpose, det_transpose]
 end
 
+@[simp] lemma det_block_diagonal {o : Type*} [fintype o] [decidable_eq o] (M : o → matrix n n R) :
+  (block_diagonal M).det = ∏ k, (M k).det :=
+begin
+  -- Rewrite the determinants as a sum over permutations.
+  unfold det,
+  -- The right hand side is a product of sums, rewrite it as a sum of products.
+  rw finset.prod_sum,
+  simp_rw [finset.mem_univ, finset.prod_attach_univ, finset.univ_pi_univ],
+  -- We claim that the only permutations contributing to the sum are those that
+  -- preserve their second component.
+  let preserving_snd : finset (equiv.perm (n × o)) :=
+    finset.univ.filter (λ σ, ∀ x, (σ x).snd = x.snd),
+  have mem_preserving_snd : ∀ {σ : equiv.perm (n × o)},
+    σ ∈ preserving_snd ↔ ∀ x, (σ x).snd = x.snd :=
+    λ σ, finset.mem_filter.trans ⟨λ h, h.2, λ h, ⟨finset.mem_univ _, h⟩⟩,
+  rw ← finset.sum_subset (finset.subset_univ preserving_snd) _,
+  -- And that these are in bijection with `o → equiv.perm m`.
+  rw (finset.sum_bij (λ (σ : ∀ (k : o), k ∈ finset.univ → equiv.perm n) _,
+                        prod_congr_left (λ k, σ k (finset.mem_univ k))) _ _ _ _).symm,
+  { intros σ _,
+    rw mem_preserving_snd,
+    rintros ⟨k, x⟩,
+    simp },
+  { intros σ _,
+    rw finset.prod_mul_distrib,
+    congr,
+    { convert congr_arg (λ (x : units ℤ), (↑x : R)) (sign_prod_congr_left (λ k, σ k _)).symm,
+      simp, congr, ext, congr },
+    rw [← finset.univ_product_univ, finset.prod_product, finset.prod_comm],
+    simp },
+  { intros σ σ' _ _ eq,
+    ext x hx k,
+    simp only at eq,
+    have : ∀ k x, prod_congr_left (λ k, σ k (finset.mem_univ _)) (k, x) =
+                  prod_congr_left (λ k, σ' k (finset.mem_univ _)) (k, x) :=
+      λ k x, by rw eq,
+    simp only [prod_congr_left_apply, prod.mk.inj_iff] at this,
+    exact (this k x).1 },
+  { intros σ hσ,
+    rw mem_preserving_snd at hσ,
+    have hσ' : ∀ x, (σ⁻¹ x).snd = x.snd,
+    { intro x, conv_rhs { rw [← perm.apply_inv_self σ x, hσ] } },
+    have mk_apply_eq : ∀ k x, ((σ (x, k)).fst, k) = σ (x, k),
+    { intros k x,
+      ext; simp [hσ] },
+    have mk_inv_apply_eq : ∀ k x, ((σ⁻¹ (x, k)).fst, k) = σ⁻¹ (x, k),
+    { intros k x,
+      conv_lhs { rw ← perm.apply_inv_self σ (x, k) },
+      ext; simp [hσ'] },
+    refine ⟨λ k _, ⟨λ x, (σ (x, k)).fst, λ x, (σ⁻¹ (x, k)).fst, _, _⟩, _, _⟩,
+    { intro x,
+      simp [mk_apply_eq, mk_inv_apply_eq] },
+    { intro x,
+      simp [mk_apply_eq, mk_inv_apply_eq] },
+    { apply finset.mem_univ },
+    { ext ⟨k, x⟩; simp [hσ] } },
+  { intros σ _ hσ,
+    rw mem_preserving_snd at hσ,
+    obtain ⟨⟨k, x⟩, hkx⟩ := not_forall.mp hσ,
+    rw [finset.prod_eq_zero (finset.mem_univ (k, x)), mul_zero],
+    rw [← @prod.mk.eta _ _ (σ (k, x)), block_diagonal_apply_ne],
+    exact hkx }
+end
+
 end matrix