English
If f is a symmetric bilinear map taking values in alternating maps, then the twice-uncurried version of f, when composed with alternatizeUncurryFinLM, is the zero map.
Русский
Если f—симметричная билинейная отображение, принимающее значения в чередующихся отображениях, то двойное «разворачивание» f после композиции с alternatizeUncurryFinLM даёт нулевое отображение.
LaTeX
$$$ alternatizeUncurryFin (alternatizeUncurryFinLM \\circ f) = 0 $$$
Lean4
/-- If `f` is a symmetric bilinear map taking values in the space of alternating maps,
then the twice uncurried `f` is zero. -/
theorem alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric {f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N}
(hf : ∀ x y, f x y = f y x) : alternatizeUncurryFin (alternatizeUncurryFinLM ∘ₗ f) = 0 :=
by
ext v
set a : Fin (n + 2) → Fin (n + 1) → N := fun i j ↦
(-1) ^ (i + j : ℕ) • f (v i) (i.removeNth v j) (j.removeNth (i.removeNth v))
suffices ∑ ij : Fin (n + 2) × Fin (n + 1), a ij.1 ij.2 = 0 by
simpa [a, alternatizeUncurryFin_apply, Finset.smul_sum, Fintype.sum_prod_type, mul_smul, pow_add] using this
set g : Fin (n + 2) × Fin (n + 1) → Fin (n + 2) × Fin (n + 1) := fun (i, j) ↦ (i.succAbove j, j.predAbove i)
have hg_invol : g.Involutive := by
intro (i, j)
simp [g, succAbove_succAbove_predAbove, predAbove_predAbove_succAbove]
refine Finset.sum_ninvolution g ?_ (by simp [g, succAbove_ne]) (by simp) hg_invol
intro (i, j)
simp only [a]
rw [hf (v i), ← removeNth_removeNth_eq_swap, removeNth_apply (i.succAbove j), succAbove_succAbove_predAbove,
neg_one_pow_succAbove_add_predAbove, neg_smul, removeNth_apply, add_neg_cancel]
