Symmetric and antisymmetric tensors in a tensor square

The flip x ⊗ y ↦ y ⊗ x is an involution of M ⊗[R] M, and the tensors it fixes and the tensors it negates cut the tensor square into the symmetric tensors TauCeti.symmetricTensors and the antisymmetric tensors TauCeti.antisymmetricTensors. When 2 is invertible they are complementary, so the tensor square is their internal direct sum; the two submodules are the concrete models of Sym²M and ⋀²M inside M ⊗[R] M, which is what a construction carrying extra structure on the tensor square — a topology, say — needs, the quotient and subobject constructions Sym[R]^2 M and ⋀[R]^2 M living outside it. That they really are those two modules, f ⊗ f-equivariantly, is TauCeti.symmetricTensorsEquivSymmetricPower and TauCeti.antisymmetricTensorsEquivExteriorPower in TauCeti/LinearAlgebra/TensorSquare.lean.

The point of the file is the trace identity TauCeti.trace_map_self_comp_comm: composing f ⊗ f with the flip has trace tr (f ∘ f), because on a basis the diagonal entry of the composite at eᵢ ⊗ eⱼ is aᵢⱼ aⱼᵢ, and summing those is Module.Basis.trace_eq_trace_comp_self_of_toMatrix_diag, the step shared with the Fin 2-indexed tensor square of TauCeti/LinearAlgebra/TensorSquare.lean. Splitting that trace along the symmetric and the antisymmetric tensors, where the flip is +1 and -1, gives TauCeti.trace_symmetricTensorsRestrict_sub_trace_antisymmetricTensorsRestrict: the traces of f ⊗ f on the symmetric and on the antisymmetric tensors differ by tr (f ∘ f). That is the character identity χ_{Sym²}(g) - χ_{⋀²}(g) = χ(g²) behind the Frobenius-Schur indicator, read on the tensor square rather than on the symmetric and exterior powers.

Main definitions

• TauCeti.symmetricTensors: the tensors of M ⊗[R] M fixed by the flip.
• TauCeti.antisymmetricTensors: the -1-eigenspace of the flip.

Main results

• TauCeti.add_comm_mem_symmetricTensors and TauCeti.sub_comm_mem_antisymmetricTensors: the symmetrization z + flip z and the antisymmetrization z - flip z of a tensor lie in the two eigenspaces.
• TauCeti.isCompl_symmetricTensors_antisymmetricTensors and TauCeti.isInternal_symmetricTensors_antisymmetricTensors: with 2 invertible the two submodules are complementary, hence an internal direct sum decomposition of the tensor square.
• TauCeti.trace_map_self_comp_comm: tr ((f ⊗ f) ∘ flip) = tr (f ∘ f).
• TauCeti.trace_symmetricTensorsRestrict_sub_trace_antisymmetricTensorsRestrict: the traces of f ⊗ f on the symmetric and on the antisymmetric tensors differ by tr (f ∘ f).

Implementation notes

Neither submodule is a fresh kernel: the symmetric tensors are LinearMap.eqLocus of the flip against the identity and the antisymmetric tensors are Module.End.eigenspace of the flip, so Mathlib's API applies to both unchanged. The membership lemmas below are the only interface the rest of the development uses, and they present the two submodules symmetrically.

The asymmetry between the two constructions is a matter of scalars, and it is deliberate. Module.End.eigenspace subtracts a scalar from an endomorphism, so it is stated over [CommRing R] [AddCommGroup M]; negation is genuinely needed for the antisymmetric tensors — the eigenvalue is -1 — but not for the symmetric ones, and LinearMap.eqLocus asks only for [CommSemiring R] [AddCommMonoid M]. So the symmetric half of the API, up to the restriction of f ⊗ f, is available over a commutative semiring, and only the antisymmetric half and the splitting theorems need a ring. The trace identity uses neither and is stated over [CommSemiring K] [AddCommMonoid M].

def TauCeti.symmetricTensors (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Submodule R (TensorProduct R M M)

The symmetric tensors of M ⊗[R] M: the tensors the flip x ⊗ y ↦ y ⊗ x fixes.

Equations

• TauCeti.symmetricTensors R M = (↑(TensorProduct.comm R M M)).eqLocus LinearMap.id

@[simp]

theorem TauCeti.mem_symmetricTensors {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {x : TensorProduct R M M} : x ∈ symmetricTensors R M ↔ (TensorProduct.comm R M M) x = x

A tensor is symmetric exactly when the flip fixes it.

theorem TauCeti.add_comm_mem_symmetricTensors {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (z : TensorProduct R M M) : z + (TensorProduct.comm R M M) z ∈ symmetricTensors R M

The symmetrization z + flip z of a tensor is symmetric.

theorem TauCeti.map_self_mem_symmetricTensors {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) {x : TensorProduct R M M} (hx : x ∈ symmetricTensors R M) : (TensorProduct.map f f) x ∈ symmetricTensors R M

f ⊗ f preserves the symmetric tensors, because it commutes with the flip.

noncomputable def TauCeti.symmetricTensorsRestrict {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) : ↥(symmetricTensors R M) →ₗ[R] ↥(symmetricTensors R M)

The restriction of f ⊗ f to the symmetric tensors, as an endomorphism.

Equations

• TauCeti.symmetricTensorsRestrict f = (TensorProduct.map f f).restrict ⋯

@[simp]

theorem TauCeti.coe_symmetricTensorsRestrict_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (x : ↥(symmetricTensors R M)) : ↑((symmetricTensorsRestrict f) x) = (TensorProduct.map f f) ↑x

def TauCeti.antisymmetricTensors (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : Submodule R (TensorProduct R M M)

The antisymmetric tensors of M ⊗[R] M: the -1-eigenspace of the flip.

Equations

• TauCeti.antisymmetricTensors R M = Module.End.eigenspace (↑(TensorProduct.comm R M M)) (-1)

@[simp]

theorem TauCeti.mem_antisymmetricTensors {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : TensorProduct R M M} : x ∈ antisymmetricTensors R M ↔ (TensorProduct.comm R M M) x = -x

A tensor is antisymmetric exactly when the flip negates it.

theorem TauCeti.sub_comm_mem_antisymmetricTensors {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (z : TensorProduct R M M) : z - (TensorProduct.comm R M M) z ∈ antisymmetricTensors R M

The antisymmetrization z - flip z of a tensor is antisymmetric.

theorem TauCeti.map_self_mem_antisymmetricTensors {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) {x : TensorProduct R M M} (hx : x ∈ antisymmetricTensors R M) : (TensorProduct.map f f) x ∈ antisymmetricTensors R M

f ⊗ f preserves the antisymmetric tensors, because it commutes with the flip.

noncomputable def TauCeti.antisymmetricTensorsRestrict {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) : ↥(antisymmetricTensors R M) →ₗ[R] ↥(antisymmetricTensors R M)

The restriction of f ⊗ f to the antisymmetric tensors, as an endomorphism.

Equations

• TauCeti.antisymmetricTensorsRestrict f = (TensorProduct.map f f).restrict ⋯

@[simp]

theorem TauCeti.coe_antisymmetricTensorsRestrict_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (x : ↥(antisymmetricTensors R M)) : ↑((antisymmetricTensorsRestrict f) x) = (TensorProduct.map f f) ↑x

theorem TauCeti.isCompl_symmetricTensors_antisymmetricTensors (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] : IsCompl (symmetricTensors R M) (antisymmetricTensors R M)

The tensor square is the sum of its symmetric and antisymmetric parts, when 2 is invertible: a tensor is the sum of ½ (x + flip x) and ½ (x - flip x), and a tensor both symmetric and antisymmetric is its own negative.

theorem TauCeti.isInternal_symmetricTensors_antisymmetricTensors (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] : DirectSum.IsInternal fun (b : Bool) => bif b then symmetricTensors R M else antisymmetricTensors R M

The symmetric and antisymmetric tensors decompose the tensor square as an internal direct sum, the form in which traces split along them.

theorem TauCeti.trace_map_self_comp_comm {K : Type u_1} {M : Type u_2} [CommSemiring K] [AddCommMonoid M] [Module K M] [Module.Free K M] [Module.Finite K M] (f : M →ₗ[K] M) : (LinearMap.trace K (TensorProduct K M M)) (TensorProduct.map f f ∘ₗ ↑(TensorProduct.comm K M M)) = (LinearMap.trace K M) (f ∘ₗ f)

The trace of f ⊗ f composed with the flip is the trace of f ∘ f. In a basis the diagonal entry of the composite at eᵢ ⊗ eⱼ is aᵢⱼ aⱼᵢ, and summing those over all pairs is the trace of the square of the matrix of f, which is Module.Basis.trace_eq_trace_comp_self_of_toMatrix_diag.

theorem TauCeti.trace_symmetricTensorsRestrict_sub_trace_antisymmetricTensorsRestrict {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] [Invertible 2] (f : M →ₗ[K] M) : (LinearMap.trace K ↥(symmetricTensors K M)) (symmetricTensorsRestrict f) - (LinearMap.trace K ↥(antisymmetricTensors K M)) (antisymmetricTensorsRestrict f) = (LinearMap.trace K M) (f ∘ₗ f)

The traces of f ⊗ f on the symmetric and on the antisymmetric tensors differ by tr (f ∘ f). Both traces are read off the same splitting of M ⊗ M: composing f ⊗ f with the flip leaves it unchanged on the symmetric part and negates it on the antisymmetric part, so the trace of that composite — which is tr (f ∘ f) — is the difference of the two.