English
If swapping two indices i and j in σ, while v(i) = v(j), then the sum of two summands with σ and swap(i,j)•σ cancels to zero.
Русский
Если подменить индексы i и j в σ при условии v(i)=v(j), то сумма двух суммант равна нулю.
LaTeX
$$$$\text{domCoprod.summand}(a,b,σ)\,v + \text{domCoprod.summand}(a,b,\text{swap } i j \cdot σ)\,v = 0.$$$$
Lean4
/-- Swapping elements in `σ` with equal values in `v` results in an addition that cancels -/
theorem summand_add_swap_smul_eq_zero (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb)
{v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb} (hv : v i = v j) (hij : i ≠ j) :
domCoprod.summand a b σ v + domCoprod.summand a b (swap i j • σ) v = 0 :=
by
refine Quotient.inductionOn' σ fun σ => ?_
dsimp only [Quotient.liftOn'_mk'', Quotient.map'_mk'', MulAction.Quotient.smul_mk, domCoprod.summand]
rw [smul_eq_mul, Perm.sign_mul, Perm.sign_swap hij]
simp only [one_mul, neg_mul, Function.comp_apply, Units.neg_smul, Perm.coe_mul, MultilinearMap.smul_apply,
MultilinearMap.neg_apply, MultilinearMap.domDomCongr_apply, MultilinearMap.domCoprod_apply]
convert add_neg_cancel (G := N₁ ⊗[R'] N₂) _ using 6 <;>
· ext k
rw [Equiv.apply_swap_eq_self hv]
