Basic operations on tensor powers

Mathlib's TensorPower.mulEquiv identifies ⨂[R]^k M ⊗[R] ⨂[R]^m M with ⨂[R]^(k + m) M. This file records the inverse operation: TensorPower.splitAt cuts a tensor power of length n after its first k factors, landing in ⨂[R]^k M ⊗[R] ⨂[R]^(n - k) M, together with its value on pure tensors and the fact that it is injective. It also identifies the first tensor power with the underlying module.

Main definitions

• TensorPower.splitAt: split a tensor power at a specified position.
• TauCeti.TensorPower.oneEquiv: identify the first tensor power with the underlying module.

noncomputable def TauCeti.TensorPower.oneEquiv (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorPower R 1 M ≃ₗ[R] M

A tensor word of length one is a single letter.

Equations

• TauCeti.TensorPower.oneEquiv R M = PiTensorProduct.subsingletonEquiv 0

@[simp]

theorem TauCeti.TensorPower.oneEquiv_tprod (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Fin 1 → M) : (oneEquiv R M) ((PiTensorProduct.tprod R) f) = f 0

The length-one tensor-power equivalence evaluates a pure tensor at its unique index.

@[simp]

theorem TauCeti.TensorPower.oneEquiv_symm_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) : (oneEquiv R M).symm a = (PiTensorProduct.tprod R) fun (x : Fin 1) => a

The inverse length-one tensor-power equivalence sends a letter to the corresponding pure tensor.

noncomputable def TensorPower.splitAt (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n k : ℕ) (hk : k ≤ n) : TensorPower R n M →ₗ[R] TensorProduct R (TensorPower R k M) (TensorPower R (n - k) M)

Split a tensor power after its first k factors.

Equations

• TensorPower.splitAt R M n k hk = ↑TensorPower.mulEquiv.symm ∘ₗ ↑(TensorPower.cast R M ⋯)

@[simp]

theorem TensorPower.mulEquiv_splitAt (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n k : ℕ) (hk : k ≤ n) (x : TensorPower R n M) : mulEquiv ((splitAt R M n k hk) x) = (cast R M ⋯) x

theorem TensorPower.splitAt_injective (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n k : ℕ) (hk : k ≤ n) : Function.Injective ⇑(splitAt R M n k hk)

Splitting a tensor power at a fixed position loses no information: it is the composite of two linear equivalences.

@[simp]

theorem TensorPower.splitAt_tprod (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n k : ℕ) (hk : k ≤ n) (x : Fin n → M) : (splitAt R M n k hk) ((PiTensorProduct.tprod R) x) = ((PiTensorProduct.tprod R) fun (i : Fin k) => x (Fin.castLE hk i)) ⊗ₜ[R] (PiTensorProduct.tprod R) fun (j : Fin (n - k)) => x ⟨k + ↑j, ⋯⟩

Splitting a pure tensor separates its first k entries from the remaining entries.

theorem TensorPower.lid_map_algebraMap₀_symm (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (z : TensorProduct R (TensorPower R 0 M) (TensorPower R n M)) : (TensorProduct.lid R (TensorPower R n M)) ((TensorProduct.map (↑algebraMap₀.symm) LinearMap.id) z) = (cast R M ⋯) (mulEquiv z)

Identifying the empty left tensor block with scalars agrees with concatenation.

theorem TensorPower.rid_map_algebraMap₀_symm (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (z : TensorProduct R (TensorPower R n M) (TensorPower R 0 M)) : (TensorProduct.rid R (TensorPower R n M)) ((TensorProduct.map LinearMap.id ↑algebraMap₀.symm) z) = (cast R M ⋯) (mulEquiv z)

Identifying the empty right tensor block with scalars agrees with concatenation.

theorem TensorPower.mulEquiv_symm_assoc (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (p q r : ℕ) (x : TensorPower R (p + q + r) M) : (TensorProduct.assoc R (TensorPower R p M) (TensorPower R q M) (TensorPower R r M)) ((TensorProduct.map (↑mulEquiv.symm) LinearMap.id) (mulEquiv.symm x)) = (TensorProduct.map LinearMap.id ↑mulEquiv.symm) (mulEquiv.symm ((cast R M ⋯) x))

Splitting a tensor power into three consecutive blocks is independent of the order of the two cuts, after applying the tensor associator.