Regrouping tensor products over a dependent sum

A tensor product of a family of modules indexed by a finite disjoint union can be regrouped as an outer tensor product whose factors are the tensor products over the individual fibres. The fibres themselves need not be finite, and the modules may vary over the dependent sum. The constant case is PiTensorProduct.prodEquiv, which is derived from this equivalence.

The equivalence is characterized on tensors of pure tensors, and is compatible with factorwise linear maps. Its first application is the double-coset decomposition of tensor induction, where the outer indices are double cosets and the fibre over a representative s is K ⧸ (K ⊓ sHs⁻¹).

noncomputable def PiTensorProduct.sigmaEquiv {R : Type u} [CommSemiring R] {ι : Type w} {κ : ι → Type x} {M : (i : ι) → κ i → Type v} [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [Finite ι] : (PiTensorProduct R fun (i : ι) => PiTensorProduct R fun (j : κ i) => M i j) ≃ₗ[R] PiTensorProduct R fun (p : (i : ι) × κ i) => M p.fst p.snd

Regroup a tensor product indexed by a dependent sum into the tensor product of the tensor products over its fibres. Only the outer index must be finite.

@[simp]

theorem PiTensorProduct.sigmaEquiv_tprod {R : Type u} [CommSemiring R] {ι : Type w} {κ : ι → Type x} {M : (i : ι) → κ i → Type v} [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [Finite ι] (m : (i : ι) → (j : κ i) → M i j) : sigmaEquiv ((tprod R) fun (i : ι) => (tprod R) (m i)) = (tprod R) fun (p : (i : ι) × κ i) => m p.fst p.snd

Flattening a tensor of fibrewise pure tensors produces the corresponding pure tensor on the dependent sum.

@[simp]

theorem PiTensorProduct.sigmaEquiv_symm_tprod {R : Type u} [CommSemiring R] {ι : Type w} {κ : ι → Type x} {M : (i : ι) → κ i → Type v} [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [Finite ι] (m : (p : (i : ι) × κ i) → M p.fst p.snd) : sigmaEquiv.symm ((tprod R) m) = (tprod R) fun (i : ι) => (tprod R) fun (j : κ i) => m ⟨i, j⟩

The inverse Sigma regrouping forms one inner pure tensor in each outer coordinate.

theorem PiTensorProduct.ext_sigma_tprod {R : Type u} [CommSemiring R] {ι : Type w} {κ : ι → Type x} {M : (i : ι) → κ i → Type v} [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [Finite ι] {N : Type u_1} [AddCommMonoid N] [Module R N] {f g : (PiTensorProduct R fun (i : ι) => PiTensorProduct R fun (j : κ i) => M i j) →ₗ[R] N} (h : ∀ (m : (i : ι) → (j : κ i) → M i j), f ((tprod R) fun (i : ι) => (tprod R) (m i)) = g ((tprod R) fun (i : ι) => (tprod R) (m i))) : f = g

Linear maps from an iterated tensor product with finite outer index are determined on tensors of fibrewise pure tensors.

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

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