English
The basic building block for domCoprod, called summand, behaves under permutation as a sign-twisted domCoprod. In particular, applying Summand to a quotient by σ is the sign of σ times the permutation-conjugated domCoprod.
Русский
Базовый элемент domCoprod, называемый summand, ведёт себя при перестановке как умножение на знак перестановки; конкретно, summand σ равен знаку σ умноженному на domCoprod, свернутому через σ.
LaTeX
$$$$\text{summand}(a,b,\sigma) = \operatorname{sign}(\sigma) \cdot (\text{domCoprod } a \ b)_{\text{domCongr}}(\sigma).$$$$
Lean4
/-- summand used in `AlternatingMap.domCoprod` -/
def summand (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb) :
MultilinearMap R' (fun _ : ιa ⊕ ιb => Mᵢ) (N₁ ⊗[R'] N₂) :=
Quotient.liftOn' σ
(fun σ =>
Equiv.Perm.sign σ • (MultilinearMap.domCoprod ↑a ↑b : MultilinearMap R' (fun _ => Mᵢ) (N₁ ⊗ N₂)).domDomCongr σ)
fun σ₁ σ₂ H => by
rw [QuotientGroup.leftRel_apply] at H
obtain ⟨⟨sl, sr⟩, h⟩ := H
ext v
simp only [MultilinearMap.domDomCongr_apply, MultilinearMap.domCoprod_apply, coe_multilinearMap,
MultilinearMap.smul_apply]
replace h := inv_mul_eq_iff_eq_mul.mp h.symm
have :
Equiv.Perm.sign (σ₁ * Perm.sumCongrHom _ _ (sl, sr)) =
Equiv.Perm.sign σ₁ * (Equiv.Perm.sign sl * Equiv.Perm.sign sr) :=
by simp
rw [h, this, mul_smul, mul_smul, smul_left_cancel_iff, ← TensorProduct.tmul_smul, TensorProduct.smul_tmul',
a.map_congr_perm _ sl, b.map_congr_perm _ sr]
simp only [Sum.map_inr, Perm.sumCongrHom_apply, Perm.sumCongr_apply, Sum.map_inl, Function.comp_def, Perm.coe_mul]
