feat(linear_algebra/determinant): determinant of a block triangular matrix (#6050)

Add lemmas for determinants of block triangular matrices.



Co-authored-by: paulvanwamelen <30371019+paulvanwamelen@users.noreply.github.com>

Author: paulvanwamelen

src/data/equiv/basic.lean

@@ -1289,12 +1289,20 @@ def subtype_subtype_equiv_subtype_exists {α : Type u} (p : α → Prop) (q : su
   λ⟨a, ha⟩, ⟨⟨a, ha.cases_on $ assume h _, h⟩, by { cases ha, exact ha_h }⟩,
   assume ⟨⟨a, ha⟩, h⟩, rfl, assume ⟨a, h₁, h₂⟩, rfl⟩
 
+@[simp] lemma subtype_subtype_equiv_subtype_exists_apply {α : Type u} (p : α → Prop)
+  (q : subtype p → Prop) (a) : (subtype_subtype_equiv_subtype_exists p q a : α) = a :=
+by { cases a, cases a_val, refl }
+
 /-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. -/
 def subtype_subtype_equiv_subtype_inter {α : Type u} (p q : α → Prop) :
   {x : subtype p // q x.1} ≃ subtype (λ x, p x ∧ q x) :=
 (subtype_subtype_equiv_subtype_exists p _).trans $
 subtype_equiv_right $ λ x, exists_prop
 
+@[simp] lemma subtype_subtype_equiv_subtype_inter_apply {α : Type u} (p q : α → Prop) (a) :
+  (subtype_subtype_equiv_subtype_inter p q a : α) = a :=
+by { cases a, cases a_val, refl }
+
 /-- If the outer subtype has more restrictive predicate than the inner one,
 then we can drop the latter. -/
 def subtype_subtype_equiv_subtype {α : Type u} {p q : α → Prop} (h : ∀ {x}, q x → p x) :
@@ -1304,6 +1312,11 @@ subtype_equiv_right $
 assume x,
 ⟨and.right, λ h₁, ⟨h h₁, h₁⟩⟩
 
+@[simp] lemma subtype_subtype_equiv_subtype_apply {α : Type u} {p q : α → Prop} (h : ∀ x, q x → p x)
+  (a : {x : subtype p // q x.1}) :
+  (subtype_subtype_equiv_subtype h a : α) = a :=
+by { cases a, cases a_val, refl }
+
 /-- If a proposition holds for all elements, then the subtype is
 equivalent to the original type. -/
 def subtype_univ_equiv {α : Type u} {p : α → Prop} (h : ∀ x, p x) :

src/data/matrix/basic.lean

@@ -985,22 +985,22 @@ rfl
   from_blocks A B C D (sum.inr i) (sum.inr j) = D i j :=
 rfl
 
-/-- Given a matrix whose row and column indexes are sum types, we can extract the correspnding
+/-- Given a matrix whose row and column indexes are sum types, we can extract the corresponding
 "top left" submatrix. -/
 def to_blocks₁₁ (M : matrix (n ⊕ o) (l ⊕ m) α) : matrix n l α :=
 λ i j, M (sum.inl i) (sum.inl j)
 
-/-- Given a matrix whose row and column indexes are sum types, we can extract the correspnding
+/-- Given a matrix whose row and column indexes are sum types, we can extract the corresponding
 "top right" submatrix. -/
 def to_blocks₁₂ (M : matrix (n ⊕ o) (l ⊕ m) α) : matrix n m α :=
 λ i j, M (sum.inl i) (sum.inr j)
 
-/-- Given a matrix whose row and column indexes are sum types, we can extract the correspnding
+/-- Given a matrix whose row and column indexes are sum types, we can extract the corresponding
 "bottom left" submatrix. -/
 def to_blocks₂₁ (M : matrix (n ⊕ o) (l ⊕ m) α) : matrix o l α :=
 λ i j, M (sum.inr i) (sum.inl j)
 
-/-- Given a matrix whose row and column indexes are sum types, we can extract the correspnding
+/-- Given a matrix whose row and column indexes are sum types, we can extract the corresponding
 "bottom right" submatrix. -/
 def to_blocks₂₂ (M : matrix (n ⊕ o) (l ⊕ m) α) : matrix o m α :=
 λ i j, M (sum.inr i) (sum.inr j)
@@ -1038,6 +1038,39 @@ begin
   ext i j, rcases i; rcases j; simp [from_blocks],
 end
 
+/-- Let `p` pick out certain rows and `q` pick out certain columns of a matrix `M`. Then
+  `to_block M p q` is the corresponding block matrix. -/
+def to_block (M : matrix m n α) (p : m → Prop) [decidable_pred p]
+  (q : n → Prop) [decidable_pred q] : matrix {a // p a} {a // q a} α := M.minor coe coe
+
+@[simp] lemma to_block_apply (M : matrix m n α) (p : m → Prop) [decidable_pred p]
+  (q : n → Prop) [decidable_pred q] (i : {a // p a}) (j : {a // q a}) :
+  to_block M p q i j = M ↑i ↑j := rfl
+
+/-- Let `b` map rows and columns of a square matrix `M` to blocks. Then
+  `to_square_block M b k` is the block `k` matrix. -/
+def to_square_block (M : matrix m m α) {n : nat} (b : m → fin n) (k : fin n) :
+  matrix {a // b a = k} {a // b a = k} α := M.minor coe coe
+
+@[simp] lemma to_square_block_def (M : matrix m m α) {n : nat} (b : m → fin n) (k : fin n) :
+  to_square_block M b k = λ i j, M ↑i ↑j := rfl
+
+/-- Alternate version with `b : m → nat`. Let `b` map rows and columns of a square matrix `M` to
+  blocks. Then `to_square_block' M b k` is the block `k` matrix. -/
+def to_square_block' (M : matrix m m α) (b : m → nat) (k : nat) :
+  matrix {a // b a = k} {a // b a = k} α := M.minor coe coe
+
+@[simp] lemma to_square_block_def' (M : matrix m m α) (b : m → nat) (k : nat) :
+  to_square_block' M b k = λ i j, M ↑i ↑j := rfl
+
+/-- Let `p` pick out certain rows and columns of a square matrix `M`. Then
+  `to_square_block_prop M p` is the corresponding block matrix. -/
+def to_square_block_prop (M : matrix m m α) (p : m → Prop) [decidable_pred p] :
+  matrix {a // p a} {a // p a} α := M.minor coe coe
+
+@[simp] lemma to_square_block_prop_def (M : matrix m m α) (p : m → Prop) [decidable_pred p] :
+  to_square_block_prop M p = λ i j, M ↑i ↑j := rfl
+
 variables [semiring α]
 
 lemma from_blocks_smul

src/group_theory/perm/basic.lean

@@ -240,6 +240,12 @@ else by simp [h, of_subtype_apply_of_not_mem f h]
 equiv.ext $ λ ⟨x, hx⟩, by { dsimp [subtype_perm, of_subtype],
   simp only [show p x, from hx, dif_pos, subtype.coe_eta] }
 
+instance perm_unique {n : Type*} [unique n] : unique (equiv.perm n) :=
+{ default := 1,
+  uniq := λ σ, equiv.ext (λ i, subsingleton.elim _ _) }
+
+@[simp] lemma default_perm {n : Type*} : default (equiv.perm n) = 1 := rfl
+
 end perm
 
 section swap

src/group_theory/perm/sign.lean

@@ -86,6 +86,37 @@ f.subtype_perm (λ x, ⟨h x, λ h₂, f.inv_apply_self x ▸ perm_inv_on_of_per
   (h : ∀ x, p x → p ((1 : perm α) x)) : @subtype_perm_of_fintype α 1 p _ h = 1 :=
 equiv.ext $ λ ⟨_, _⟩, rfl
 
+lemma perm_maps_to_inl_iff_maps_to_inr {m n : Type*} [fintype m] [fintype n]
+  (σ : equiv.perm (m ⊕ n)) :
+  set.maps_to σ (set.range sum.inl) (set.range sum.inl) ↔
+  set.maps_to σ (set.range sum.inr) (set.range sum.inr) :=
+begin
+  split; id {
+    intros h,
+    classical,
+    rw ←perm_inv_maps_to_iff_maps_to at h,
+    intro x,
+    cases hx : σ x with l r, },
+  { rintros ⟨a, rfl⟩,
+    obtain ⟨y, hy⟩ := h ⟨l, rfl⟩,
+    rw [←hx, σ.inv_apply_self] at hy,
+    exact absurd hy sum.inl_ne_inr},
+  { rintros ⟨a, ha⟩, exact ⟨r, rfl⟩, },
+  { rintros ⟨a, ha⟩, exact ⟨l, rfl⟩, },
+  { rintros ⟨a, rfl⟩,
+    obtain ⟨y, hy⟩ := h ⟨r, rfl⟩,
+    rw [←hx, σ.inv_apply_self] at hy,
+    exact absurd hy sum.inr_ne_inl},
+end
+
+lemma perm_on_inl_iff_perm_on_inr {m n : Type*} [fintype m] [fintype n] (σ : equiv.perm (m ⊕ n)) :
+  (∀ a1, ∃ a2, sum.inl a2 = σ (sum.inl a1)) ↔ ∀ b1, ∃ b2, sum.inr b2 = σ (sum.inr b1) :=
+begin
+  have := perm_maps_to_inl_iff_maps_to_inr σ,
+  rw [set.maps_range_to, set.maps_range_to] at this,
+  convert this; simp
+end
+
 /-- Two permutations `f` and `g` are `disjoint` if their supports are disjoint, i.e.,
 every element is fixed either by `f`, or by `g`. -/
 def disjoint (f g : perm α) := ∀ x, f x = x ∨ g x = x

src/linear_algebra/determinant.lean

@@ -40,7 +40,8 @@ open equiv equiv.perm finset function
 namespace matrix
 open_locale matrix big_operators
 
-variables {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R]
+variables {m n : Type u} [decidable_eq n] [fintype n] [decidable_eq m] [fintype m]
+variables {R : Type v} [comm_ring R]
 
 local notation `ε` σ:max := ((sign σ : ℤ ) : R)
 
@@ -75,6 +76,24 @@ begin
   simp [det, card_eq_zero.mp h, perm_eq],
 end
 
+/-- If `n` has only one element, the determinant of an `n` by `n` matrix is just that element.
+Although `unique` implies `decidable_eq` and `fintype`, the instances might
+not be syntactically equal. Thus, we need to fill in the args explicitly. -/
+@[simp]
+lemma det_unique {n : Type*} [unique n] [decidable_eq n] [fintype n] (A : matrix n n R) :
+  det A = A (default n) (default n) :=
+by simp [det, univ_unique]
+
+lemma det_eq_elem_of_card_eq_one {A : matrix n n R} (h : fintype.card n = 1) (k : n) :
+  det A = A k k :=
+begin
+  have h1 : (univ : finset (perm n)) = {1},
+  { apply univ_eq_singleton_of_card_one (1 : perm n),
+    simp [card_univ, fintype.card_perm, h] },
+  have h2 := univ_eq_singleton_of_card_one k h,
+  simp [det, h1, h2],
+end
+
 lemma det_mul_aux {M N : matrix n n R} {p : n → n} (H : ¬bijective p) :
   ∑ σ : perm n, (ε σ) * ∏ x, (M (σ x) (p x) * N (p x) x) = 0 :=
 begin
@@ -344,4 +363,78 @@ begin
     exact hkx }
 end
 
+/-- The determinant of a 2x2 block matrix with the lower-left block equal to zero is the product of
+the determinants of the diagonal blocks. For the generalization to any number of blocks, see
+`matrix.upper_block_triangular_det`. -/
+lemma upper_two_block_triangular_det (A : matrix m m R) (B : matrix m n R) (D : matrix n n R) :
+  (matrix.from_blocks A B 0 D).det = A.det * D.det :=
+begin
+  unfold det,
+  rw sum_mul_sum,
+  let preserving_A : finset (perm (m ⊕ n)) :=
+    univ.filter (λ σ, ∀ x, ∃ y, sum.inl y = (σ (sum.inl x))),
+  simp_rw univ_product_univ,
+  have mem_preserving_A : ∀ {σ : perm (m ⊕ n)},
+    σ ∈ preserving_A ↔ ∀ x, ∃ y, sum.inl y = σ (sum.inl x) :=
+    λ σ, mem_filter.trans ⟨λ h, h.2, λ h, ⟨mem_univ _, h⟩⟩,
+  rw ← sum_subset (subset_univ preserving_A) _,
+  rw (sum_bij (λ (σ : perm m × perm n) _, equiv.sum_congr σ.fst σ.snd) _ _ _ _).symm,
+  { intros a ha,
+    rw mem_preserving_A,
+    intro x,
+    use a.fst x,
+    simp },
+  { simp only [forall_prop_of_true, prod.forall, mem_univ],
+    intros σ₁ σ₂,
+    rw fintype.prod_sum_type,
+    simp_rw [equiv.sum_congr_apply, sum.map_inr, sum.map_inl, from_blocks_apply₁₁,
+      from_blocks_apply₂₂],
+    have hr : ∀ (a b c d : R), (a * b) * (c * d) = a * c * (b * d), { intros, ac_refl },
+    rw hr,
+    congr,
+    norm_cast,
+    rw sign_sum_congr },
+  { intros σ₁ σ₂ h₁ h₂,
+    dsimp only [],
+    intro h,
+    have h2 : ∀ x, perm.sum_congr σ₁.fst σ₁.snd x = perm.sum_congr σ₂.fst σ₂.snd x,
+    { intro x, exact congr_fun (congr_arg to_fun h) x },
+    simp only [sum.map_inr, sum.map_inl, perm.sum_congr_apply, sum.forall] at h2,
+    ext,
+    { exact h2.left x },
+    { exact h2.right x }},
+  { intros σ hσ,
+    have h1 : ∀ (x : m ⊕ n), (∃ (a : m), sum.inl a = x) → (∃ (a : m), sum.inl a = σ x),
+    { rintros x ⟨a, ha⟩,
+      rw ← ha,
+      exact (@mem_preserving_A σ).mp hσ a },
+    have h2 : ∀ (x : m ⊕ n), (∃ (b : n), sum.inr b = x) → (∃ (b : n), sum.inr b = σ x),
+    { rintros x ⟨b, hb⟩,
+      rw ← hb,
+      exact (perm_on_inl_iff_perm_on_inr σ).mp ((@mem_preserving_A σ).mp hσ) b },
+    let σ₁' := subtype_perm_of_fintype σ h1,
+    let σ₂' := subtype_perm_of_fintype σ h2,
+    let σ₁ := perm_congr (equiv.set.range (@sum.inl m n) sum.injective_inl).symm σ₁',
+    let σ₂ := perm_congr (equiv.set.range (@sum.inr m n) sum.injective_inr).symm σ₂',
+    use [⟨σ₁, σ₂⟩, finset.mem_univ _],
+    ext,
+    cases x with a b,
+    { rw [equiv.sum_congr_apply, sum.map_inl, perm_congr_apply, equiv.symm_symm,
+        set.apply_range_symm (@sum.inl m n)],
+      erw subtype_perm_apply,
+      rw [set.range_apply, subtype.coe_mk, subtype.coe_mk] },
+    { rw [equiv.sum_congr_apply, sum.map_inr, perm_congr_apply, equiv.symm_symm,
+        set.apply_range_symm (@sum.inr m n)],
+      erw subtype_perm_apply,
+      rw [set.range_apply, subtype.coe_mk, subtype.coe_mk] }},
+  { intros σ h0 hσ,
+    obtain ⟨a, ha⟩ := not_forall.mp ((not_congr (@mem_preserving_A σ)).mp hσ),
+    generalize hx : σ (sum.inl a) = x,
+    cases x with a2 b,
+    { have hn := (not_exists.mp ha) a2,
+      exact absurd hx.symm hn },
+    { rw [finset.prod_eq_zero (finset.mem_univ (sum.inl a)), mul_zero],
+      rw [hx, from_blocks_apply₂₁], refl }}
+end
+
 end matrix