Pure tensors on two strands

Calculations on a tensor square index their pure tensors by Fin 2, and repeatedly need the same three pieces of bookkeeping: a sum over the functions Fin 2 → ι is a double sum, a pure tensor indexed by Fin 2 may be rewritten in ![·, ·] form, and pushing a matrix through both strands re-expands a basis pure tensor in the standard basis. None of them says anything about what the tensor square is being used for, so they live here rather than in any one consumer.

Main results

• TauCeti.sum_pi_fin_two: a sum over Fin 2 → ι is a double sum over ι.
• TauCeti.tprod_fin_two: a pure tensor on two strands is ⨂ₜ ![v 0, v 1].
• Matrix.piTensorProductMap_tprod_single: applying a matrix in both strands re-expands a basis pure tensor in the standard basis. Use it whenever a two-strand pure tensor of standard basis vectors is pushed through PiTensorProduct.map and the result is wanted coefficientwise.
• Matrix.piTensorProductMap_bivector: the same for a whole bivector ∑ x y, K x y • ⨂ₜ, which becomes the bivector of the congruate A * K * Aᵀ. A may be rectangular, so the result is indexed by its row type.

theorem TauCeti.sum_pi_fin_two {ι : Type u_1} {M : Type u_2} [Fintype ι] [AddCommMonoid M] (f : ι → ι → M) : ∑ r : Fin 2 → ι, f (r 0) (r 1) = ∑ p : ι, ∑ q : ι, f p q

A sum over the functions Fin 2 → ι is a double sum.

theorem TauCeti.tprod_fin_two {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (v : Fin 2 → M) : (PiTensorProduct.tprod R) v = (PiTensorProduct.tprod R) ![v 0, v 1]

A pure tensor on two strands, written in ![·, ·] form.

theorem Matrix.piTensorProductMap_tprod_single {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [CommSemiring R] (A : Matrix κ ι R) (x y : ι) : (PiTensorProduct.map fun (x : Fin 2) => A.mulVecLin) ((PiTensorProduct.tprod R) ![Pi.single x 1, Pi.single y 1]) = ∑ p : κ, ∑ q : κ, (A p x * A q y) • (PiTensorProduct.tprod R) ![Pi.single p 1, Pi.single q 1]

Applying a matrix A in both strands re-expands a pure tensor of standard basis vectors back in the standard basis: the coefficient of Pi.single p 1 ⊗ Pi.single q 1 is A p x * A q y.

theorem Matrix.piTensorProductMap_bivector {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [CommSemiring R] (A : Matrix κ ι R) (K : Matrix ι ι R) : (PiTensorProduct.map fun (x : Fin 2) => A.mulVecLin) (∑ x : ι, ∑ y : ι, K x y • (PiTensorProduct.tprod R) ![Pi.single x 1, Pi.single y 1]) = ∑ p : κ, ∑ q : κ, (A * K * A.transpose) p q • (PiTensorProduct.tprod R) ![Pi.single p 1, Pi.single q 1]

Applying a matrix A in both tensor factors turns the bivector of K into the bivector of the congruate A * K * Aᵀ. It is the computation behind the invariance of the Brauer cup.