English
The (i,i) entry of A * adjp(s) A equals detp(s) A; a precise identity linking detp with adjugate.
Русский
Диагональные элементы произведения A · adjp(s) A равны detp(s) A.
LaTeX
$$$(A \\cdot \\operatorname{adjp}(s) A)_{ii} = \\detp(s; A)$$$
Lean4
theorem detp_mul :
detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) :=
by
have hf {s t} {σ : Perm n} (hσ : σ ∈ ofSign s) : ofSign (t * s) = (ofSign t).map (mulRightEmbedding σ) :=
by
ext τ
simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right, mem_ofSign, map_mul, map_inv,
mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]
have h {s t} : detp s A * detp t B = ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k) :=
by
simp_rw [detp, sum_mul_sum, prod_mul_distrib]
refine sum_congr rfl fun σ hσ ↦ ?_
simp_rw [hf hσ, sum_map, mulRightEmbedding_apply, Perm.mul_apply]
exact sum_congr rfl fun τ hτ ↦ (congr_arg (_ * ·) (Equiv.prod_comp σ _).symm)
let ι : Perm n ↪ (n → n) := ⟨_, coe_fn_injective⟩
have hι {σ x} : ι σ x = σ x := rfl
let bij : Finset (n → n) := (disjUnion (ofSign 1) (ofSign (-1)) ofSign_disjoint).map ι
replace h (s) :
detp s (A * B) =
∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i : n, A i (σ i) * B (σ i) (τ i) +
(detp 1 A * detp s B + detp (-1) A * detp (-s) B) :=
by
simp_rw [h, neg_mul_neg, mul_one, detp, mul_apply, prod_univ_sum, Fintype.piFinset_univ]
rw [sum_comm, ← sum_compl_add_sum bij, sum_map, sum_disjUnion]
simp_rw [hι]
rw [h, h, neg_neg, add_assoc]
conv_rhs => rw [add_assoc]
refine congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (add_comm _ _)
replace hσ : ¬Function.Injective σ := by
contrapose! hσ
rw [notMem_compl, mem_map, ofSign_disjUnion]
exact ⟨Equiv.ofBijective σ hσ.bijective_of_finite, mem_univ _, rfl⟩
obtain ⟨i, j, hσ, hij⟩ := Function.not_injective_iff.mp hσ
replace hσ k : σ (swap i j k) = σ k := by
rw [swap_apply_def]
split_ifs with h h <;> simp only [hσ, h]
rw [← mul_neg_one, hf (mem_ofSign.mpr (sign_swap hij)), sum_map]
simp_rw [prod_mul_distrib, mulRightEmbedding_apply, Perm.mul_apply]
refine sum_congr rfl fun τ hτ ↦ congr_arg (_ * ·) ?_
rw [← Equiv.prod_comp (swap i j)]
simp only [hσ]
