Theorems · Theorem · linear algebra

AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply

∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v : Fin (n + 2) → M),
  (AlternatingMap.alternatizeUncurryFin (AlternatingMap.alternatizeUncurryFinLM ∘ₗ f)) v =
    ∑ i,
      ∑ j ≥ i,
        (-1) ^ (↑i + ↑j) •
          (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
            ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))

If f is a bilinear map taking values in the space of alternating maps, then evaluation of the twice uncurried f on a tuple of vectors v can be represented as a sum of $$ f(v_i, v_j; v_0, \dots, \hat{v_i}, \dots, \hat{v_j}-) - f(v_j, v_i; v_0, \dots, \hat{v_i}, \dots, \hat{v_j}-) $$ over all (i j : Fin (n + 2)), i < j, taken with appropriate signs. Here $\hat{v_i}$ and $\hat{v_j}$ mean that these vectors are removed from the tuple. We use pairs of i j : Fin (n + 1), i ≤ j, to encode pairs (i.castSucc : Fin (n + 2), j.succ : Fin (n + 2)), so the power of -1 is off by one compared to the informal texts. In particular, if f is symmetric in the first two arguments, then the resulting alternating map is zero, see alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric below.

Defined in

Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Cited by

2 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupAddCommGroupModuleModule