Expanding two slots of a pure tensor in the standard basis

A pure tensor ⨂ₜ u over a constant family ν → R is multilinear in its slots, so plugging a vector into one slot and expanding that vector along the standard basis Pi.single a 1 turns the tensor into a sum (MultilinearMap.map_update_sum). Doing this at two distinct slots at once is the bookkeeping recorded here: the pure tensor whose slots i and j carry x and y is the double sum over the standard basis with coefficients the products x a * y b of the coordinates. The two slots have to be distinct for the two Function.updates to be independent; that is where Function.update_comm enters.

This is the shape that a diagonal expansion at two slots of a tensor power — a Brauer cup, say — is read through when one wants its coefficients, so it is stated here rather than in any one consumer. Pushing a matrix A through those two slots of a weighted sum of basis pure tensors is the immediate consequence recorded next to it: the weight matrix is replaced by its congruate A * K * Aᵀ, which is what makes a copairing at two slots invariant under the matrices preserving it.

Main results

• TauCeti.tprod_update_pair_expand: a pure tensor whose slots i and j carry arbitrary vectors of ν → R is the standard-basis expansion of those two slots.
• TauCeti.sum_sum_smul_tprod_update_pair_mulVec: pushing a matrix A through the slots i and j of a weighted sum of basis pure tensors congruates the weight matrix.

theorem TauCeti.tprod_update_pair_expand {ι : Type u_1} {ν : Type u_2} {R : Type u_3} [DecidableEq ι] [Fintype ν] [DecidableEq ν] [CommSemiring R] {i j : ι} (hij : i ≠ j) (u : ι → ν → R) (x y : ν → R) : (PiTensorProduct.tprod R) (Function.update (Function.update u i x) j y) = ∑ a : ν, ∑ b : ν, (x a * y b) • (PiTensorProduct.tprod R) (Function.update (Function.update u i (Pi.single a 1)) j (Pi.single b 1))

The bilinear expansion at two slots: a pure tensor over the constant family ν → R whose slots i and j carry arbitrary vectors is the standard-basis expansion of those two slots, with the product x a * y b of the two coordinates as the coefficient of the (a, b) term.

theorem TauCeti.sum_sum_smul_tprod_update_pair_mulVec {ι : Type u_1} {ν : Type u_2} {κ : Type u_3} {R : Type u_4} [DecidableEq ι] [Fintype ν] [DecidableEq ν] [Fintype κ] [DecidableEq κ] [CommSemiring R] (A : Matrix κ ν R) (K : Matrix ν ν R) {i j : ι} (hij : i ≠ j) (u : ι → κ → R) : ∑ x : ν, ∑ y : ν, K x y • (PiTensorProduct.tprod R) (Function.update (Function.update u i (A.mulVec (Pi.single x 1))) j (A.mulVec (Pi.single y 1))) = ∑ a : κ, ∑ b : κ, (A * K * A.transpose) a b • (PiTensorProduct.tprod R) (Function.update (Function.update u i (Pi.single a 1)) j (Pi.single b 1))

Congruence at two slots. Pushing a matrix A through the slots i and j of the weighted sum ∑ x y, K x y • ⨂ₜ of pure tensors of standard basis vectors re-expands it in the standard basis with the congruate A * K * Aᵀ as its weight. The matrix may be rectangular, so the two slots end up indexed by its row type. This is the general-slot form of Matrix.piTensorProductMap_bivector, which is the same statement on a tensor square; a copairing K at two slots is invariant under exactly the matrices with A * K * Aᵀ = K.