English
Taking alternatization of a domCoprod equals a scaled domCoprod of alternatizations.
Русский
Чередование domCoprod даёт масштабированную комбинацию чередований.
LaTeX
$$$$ MultilinearMap.alternatization( (a.domCoprod b) ) = (|ιa|!)(|ιb|!) \cdot (a.domCoprod b). $$$$
Lean4
/-- Taking the `MultilinearMap.alternatization` of the `MultilinearMap.domCoprod` of two
`AlternatingMap`s gives a scaled version of the `AlternatingMap.coprod` of those maps.
-/
theorem domCoprod_alternization_eq [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) :
MultilinearMap.alternatization
(MultilinearMap.domCoprod a b : MultilinearMap R' (fun _ : ιa ⊕ ιb => Mᵢ) (N₁ ⊗ N₂)) =
((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b :=
by
rw [MultilinearMap.domCoprod_alternization, coe_alternatization, coe_alternatization, mul_smul, ←
AlternatingMap.domCoprod'_apply, ← AlternatingMap.domCoprod'_apply, ← TensorProduct.smul_tmul',
TensorProduct.tmul_smul, LinearMap.map_smul_of_tower AlternatingMap.domCoprod',
LinearMap.map_smul_of_tower AlternatingMap.domCoprod']
