Exchanging two blocks of arguments of an alternating map

An alternating map f in a + b + (c + d) arguments is evaluated on the concatenation (x, y, z, w) of four families of lengths a, b, c and d. Exchanging the two middle blocks y and z permutes the arguments by a block swap, which has b * c inversions; hence f (x, z, y, w) = (-1) ^ (b * c) • f (x, y, z, w) (AlternatingMap.map_append_append_comm). This is the Koszul sign rule for reordering two blocks of vectors in a determinant, as in the multiplicativity of the torsion of chain complexes.

Similarly, negating the last block y of a concatenation (x, y) of families of lengths a and b multiplies the value of an alternating map by (-1) ^ b (AlternatingMap.map_append_neg), as for the negated differential of a shifted chain complex.

theorem AlternatingMap.map_append_append_comm {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommGroup N] [Module R N] {a b c d : ℕ} (f : M [⋀^Fin (a + b + (c + d))]→ₗ[R] N) (x : Fin a → M) (y : Fin b → M) (z : Fin c → M) (w : Fin d → M) : f (Fin.append (Fin.append x z) (Fin.append y w) ∘ Fin.cast ⋯) = (-1) ^ (b * c) • f (Fin.append (Fin.append x y) (Fin.append z w))

Exchanging the two middle blocks of arguments, of lengths b and c, of an alternating map evaluated on a concatenation of four families multiplies its value by (-1) ^ (b * c).

theorem AlternatingMap.map_append_neg {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {a b : ℕ} (f : M [⋀^Fin (a + b)]→ₗ[R] N) (x : Fin a → M) (y : Fin b → M) : f (Fin.append x (-y)) = (-1) ^ b • f (Fin.append x y)

Negating the last block of arguments, of length b, of an alternating map evaluated on a concatenation of two families multiplies its value by (-1) ^ b.