English
A similar product-map identity holds with roles reversed, mirroring the previous contraction statement.
Русский
Похожее тождество для prodMap с ролями наоборот, зеркалируя предыдущее тождество контура.
LaTeX
$$$(\mathrm{dualTensorHom}(R N Q) (g ⊗ q)).prodMap 0 = \, \mathrm{dualTensorHom}(R, M \times N, P \times Q) ((g \circ_\ell snd) ⊗_\ell inr(q)).$$$
Lean4
/-- As a matrix, `dualTensorHom` evaluated on a basis element of `M* ⊗ N` is a matrix with a
single one and zeros elsewhere -/
theorem toMatrix_dualTensorHom {m : Type*} {n : Type*} [Fintype m] [Finite n] [DecidableEq m] [DecidableEq n]
(bM : Basis m R M) (bN : Basis n R N) (j : m) (i : n) :
toMatrix bM bN (dualTensorHom R M N (bM.coord j ⊗ₜ bN i)) = single i j 1 :=
by
ext i' j'
by_cases hij : i = i' ∧ j = j' <;> simp [LinearMap.toMatrix_apply, Finsupp.single_eq_pi_single, hij]
rw [and_iff_not_or_not, Classical.not_not] at hij
rcases hij with hij | hij <;> simp [hij]
