English
DomCoprod' applied to simple tensor yields DomCoprod.
Русский
DomCoprod' применённый к простому тензору даёт DomCoprod.
LaTeX
$$$$ domCoprod'(a \otimes_R' b) = domCoprod(a,b). $$$$
Lean4
/-- Let `v` be an `(n + 1)`-tuple with two equal elements `v i = v j`, `i ≠ j`.
Let `w i` (resp., `w j`) be the vector `v` with `i`th (resp., `j`th) element removed.
Then `(-1) ^ i • f (w i) + (-1) ^ j • f (w j) = 0`.
This follows from the fact that these two vectors differ by a permutation of sign `(-1) ^ (i + j)`.
These are the only two nonzero terms in the proof of `map_eq_zero_of_eq`
in the definition of `alternatizeUncurryFin` below. -/
theorem neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq (f : M [⋀^Fin n]→ₗ[R] N) {v : Fin (n + 1) → M}
{i j : Fin (n + 1)} (hvij : v i = v j) (hij : i ≠ j) :
(-1) ^ (i : ℕ) • f (i.removeNth v) + (-1) ^ (j : ℕ) • f (j.removeNth v) = 0 :=
by
rcases exists_succAbove_eq hij with ⟨i, rfl⟩
obtain ⟨m, rfl⟩ : ∃ m, m + 1 = n := by simp [i.pos]
rw [← (i.predAbove j).insertNth_self_removeNth (removeNth _ _), ← removeNth_removeNth_eq_swap, removeNth,
succAbove_succAbove_predAbove, map_insertNth, ← neg_one_pow_smul_map_insertNth, insertNth_removeNth,
update_eq_self_iff.2, smul_smul, ← pow_add, neg_one_pow_succAbove_add_predAbove, neg_smul, pow_add, mul_smul,
smul_smul (_ ^ i.val), ← sq, ← pow_mul, pow_mul', neg_one_pow_two, one_pow, one_smul, neg_add_cancel]
exact hvij.symm
