Algebra equivalences for indexed tensor products

The linear equivalences for reindexing, removing an empty index set, and splitting off one factor preserve the algebra structures on indexed tensor products. Their algebra versions allow algebraic properties stable under binary tensor products to be proved by induction on a finite index type.

These constructions upgrade Mathlib's PiTensorProduct.reindex and PiTensorProduct.isEmptyEquiv, and PiTensorProduct.optionEquiv. Reindexing along permutations gives the action of Equiv.Perm ι on a tensor power by algebra automorphisms (PiTensorProduct.permAlgEquiv).

For finite index types, the tensor product of the split algebras κ i → R is the split algebra of functions on Π i, κ i (PiTensorProduct.piScalarAlgEquiv), built from Mathlib's PiTensorProduct.ofFinsuppEquiv'. On a tensor power of κ → R, permuting the factors becomes precomposition on functions on ι → κ.

noncomputable def PiTensorProduct.reindexAlgEquiv {R : Type u_1} [CommSemiring R] {ι : Type u_2} {κ : Type u_3} (A : ι → Type u_4) [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] (e : ι ≃ κ) : (PiTensorProduct R fun (i : ι) => A i) ≃ₐ[R] PiTensorProduct R fun (j : κ) => A (e.symm j)

Reindexing an indexed tensor product of algebras as an algebra equivalence.

@[simp]

theorem PiTensorProduct.reindexAlgEquiv_toLinearEquiv {R : Type u_1} [CommSemiring R] {ι : Type u_2} {κ : Type u_3} (A : ι → Type u_4) [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] (e : ι ≃ κ) : ↑(reindexAlgEquiv A e) = reindex R A e

The underlying linear equivalence of algebra reindexing is tensor reindexing.

@[simp]

theorem PiTensorProduct.reindexAlgEquiv_tprod {R : Type u_1} [CommSemiring R] {ι : Type u_2} {κ : Type u_3} (A : ι → Type u_4) [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] (e : ι ≃ κ) (a : (i : ι) → A i) : (reindexAlgEquiv A e) ((tprod R) a) = (tprod R) fun (j : κ) => a (e.symm j)

Reindexing preserves the labels of the entries of a pure tensor.

@[simp]

theorem PiTensorProduct.reindexAlgEquiv_symm_tprod {R : Type u_1} [CommSemiring R] {ι : Type u_2} {κ : Type u_3} (A : ι → Type u_4) [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] (e : ι ≃ κ) (a : (i : ι) → A i) : (reindexAlgEquiv A e).symm ((tprod R) fun (j : κ) => a (e.symm j)) = (tprod R) a

Reattaching the original index labels recovers the original pure tensor.

@[simp]

theorem PiTensorProduct.reindexAlgEquiv_singleAlgHom {R : Type u_1} [CommSemiring R] {ι : Type u_2} {κ : Type u_3} [DecidableEq ι] [DecidableEq κ] {A : Type u_4} [Semiring A] [Algebra R A] (e : ι ≃ κ) (i : ι) (a : A) : (reindexAlgEquiv (fun (x : ι) => A) e) ((singleAlgHom i) a) = (singleAlgHom (e i)) a

Reindexing along e moves the factor inclusion at i to the factor inclusion at e i. It is a pre-simp lemma since singleAlgHom_apply would otherwise rewrite the factor inclusion first.

noncomputable def PiTensorProduct.permAlgEquiv {R : Type u_1} [CommSemiring R] {ι : Type u_2} (A : Type u_3) [Semiring A] [Algebra R A] : Equiv.Perm ι →* (PiTensorProduct R fun (x : ι) => A) ≃ₐ[R] PiTensorProduct R fun (x : ι) => A

The permutations of ι act on the tensor power ⨂[R] _ : ι, A by algebra automorphisms: σ moves the factor in slot i to slot σ i. This is PiTensorProduct.reindexAlgEquiv along σ, made multiplicative in σ.

@[simp]

theorem PiTensorProduct.permAlgEquiv_toLinearEquiv {R : Type u_1} [CommSemiring R] {ι : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (σ : Equiv.Perm ι) : ↑((permAlgEquiv A) σ) = reindex R (fun (x : ι) => A) σ

The underlying linear equivalence of a permutation of the factors is tensor reindexing.

@[simp]

theorem PiTensorProduct.permAlgEquiv_tprod {R : Type u_1} [CommSemiring R] {ι : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] (σ : Equiv.Perm ι) (x : ι → A) : ((permAlgEquiv A) σ) ((tprod R) x) = (tprod R) (x ∘ ⇑(Equiv.symm σ))

A permutation σ sends the pure tensor ⨂ₜ xᵢ to the pure tensor with x (σ⁻¹ j) in slot j.

@[simp]

theorem PiTensorProduct.permAlgEquiv_singleAlgHom {R : Type u_1} [CommSemiring R] {ι : Type u_2} {A : Type u_3} [Semiring A] [Algebra R A] [DecidableEq ι] (σ : Equiv.Perm ι) (i : ι) (a : A) : ((permAlgEquiv A) σ) ((singleAlgHom i) a) = (singleAlgHom (σ i)) a

A permutation σ moves the factor inclusion at i to the factor inclusion at σ i.

noncomputable def PiTensorProduct.isEmptyAlgEquiv {R : Type u_1} [CommSemiring R] (ι : Type u_2) [IsEmpty ι] (A : ι → Type u_3) [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] : (PiTensorProduct R fun (i : ι) => A i) ≃ₐ[R] R

The tensor product over an empty family of algebras is the base algebra.

@[simp]

theorem PiTensorProduct.isEmptyAlgEquiv_toLinearEquiv {R : Type u_1} [CommSemiring R] (ι : Type u_2) [IsEmpty ι] (A : ι → Type u_3) [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] : ↑(isEmptyAlgEquiv ι A) = isEmptyEquiv ι

The empty-family algebra equivalence has the usual empty-family linear equivalence.

@[simp]

theorem PiTensorProduct.isEmptyAlgEquiv_tprod {R : Type u_1} [CommSemiring R] (ι : Type u_2) [IsEmpty ι] (A : ι → Type u_3) [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] (a : (i : ι) → A i) : (isEmptyAlgEquiv ι A) ((tprod R) a) = 1

An empty pure tensor is the multiplicative unit.

@[simp]

theorem PiTensorProduct.isEmptyAlgEquiv_symm_apply {R : Type u_1} [CommSemiring R] (ι : Type u_2) [IsEmpty ι] (A : ι → Type u_3) [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] (r : R) : (isEmptyAlgEquiv ι A).symm r = r • 1

The inverse empty-family equivalence sends a scalar to that scalar times the empty tensor.

noncomputable def PiTensorProduct.optionAlgEquiv {R : Type u_1} [CommSemiring R] {ι : Type u_2} (A : Option ι → Type u_3) [(i : Option ι) → Semiring (A i)] [(i : Option ι) → Algebra R (A i)] : (PiTensorProduct R fun (i : Option ι) => A i) ≃ₐ[R] TensorProduct R (PiTensorProduct R fun (i : ι) => A (some i)) (A none)

Splitting off the factor at none of an indexed tensor product of algebras.

@[simp]

theorem PiTensorProduct.optionAlgEquiv_toLinearEquiv {R : Type u_1} [CommSemiring R] {ι : Type u_2} (A : Option ι → Type u_3) [(i : Option ι) → Semiring (A i)] [(i : Option ι) → Algebra R (A i)] : ↑(optionAlgEquiv A) = optionEquiv A

The underlying linear equivalence splits off the same factor at none.

@[simp]

theorem PiTensorProduct.optionAlgEquiv_tprod {R : Type u_1} [CommSemiring R] {ι : Type u_2} (A : Option ι → Type u_3) [(i : Option ι) → Semiring (A i)] [(i : Option ι) → Algebra R (A i)] (a : (i : Option ι) → A i) : (optionAlgEquiv A) ((tprod R) a) = ((tprod R) fun (i : ι) => a (some i)) ⊗ₜ[R] a none

Splitting off a factor of a pure tensor separates the some entries from the none entry.

@[simp]

theorem PiTensorProduct.optionAlgEquiv_symm_tmul {R : Type u_1} [CommSemiring R] {ι : Type u_2} (A : Option ι → Type u_3) [(i : Option ι) → Semiring (A i)] [(i : Option ι) → Algebra R (A i)] (a : (i : Option ι) → A i) : (optionAlgEquiv A).symm (((tprod R) fun (i : ι) => a (some i)) ⊗ₜ[R] a none) = (tprod R) a

Reattaching the separated factor recovers the original pure tensor.

noncomputable def PiTensorProduct.piScalarAlgEquiv (R : Type u_1) [CommSemiring R] {ι : Type u_2} [Fintype ι] (κ : ι → Type u_3) [∀ (i : ι), Finite (κ i)] : (PiTensorProduct R fun (i : ι) => κ i → R) ≃ₐ[R] ((i : ι) → κ i) → R

For finite index types, the tensor product of the function algebras κ i → R is the algebra of functions on the product Π i, κ i: the pure tensor ⨂ₜ fᵢ is the function p ↦ ∏ i, fᵢ (p i). In particular, a tensor power of a split algebra κ → R is split.

@[simp]

theorem PiTensorProduct.piScalarAlgEquiv_tprod {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] {κ : ι → Type u_3} [∀ (i : ι), Finite (κ i)] (f : (i : ι) → κ i → R) : (piScalarAlgEquiv R κ) ((tprod R) f) = fun (p : (i : ι) → κ i) => ∏ i : ι, f i (p i)

PiTensorProduct.piScalarAlgEquiv sends ⨂ₜ fᵢ to p ↦ ∏ i, fᵢ (p i).

@[simp]

theorem PiTensorProduct.piScalarAlgEquiv_singleAlgHom {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] {κ : ι → Type u_3} [∀ (i : ι), Finite (κ i)] [DecidableEq ι] (i : ι) (f : κ i → R) : (piScalarAlgEquiv R κ) ((singleAlgHom i) f) = fun (p : (i : ι) → κ i) => f (p i)

PiTensorProduct.piScalarAlgEquiv sends the function f placed in slot i to p ↦ f (p i). It is a pre-simp lemma since singleAlgHom_apply would otherwise rewrite the factor inclusion first.

theorem PiTensorProduct.piScalarAlgEquiv_permAlgEquiv {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] {κ : Type u_4} [Finite κ] (σ : Equiv.Perm ι) (x : PiTensorProduct R fun (x : ι) => κ → R) : (piScalarAlgEquiv R fun (x : ι) => κ) (((permAlgEquiv (κ → R)) σ) x) = fun (p : ι → κ) => (piScalarAlgEquiv R fun (x : ι) => κ) x (p ∘ ⇑σ)

Permuting the tensor factors of a tensor power of a function algebra by σ becomes precomposition with σ on functions on ι → κ.