Tensor-product contractions and trace identities

This file defines contraction of a tensor product against a linear functional on its right factor, and records its behavior on pure tensors and under tensor-product maps. Such contractions extract coordinates and test tensor identities, supporting componentwise arguments about coactions and weight spaces. It also proves the tensor identity that makes the Casimir element of a trace commute with multiplication.

Main declarations

• LinearMap.tensorComponent: contraction against the right factor of a tensor product.
• LinearMap.tensorComponent_map: naturality of contraction under TensorProduct.map.
• LinearMap.tensorComponent_assoc_symm: contraction commutes with reassociation.
• LinearMap.comp_tensorComponent: contraction commutes with a functional on the left.
• TauCeti.tensorProduct_rid_rTensor_apply: naturality of the right tensor unitor.
• LinearMap.sum_mul_tmul_eq_sum_tmul_mul: the Casimir element of a trace commutes with multiplication.

References

• L. Kadison, New examples of Frobenius extensions, University Lecture Series 14, AMS, 1999 (dual bases of Frobenius algebras and extensions, and their Casimir elements).

noncomputable def LinearMap.tensorComponent {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (phi : N →ₗ[R] R) : TensorProduct R M N →ₗ[R] M

Apply a linear functional to the right factor of a tensor.

Equations

• phi.tensorComponent = ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M phi

theorem LinearMap.tensorComponent_def {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (phi : N →ₗ[R] R) : phi.tensorComponent = ↑(TensorProduct.rid R M) ∘ₗ lTensor M phi

Contraction is the tensor product of the functional with the identity, followed by the right tensor unitor.

@[simp]

theorem LinearMap.tensorComponent_tmul {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (phi : N →ₗ[R] R) (m : M) (n : N) : phi.tensorComponent (m ⊗ₜ[R] n) = phi n • m

A right tensor component sends a pure tensor to the corresponding scalar multiple.

@[simp]

theorem LinearMap.tensorComponent_map {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {M' : Type x} {N' : Type y} [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N'] (phi : N' →ₗ[R] R) (f : M →ₗ[R] M') (g : N →ₗ[R] N') (t : TensorProduct R M N) : phi.tensorComponent ((TensorProduct.map f g) t) = f ((phi ∘ₗ g).tensorComponent t)

Taking a right tensor component commutes with a map on both tensor factors.

@[simp]

theorem LinearMap.tensorComponent_zero {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : tensorComponent 0 = 0

Contraction by the zero functional is the zero linear map.

@[simp]

theorem LinearMap.tensorComponent_assoc_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (phi : P →ₗ[R] R) (u : TensorProduct R M (TensorProduct R N P)) : phi.tensorComponent ((TensorProduct.assoc R M N P).symm u) = (lTensor M phi.tensorComponent) u

Contraction of the last tensor factor commutes with reassociation.

theorem LinearMap.comp_tensorComponent {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (psi : M →ₗ[R] R) (phi : N →ₗ[R] R) : psi ∘ₗ phi.tensorComponent = phi ∘ₗ ↑(TensorProduct.lid R N) ∘ₗ rTensor N psi

Applying functionals to both factors is independent of the order of contraction.

The Casimir element of a trace

Let φ : A →ₗ[k] k be a trace on a k-algebra A, so φ (a * b) = φ (b * a), and let x and y be finite families dual to each other for the pairing (a, b) ↦ φ (a * b), in the sense that every element expands in either family with coefficients read off by pairing against the other:

a = ∑ i, φ (a * y i) • x i,        a = ∑ i, φ (x i * a) • y i.

For a finite free symmetric Frobenius algebra, a basis and its dual basis give such families; the expansion identities also allow redundant families. The Casimir element ∑ i, x i ⊗ y i of A ⊗[k] A then commutes with A in the bimodule sense:

∑ i, (a * x i) ⊗ y i = ∑ i, x i ⊗ (y i * a).

This is what makes 1 ↦ ∑ i, x i ⊗ y i a map of A-bimodules A → A ⊗[k] A, the coevaluation of a symmetric Frobenius algebra; for a Frobenius coalgebra in Mathlib's sense (Coalgebra.IsFrobenius) with counit φ, the element is the comultiplication of 1.

The tensor identity itself needs only a k-module A with an associative multiplication. No multiplicative identity, distributivity, or compatibility with scalar multiplication is needed.

theorem LinearMap.sum_mul_tmul_eq_sum_tmul_mul {k : Type u_1} {A : Type u_2} [CommSemiring k] [AddCommMonoid A] [Semigroup A] [Module k A] {ι : Type u_3} [Fintype ι] (φ : A →ₗ[k] k) (hφ : ∀ (a b : A), φ (a * b) = φ (b * a)) {x y : ι → A} (hx : ∀ (a : A), ∑ i : ι, φ (a * y i) • x i = a) (hy : ∀ (a : A), ∑ i : ι, φ (x i * a) • y i = a) (a : A) : ∑ i : ι, (a * x i) ⊗ₜ[k] y i = ∑ i : ι, x i ⊗ₜ[k] (y i * a)

The Casimir element of a trace commutes with multiplication. If φ is a trace on A and the finite families x and y are dual for (a, b) ↦ φ (a * b), then ∑ i, (a * x i) ⊗ y i = ∑ i, x i ⊗ (y i * a) for every a : A.

@[simp]

theorem TauCeti.tensorProduct_rid_rTensor_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (t : TensorProduct R M R) : (TensorProduct.rid R N) ((LinearMap.rTensor R f) t) = f ((TensorProduct.rid R M) t)

The right tensor unitor is natural with respect to a linear map in its left factor.