English
Let A and B be square matrices over a commutative semiring with AB = I. Then the matrix expression detp(1)A · (B · adjp(−1)B) + detp(−1)A · (B · adjp(1)B) is an additive unit, i.e. it has an additive inverse in the matrix additive monoid.
Русский
Пусть A и B — квадратные матрицы над коммутативной полугруппой, удовлетворяющие AB = I. Тогда выражение detp(1)A · (B · adjp(−1)B) + detp(−1)A · (B · adjp(1)B) является добавочным единичным элементом, то есть имеет аддитивного обратного.
LaTeX
$$$\text{Let } A,B \in M_n(R) \text{ with } AB=I. \quad \detp(1)A \cdot (B \cdot \operatorname{adj}_p(-1)B) + \detp(-1)A \cdot (B \cdot \operatorname{adj}_p(1)B) \text{ is an additive unit.}$$$
Lean4
theorem isAddUnit_detp_smul_mul_adjp (hAB : A * B = 1) :
IsAddUnit (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) :=
by
suffices h : ∀ {s t}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B)) from (h (by decide)).add (h (by decide))
intro s t h
rw [isAddUnit_iff]
intro i j
simp_rw [smul_apply, smul_eq_mul, mul_apply, detp, adjp_apply, mul_sum, sum_mul, IsAddUnit.sum_iff]
intro k hk σ hσ τ hτ
rw [mem_filter] at hσ
rw [mem_ofSign] at hσ hτ
rw [← hσ.1, ← hτ, ← sign_inv] at h
replace h := ne_of_apply_ne sign h
rw [ne_eq, eq_comm, eq_inv_iff_mul_eq_one] at h
obtain ⟨l, hl1, hl2⟩ := exists_mem_ne (one_lt_card_support_of_ne_one h) (τ⁻¹ j)
rw [mem_support, ne_comm] at hl1
rw [ne_eq, ← mem_singleton, ← mem_compl] at hl2
rw [← prod_mul_prod_compl {τ⁻¹ j}, mul_mul_mul_comm, mul_comm, ← smul_eq_mul]
apply IsAddUnit.smul_right
have h0 : ∀ k, k ∈ ({τ⁻¹ j} : Finset n)ᶜ ↔ τ k ∈ ({ j } : Finset n)ᶜ := by simp [inv_def, eq_symm_apply]
rw [← prod_equiv τ h0 fun _ _ ↦ rfl, ← prod_mul_distrib, ← mul_prod_erase _ _ hl2, ← smul_eq_mul]
exact (isAddUnit_mul hAB l (σ (τ l)) (τ l) hl1).smul_right _
