English
The domCoprod of alternating maps equals the formula for domCoprod applied to dotwise components.
Русский
DomCoprod чередующихся карт равен формуле domCoprod примененной к компонентам по точкам.
LaTeX
$$$$domCoprod(a,b) = \sum_{σ} domCoprod.summand(a,b,σ).$$$$
Lean4
/-- A helper lemma for `MultilinearMap.domCoprod_alternization`. -/
theorem domCoprod_alternization_coe [DecidableEq ιa] [DecidableEq ιb] (a : MultilinearMap R' (fun _ : ιa => Mᵢ) N₁)
(b : MultilinearMap R' (fun _ : ιb => Mᵢ) N₂) :
MultilinearMap.domCoprod (MultilinearMap.alternatization a) (MultilinearMap.alternatization b) =
∑ σa : Perm ιa,
∑ σb : Perm ιb,
Equiv.Perm.sign σa • Equiv.Perm.sign σb • MultilinearMap.domCoprod (a.domDomCongr σa) (b.domDomCongr σb) :=
by
simp_rw [← MultilinearMap.domCoprod'_apply, MultilinearMap.alternatization_coe]
simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, _root_.map_sum, ← TensorProduct.smul_tmul',
TensorProduct.tmul_smul]
rfl
