English
Taking alternatization of domCoprod is the same as domCoprod of alternatizations.
Русский
Получение alternatization(domCoprod) равно domCoprod(alternatization).
LaTeX
$$$$ MultilinearMap.alternatization(\text{domCoprod } a b) = a.alternatization.\text{domCoprod } (\text{MultilinearMap.alternatization } b). $$$$
Lean4
/-- Computing the `MultilinearMap.alternatization` of the `MultilinearMap.domCoprod` is the same
as computing the `AlternatingMap.domCoprod` of the `MultilinearMap.alternatization`s.
-/
theorem domCoprod_alternization [DecidableEq ιa] [DecidableEq ιb] (a : MultilinearMap R' (fun _ : ιa => Mᵢ) N₁)
(b : MultilinearMap R' (fun _ : ιb => Mᵢ) N₂) :
MultilinearMap.alternatization (MultilinearMap.domCoprod a b) =
a.alternatization.domCoprod (MultilinearMap.alternatization b) :=
by
apply coe_multilinearMap_injective
rw [domCoprod_coe, MultilinearMap.alternatization_coe,
Finset.sum_partition (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)]
congr 1
ext1 σ
induction σ using Quotient.inductionOn' with
| h σ =>
set f := sumCongrHom ιa ιb
calc
∑ τ ∈ _, sign τ • domDomCongr τ (a.domCoprod b) =
∑ τ ∈ {τ | τ⁻¹ * σ ∈ f.range}, sign τ • domDomCongr τ (a.domCoprod b) :=
by simp [QuotientGroup.leftRel_apply, f]
_ = ∑ τ ∈ {τ | τ⁻¹ ∈ f.range}, sign (σ * τ) • domDomCongr (σ * τ) (a.domCoprod b) :=
by
conv_lhs => rw [← Finset.map_univ_equiv (Equiv.mulLeft σ), Finset.filter_map, Finset.sum_map]
simp [Function.comp_def, -MonoidHom.mem_range]
_ = ∑ τ, sign (σ * f τ) • domDomCongr (σ * f τ) (a.domCoprod b) := by
simp_rw [f, Subgroup.inv_mem_iff, MonoidHom.mem_range, Finset.univ_filter_exists,
Finset.sum_image sumCongrHom_injective.injOn]
_ =
∑ τ : Perm ιa × Perm ιb,
sign σ • (domDomCongrEquiv σ) (sign τ.1 • sign τ.2 • (domDomCongr τ.1 a).domCoprod (domDomCongr τ.2 b)) :=
by simp [f, domDomCongr_mul, domCoprod_domDomCongr_sumCongr, mul_smul]
_ = domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ) := by
simp [domCoprod.summand_mk'', domCoprod_alternization_coe, ← domDomCongrEquiv_apply, Finset.smul_sum,
← Finset.sum_product']
