Regrouping finite tensor powers

An iterated tensor power with finite outer index can be flattened to the tensor power indexed by the product of the two index types. The characteristic equation on tensors of pure tensors fixes this equivalence and makes it compatible with factorwise linear maps.

This regrouping is used for transitivity of tensor induction. It is the constant-fibre case of the dependent-sum regrouping PiTensorProduct.sigmaEquiv, transported along Equiv.sigmaEquivProd. Finiteness of the outer index permits expansion of tensors of sums in the inner tensor powers; the inner index need not be finite.

noncomputable def PiTensorProduct.prodEquiv {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {ι : Type w} {κ : Type x} [Finite ι] : (PiTensorProduct R fun (x : ι) => PiTensorProduct R fun (x : κ) => M) ≃ₗ[R] PiTensorProduct R fun (x : ι × κ) => M

Flatten an iterated tensor power along a finite outer index to the tensor power indexed by the product. The inner index can be arbitrary.

theorem PiTensorProduct.prodEquiv_def {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {ι : Type w} {κ : Type x} [Finite ι] : prodEquiv = sigmaEquiv ≪≫ₗ reindex R (fun (x : (_ : ι) × κ) => M) (Equiv.sigmaEquivProd ι κ)

Product regrouping is dependent-sum regrouping followed by reindexing.

@[simp]

theorem PiTensorProduct.prodEquiv_tprod {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {ι : Type w} {κ : Type x} [Finite ι] (m : ι → κ → M) : prodEquiv ((tprod R) fun (i : ι) => (tprod R) (m i)) = (tprod R) fun (p : ι × κ) => m p.1 p.2

Flattening a tensor of pure tensors concatenates the two index coordinates.

@[simp]

theorem PiTensorProduct.prodEquiv_symm_tprod {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {ι : Type w} {κ : Type x} [Finite ι] (m : ι × κ → M) : prodEquiv.symm ((tprod R) m) = (tprod R) fun (i : ι) => (tprod R) fun (j : κ) => m (i, j)

The inverse regrouping forms the inner tensor in each outer coordinate.

theorem PiTensorProduct.prodEquiv_map {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {ι : Type w} {κ : Type x} [Finite ι] {N : Type u_1} [AddCommMonoid N] [Module R N] (f : ι → κ → M →ₗ[R] N) (z : PiTensorProduct R fun (x : ι) => PiTensorProduct R fun (x : κ) => M) : prodEquiv ((map fun (i : ι) => map (f i)) z) = (map fun (p : ι × κ) => f p.1 p.2) (prodEquiv z)

Flattening commutes with applying a chosen linear map in each tensor factor.

A scalar-valued evaluator computes the four entries of a reshaped tensor.