English
A general determinant identity for Kronecker bilinear maps involving A, B and an appropriate bilinear f.
Русский
Обобщённая тождество определителя для билинейного отображения Кронекера, связанное с A, B и соответствующим билинейным f.
LaTeX
$$$\det(\mathrm{kroneckerMapBilinear} f A B) = \det(A^{(1)})^{|B|} \cdot \det(B^{(1)})^{|A|}$, где $A^{(1)} = A.map(a \mapsto f(a,1))$, $B^{(1)} = B.map(b \mapsto f(1,b))$ и $|X|$ обозначает кардинал множества X.$$
Lean4
/-- `determinant` of `Matrix.kroneckerMapBilinear`.
This is primarily used with `R = ℕ` to prove `Matrix.det_kronecker`. -/
theorem det_kroneckerMapBilinear [Semiring S] [Semiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
[NonAssocSemiring α] [NonAssocSemiring β] [CommRing γ] [Module R α] [Module S β] [Module R γ] [Module S γ]
[SMulCommClass S R γ] (f : α →ₗ[R] β →ₗ[S] γ) (h_comm : ∀ a b a' b', f (a * b) (a' * b') = f a a' * f b b')
(A : Matrix m m α) (B : Matrix n n β) :
det (kroneckerMapBilinear f A B) =
det (A.map fun a => f a 1) ^ Fintype.card n * det (B.map fun b => f 1 b) ^ Fintype.card m :=
calc
det (kroneckerMapBilinear f A B) = det (kroneckerMapBilinear f A 1 * kroneckerMapBilinear f 1 B) := by
rw [← kroneckerMapBilinear_mul_mul f h_comm, Matrix.mul_one, Matrix.one_mul]
_ =
det (blockDiagonal fun (_ : n) => A.map fun a => f a 1) *
det (blockDiagonal fun (_ : m) => B.map fun b => f 1 b) :=
by
rw [det_mul, ← diagonal_one, ← diagonal_one, kroneckerMapBilinear_apply_apply,
kroneckerMap_diagonal_right _ fun _ => _, kroneckerMapBilinear_apply_apply,
kroneckerMap_diagonal_left _ fun _ => _, det_reindex_self]
· intro; exact LinearMap.map_zero₂ _ _
· intro; exact map_zero _
_ = _ := by simp_rw [det_blockDiagonal, Finset.prod_const, Finset.card_univ]
