Decomposing a tensor square

When 2 is invertible, the tensor square of a module is the direct sum of its symmetric and alternating parts. This file constructs the natural equivalence

⨂[R]^2 M ≃ₗ[R] Sym[R]^2 M × ⋀[R]^2 M

using the half-symmetrizer and half-antisymmetrizer. No freeness or finite-generation hypothesis is needed. Before that splitting, it proves the characteristic-free exactness of ⋀²M → M ⊗ M → Sym²M and the resulting trace sum and difference identities for finite free modules over any commutative ring.

It then transfers the decomposition to the binary tensor square M ⊗[R] M, where the two summands are the eigenspaces TauCeti.symmetricTensors and TauCeti.antisymmetricTensors of the flip x ⊗ₜ y ↦ y ⊗ₜ x. The bridge is TauCeti.tensorProductEquivTensorSquare : M ⊗[R] M ≃ₗ[R] ⨂[R]^2 M, which carries the flip to TauCeti.tensorSwap; the two embeddings above have images the +1- and -1-eigenspaces, so the eigenspaces are Sym[R]^2 M and ⋀[R]^2 M, canonically and f ⊗ f-equivariantly. The eigenspace presentation is the one a topological or analytic development has to use — a submodule of M ⊗[R] M carries a topology where a quotient of a PiTensorProduct carries none — so these comparisons are what let a statement proved there be read as a statement about Sym² and ⋀².

Main definitions

• TauCeti.tensorSwap exchanges the two factors of a tensor square; it needs no hypothesis on 2, and is what the two orders on a tensor square are compared by.
• TauCeti.tensorProductEquivTensorSquare identifies the binary tensor square M ⊗[R] M with the second tensor power ⨂[R]^2 M.
• SymmetricPower.toTensorSquare embeds a symmetric square by averaging the two orders.
• exteriorPower.toTensorSquare embeds an exterior square by alternating the two orders.
• TauCeti.tensorSquareEquivSymmetricExterior is the resulting direct-sum decomposition.
• TauCeti.symmetricTensorsEquivSymmetricPower and TauCeti.antisymmetricTensorsEquivExteriorPower identify the two flip eigenspaces of M ⊗[R] M with Sym[R]^2 M and ⋀[R]^2 M.

Main results

• exteriorPower.range_toTensorPower_two_eq_ker_symmetricPower_mk: antisymmetrization and the symmetric quotient are exact without an assumption on 2.
• exteriorPower.exact_toTensorPower_two_symmetricPower_mk: the same exactness in the Function.Exact API.
• LinearMap.trace_piTensorProduct_map_two and LinearMap.trace_symmetricPower_sub_trace_exteriorPower: the trace sum and difference identities on the symmetric and exterior squares of a finite free module over a commutative ring, valid in every characteristic.
• LinearMap.trace_piTensorProduct_map_comp_tensorSwap: the trace of the diagonal action composed with the swap is the trace of the square of the endomorphism.
• TauCeti.tensorProductEquivTensorSquare_comm and TauCeti.tensorProductEquivTensorSquare_comp_map: the bridge carries the flip to the swap and f ⊗ f to the diagonal PiTensorProduct.map.
• SymmetricPower.toTensorSquare_comp_mk and exteriorPower.toTensorSquare_comp_lift_ιMulti: the two embeddings compose with their projections to the symmetrizer ⅟2 • (1 + swap) and the antisymmetrizer ⅟2 • (1 - swap).
• TauCeti.symmetricTensorsEquivSymmetricPower_symmetricTensorsRestrict and TauCeti.antisymmetricTensorsEquivExteriorPower_antisymmetricTensorsRestrict: both comparisons turn the restriction of f ⊗ f into SymmetricPower.map f and exteriorPower.map 2 f.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Lecture 6.
• Mathlib's SymmetricPower quotient API, by Kenny Lau.
• Mathlib's exteriorPower universal-property API, by Sophie Morel and Joël Riou.

noncomputable def TauCeti.tensorSwap (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorPower R 2 M ≃ₗ[R] TensorPower R 2 M

The swap of the two factors of a tensor square, x ⊗ₜ y ↦ y ⊗ₜ x.

Equations

• TauCeti.tensorSwap R M = PiTensorProduct.reindex R (fun (x : Fin 2) => M) (Equiv.swap 0 1)

@[simp]

theorem TauCeti.tensorSwap_tprod (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Fin 2 → M) : (tensorSwap R M) ((PiTensorProduct.tprod R) f) = (PiTensorProduct.tprod R) fun (i : Fin 2) => f ((Equiv.swap 0 1) i)

The swap reads a pure tensor in the other order.

@[simp]

theorem TauCeti.tensorSwap_symm (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] : (tensorSwap R M).symm = tensorSwap R M

The swap is its own inverse.

@[simp]

theorem TauCeti.tensorSwap_tensorSwap (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : TensorPower R 2 M) : (tensorSwap R M) ((tensorSwap R M) x) = x

Swapping the two factors of an arbitrary tensor twice is the identity.

noncomputable def TauCeti.tensorProductEquivTensorSquare (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorProduct R M M ≃ₗ[R] TensorPower R 2 M

The second tensor power is the binary tensor square: both are the universal target of a bilinear map out of M × M, and the equivalence matches x ⊗ₜ y with x ⊗ y. The characterising value is TauCeti.tensorProductEquivTensorSquare_tmul.

Equations

• TauCeti.tensorProductEquivTensorSquare R M = (TensorProduct.congr (PiTensorProduct.subsingletonEquiv 0).symm (PiTensorProduct.subsingletonEquiv 0).symm).trans TensorPower.mulEquiv

@[simp]

theorem TauCeti.tensorProductEquivTensorSquare_tmul (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (x y : M) : (tensorProductEquivTensorSquare R M) (x ⊗ₜ[R] y) = (PiTensorProduct.tprod R) ![x, y]

The comparison with the second tensor power sends x ⊗ₜ y to the pure tensor x ⊗ y.

@[simp]

theorem TauCeti.tensorProductEquivTensorSquare_symm_tprod (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Fin 2 → M) : (tensorProductEquivTensorSquare R M).symm ((PiTensorProduct.tprod R) f) = f 0 ⊗ₜ[R] f 1

The inverse comparison reads a pure tensor as the product of its two entries.

theorem TauCeti.tensorProductEquivTensorSquare_comp_comm (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] : ↑(tensorProductEquivTensorSquare R M) ∘ₗ ↑(TensorProduct.comm R M M) = ↑(tensorSwap R M) ∘ₗ ↑(tensorProductEquivTensorSquare R M)

The comparison turns the flip into the swap: the flip x ⊗ₜ y ↦ y ⊗ₜ x of the binary tensor square is TauCeti.tensorSwap read through TauCeti.tensorProductEquivTensorSquare.

@[simp]

theorem TauCeti.tensorProductEquivTensorSquare_comm (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : TensorProduct R M M) : (tensorProductEquivTensorSquare R M) ((TensorProduct.comm R M M) x) = (tensorSwap R M) ((tensorProductEquivTensorSquare R M) x)

The flip of the binary tensor square agrees with the swap of the second tensor power.

theorem TauCeti.tensorProductEquivTensorSquare_comp_map (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : ↑(tensorProductEquivTensorSquare R N) ∘ₗ TensorProduct.map f f = (PiTensorProduct.map fun (x : Fin 2) => f) ∘ₗ ↑(tensorProductEquivTensorSquare R M)

The comparison is natural in the module: f ⊗ f on the binary tensor square is the diagonal PiTensorProduct.map on the second tensor power.

@[simp]

theorem exteriorPower.toTensorPower_ιMulti_two {R : Type} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (f : Fin 2 → M) : (toTensorPower R M 2) ((ιMulti R 2) f) = (PiTensorProduct.tprod R) f - (PiTensorProduct.tprod R) fun (i : Fin 2) => f ((Equiv.swap 0 1) i)

Antisymmetrizing a pure exterior square is the difference of its two tensor orders.

theorem SymmetricPower.mk_comp_exteriorPower_toTensorPower {R : Type} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] : mk R (Fin 2) M ∘ₗ exteriorPower.toTensorPower R M 2 = 0

The symmetric quotient kills antisymmetrization of an exterior square.

@[simp]

theorem SymmetricPower.mk_exteriorPower_toTensorPower {R : Type} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (x : ↥(⋀[R]^2 M)) : (mk R (Fin 2) M) ((exteriorPower.toTensorPower R M 2) x) = 0

The symmetric quotient kills every antisymmetrized exterior square.

theorem exteriorPower.range_toTensorPower_two_eq_ker_symmetricPower_mk {R : Type} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] : (toTensorPower R M 2).range = (SymmetricPower.mk R (Fin 2) M).ker

Antisymmetrization and the symmetric quotient form the characteristic-free exact sequence ⋀²M → M ⊗ M → Sym²M.

theorem exteriorPower.exact_toTensorPower_two_symmetricPower_mk {R : Type} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] : Function.Exact ⇑(toTensorPower R M 2) ⇑(SymmetricPower.mk R (Fin 2) M)

The antisymmetrization into the tensor square and its symmetric quotient are exact over every commutative ring.

theorem TauCeti.tensorSwap_comp_exteriorPower_toTensorPower {R : Type} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] : ↑(tensorSwap R M) ∘ₗ exteriorPower.toTensorPower R M 2 = -exteriorPower.toTensorPower R M 2

The swap acts as -1 on the alternating part: it exchanges the two pure tensors whose difference is the image of a wedge.

@[simp]

theorem TauCeti.tensorSwap_exteriorPower_toTensorPower {R : Type} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (x : ↥(⋀[R]^2 M)) : (tensorSwap R M) ((exteriorPower.toTensorPower R M 2) x) = -(exteriorPower.toTensorPower R M 2) x

Swapping an antisymmetrized exterior square negates it.

theorem SymmetricPower.mk_comp_tensorSwap {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] : mk R (Fin 2) M ∘ₗ ↑(TauCeti.tensorSwap R M) = mk R (Fin 2) M

The swap acts as +1 on the symmetric part: that is exactly the relation defining Sym².

@[simp]

theorem SymmetricPower.mk_tensorSwap {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : TensorPower R 2 M) : (mk R (Fin 2) M) ((TauCeti.tensorSwap R M) x) = (mk R (Fin 2) M) x

Swapping any tensor square preserves its symmetric class.

theorem LinearMap.trace_piTensorProduct_map_comp_tensorSwap {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) : (trace R (TensorPower R 2 M)) ((PiTensorProduct.map fun (x : Fin 2) => f) ∘ₗ ↑(TauCeti.tensorSwap R M)) = (trace R M) (f ∘ₗ f)

The trace of the diagonal tensor-square map composed with the swap is the trace of the square of the endomorphism.

theorem LinearMap.trace_piTensorProduct_map_two {R : Type} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) : (trace R (TensorPower R 2 M)) (PiTensorProduct.map fun (x : Fin 2) => f) = (trace R (SymmetricPower R (Fin 2) M)) (SymmetricPower.map f) + (trace R ↥(⋀[R]^2 M)) (exteriorPower.map 2 f)

The trace of the diagonal tensor-square map of a finite free module over a commutative ring is the sum of the traces on its symmetric and exterior squares.

theorem LinearMap.trace_symmetricPower_sub_trace_exteriorPower {R : Type} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) : (trace R (SymmetricPower R (Fin 2) M)) (SymmetricPower.map f) - (trace R ↥(⋀[R]^2 M)) (exteriorPower.map 2 f) = (trace R M) (f ∘ₗ f)

The trace form of the two square characters. For a finite free module over a commutative ring, the traces of an endomorphism on the symmetric and exterior squares differ by the trace of its own square.

noncomputable def SymmetricPower.toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : SymmetricPower R (Fin 2) M →ₗ[R] TensorPower R 2 M

The embedding of the symmetric square in the tensor square, given on a pure symmetric tensor by x ⊗ₛ y ↦ ⅟2 • (x ⊗ₜ y + y ⊗ₜ x).

Equations

• SymmetricPower.toTensorSquare R M = { toFun := ⇑((addConGen (SymmetricPower.Rel R (Fin 2) M)).lift (TauCeti.symmetricProjection✝ R M).toAddMonoidHom ⋯), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SymmetricPower.toTensorSquare_tprod (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (f : Fin 2 → M) : (toTensorSquare R M) (⨂ₛ[R] (i : Fin 2), f i) = ⅟2 • ((PiTensorProduct.tprod R) f + (PiTensorProduct.tprod R) fun (i : Fin 2) => f ((Equiv.swap 0 1) i))

The symmetric-square embedding is the half-sum of the two orders on pure tensors.

noncomputable def exteriorPower.toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : ↥(⋀[R]^2 M) →ₗ[R] TensorPower R 2 M

The embedding of the exterior square in the tensor square, given on a pure wedge by x ∧ y ↦ ⅟2 • (x ⊗ₜ y - y ⊗ₜ x).

Equations

• exteriorPower.toTensorSquare R M = ⅟2 • exteriorPower.toTensorPower R M 2

@[simp]

theorem exteriorPower.toTensorSquare_ιMulti (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (f : Fin 2 → M) : (toTensorSquare R M) ((ιMulti R 2) f) = ⅟2 • ((PiTensorProduct.tprod R) f - (PiTensorProduct.tprod R) fun (i : Fin 2) => f ((Equiv.swap 0 1) i))

The exterior-square embedding is the half-difference of the two orders on pure wedges.

theorem SymmetricPower.mk_comp_toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : mk R (Fin 2) M ∘ₗ toTensorSquare R M = LinearMap.id

The symmetric quotient composed with the symmetric-square embedding is the identity.

@[simp]

theorem SymmetricPower.mk_toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x : SymmetricPower R (Fin 2) M) : (mk R (Fin 2) M) ((toTensorSquare R M) x) = x

Projecting the symmetric-square embedding back to the symmetric square is the identity.

theorem SymmetricPower.toTensorSquare_injective (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : Function.Injective ⇑(toTensorSquare R M)

The map from the symmetric square to the tensor square is injective.

theorem exteriorPower.lift_ιMulti_comp_symmetricPower_toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : PiTensorProduct.lift ↑(ιMulti R 2) ∘ₗ SymmetricPower.toTensorSquare R M = 0

The exterior projection vanishes on the symmetric-square embedding.

@[simp]

theorem exteriorPower.lift_ιMulti_symmetricPower_toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x : SymmetricPower R (Fin 2) M) : (PiTensorProduct.lift ↑(ιMulti R 2)) ((SymmetricPower.toTensorSquare R M) x) = 0

The exterior projection of an element embedded from the symmetric square vanishes.

theorem SymmetricPower.mk_comp_exteriorPower_toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : mk R (Fin 2) M ∘ₗ exteriorPower.toTensorSquare R M = 0

The symmetric projection vanishes on the exterior-square embedding.

@[simp]

theorem SymmetricPower.mk_exteriorPower_toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x : ↥(⋀[R]^2 M)) : (mk R (Fin 2) M) ((exteriorPower.toTensorSquare R M) x) = 0

The symmetric projection of an element embedded from the exterior square vanishes.

theorem exteriorPower.lift_ιMulti_comp_toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : PiTensorProduct.lift ↑(ιMulti R 2) ∘ₗ toTensorSquare R M = LinearMap.id

The exterior projection composed with the exterior-square embedding is the identity.

@[simp]

theorem exteriorPower.lift_ιMulti_toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x : ↥(⋀[R]^2 M)) : (PiTensorProduct.lift ↑(ιMulti R 2)) ((toTensorSquare R M) x) = x

Projecting the exterior-square embedding back to the exterior square is the identity.

theorem exteriorPower.toTensorSquare_injective (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : Function.Injective ⇑(toTensorSquare R M)

The map from the exterior square to the tensor square is injective.

noncomputable def TauCeti.tensorSquareEquivSymmetricExterior (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : TensorPower R 2 M ≃ₗ[R] SymmetricPower R (Fin 2) M × ↥(⋀[R]^2 M)

The tensor square is naturally the direct sum of its symmetric and exterior squares when 2 is invertible. The forward map sends a tensor to its symmetric quotient and exterior product.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.tensorSquareEquivSymmetricExterior_tprod (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (f : Fin 2 → M) : (tensorSquareEquivSymmetricExterior R M) ((PiTensorProduct.tprod R) f) = (⨂ₛ[R] (i : Fin 2), f i, (exteriorPower.ιMulti R 2) f)

The tensor-square decomposition sends a pure tensor to its symmetric and exterior classes.

@[simp]

theorem TauCeti.tensorSquareEquivSymmetricExterior_symm_apply (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x : SymmetricPower R (Fin 2) M × ↥(⋀[R]^2 M)) : (tensorSquareEquivSymmetricExterior R M).symm x = (SymmetricPower.toTensorSquare R M) x.1 + (exteriorPower.toTensorSquare R M) x.2

The inverse tensor-square decomposition is the sum of the symmetric and exterior embeddings.

The flip eigenspaces of the binary tensor square

TauCeti.symmetricTensors and TauCeti.antisymmetricTensors are the ±1-eigenspaces of the flip on M ⊗[R] M. Through TauCeti.tensorProductEquivTensorSquare the flip is TauCeti.tensorSwap, whose eigenspaces are the images of the two embeddings SymmetricPower.toTensorSquare and exteriorPower.toTensorSquare; so the two eigenspaces are Sym[R]^2 M and ⋀[R]^2 M, and not merely modules of the same rank.

theorem TauCeti.tensorSwap_comp_symmetricPower_toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : ↑(tensorSwap R M) ∘ₗ SymmetricPower.toTensorSquare R M = SymmetricPower.toTensorSquare R M

The swap fixes the symmetric-square embedding.

theorem TauCeti.tensorSwap_comp_exteriorPower_toTensorSquare (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : ↑(tensorSwap R M) ∘ₗ exteriorPower.toTensorSquare R M = -exteriorPower.toTensorSquare R M

The swap negates the exterior-square embedding.

theorem SymmetricPower.toTensorSquare_comp_mk (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : toTensorSquare R M ∘ₗ mk R (Fin 2) M = ⅟2 • (LinearMap.id + ↑(TauCeti.tensorSwap R M))

The symmetric embedding is the symmetrizer: composing the symmetric quotient with the symmetric-square embedding is ⅟2 • (1 + swap).

theorem exteriorPower.toTensorSquare_comp_lift_ιMulti (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : toTensorSquare R M ∘ₗ PiTensorProduct.lift ↑(ιMulti R 2) = ⅟2 • (LinearMap.id - ↑(TauCeti.tensorSwap R M))

The exterior embedding is the antisymmetrizer: composing the exterior projection with the exterior-square embedding is ⅟2 • (1 - swap).

theorem TauCeti.symmetricPower_toTensorSquare_mk_of_tensorSwap_eq (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] {y : TensorPower R 2 M} (hy : (tensorSwap R M) y = y) : (SymmetricPower.toTensorSquare R M) ((SymmetricPower.mk R (Fin 2) M) y) = y

A swap-invariant tensor is recovered from its symmetric class.

theorem TauCeti.exteriorPower_toTensorSquare_lift_ιMulti_of_tensorSwap_eq_neg (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] {y : TensorPower R 2 M} (hy : (tensorSwap R M) y = -y) : (exteriorPower.toTensorSquare R M) ((PiTensorProduct.lift ↑(exteriorPower.ιMulti R 2)) y) = y

A swap-anti-invariant tensor is recovered from its wedge.

theorem TauCeti.tensorProductEquivTensorSquare_symm_symmetricPower_toTensorSquare_mem_symmetricTensors (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x : SymmetricPower R (Fin 2) M) : (tensorProductEquivTensorSquare R M).symm ((SymmetricPower.toTensorSquare R M) x) ∈ symmetricTensors R M

The symmetric-square embedding lands in the symmetric tensors.

theorem TauCeti.tensorProductEquivTensorSquare_symm_exteriorPower_toTensorSquare_mem_antisymmetricTensors (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x : ↥(⋀[R]^2 M)) : (tensorProductEquivTensorSquare R M).symm ((exteriorPower.toTensorSquare R M) x) ∈ antisymmetricTensors R M

The exterior-square embedding lands in the antisymmetric tensors.

noncomputable def TauCeti.symmetricTensorsEquivSymmetricPower (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : ↥(symmetricTensors R M) ≃ₗ[R] SymmetricPower R (Fin 2) M

The symmetric tensors are the symmetric square. The flip-fixed submodule of M ⊗[R] M is Sym[R]^2 M, by the symmetric quotient read through TauCeti.tensorProductEquivTensorSquare; the inverse is the symmetrizer x ⊗ₛ y ↦ ⅟2 • (x ⊗ₜ y + y ⊗ₜ x). This is what justifies calling TauCeti.symmetricTensors a symmetric square: the two modules are not merely of the same rank, they are canonically the same.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.symmetricTensorsEquivSymmetricPower_apply (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (z : ↥(symmetricTensors R M)) : (symmetricTensorsEquivSymmetricPower R M) z = (SymmetricPower.mk R (Fin 2) M) ((tensorProductEquivTensorSquare R M) ↑z)

The forward map of TauCeti.symmetricTensorsEquivSymmetricPower is the symmetric quotient.

@[simp]

theorem TauCeti.coe_symmetricTensorsEquivSymmetricPower_symm_apply (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x : SymmetricPower R (Fin 2) M) : ↑((symmetricTensorsEquivSymmetricPower R M).symm x) = (tensorProductEquivTensorSquare R M).symm ((SymmetricPower.toTensorSquare R M) x)

The inverse of TauCeti.symmetricTensorsEquivSymmetricPower is the symmetric-square embedding.

theorem TauCeti.coe_symmetricTensorsEquivSymmetricPower_symm_tprod (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x y : M) : ↑((symmetricTensorsEquivSymmetricPower R M).symm (⨂ₛ[R] (i : Fin 2), ![x, y] i)) = ⅟2 • (x ⊗ₜ[R] y + y ⊗ₜ[R] x)

The symmetrizer, explicitly: the symmetric tensor matching x ⊗ₛ y is ⅟2 • (x ⊗ₜ y + y ⊗ₜ x).

theorem TauCeti.symmetricTensorsEquivSymmetricPower_apply_tmul_add_tmul (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x y : M) : (symmetricTensorsEquivSymmetricPower R M) ⟨x ⊗ₜ[R] y + y ⊗ₜ[R] x, ⋯⟩ = 2 • ⨂ₛ[R] (i : Fin (Nat.succ 1)), ![x, y] i

The symmetric quotient, explicitly: the symmetrization of x ⊗ₜ y has symmetric class 2 • (x ⊗ₛ y).

noncomputable def TauCeti.antisymmetricTensorsEquivExteriorPower (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] : ↥(antisymmetricTensors R M) ≃ₗ[R] ↥(⋀[R]^2 M)

The antisymmetric tensors are the exterior square. The -1-eigenspace of the flip on M ⊗[R] M is ⋀[R]^2 M, by the wedge map read through TauCeti.tensorProductEquivTensorSquare; the inverse is the antisymmetrizer x ∧ y ↦ ⅟2 • (x ⊗ₜ y - y ⊗ₜ x).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.antisymmetricTensorsEquivExteriorPower_apply (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (z : ↥(antisymmetricTensors R M)) : (antisymmetricTensorsEquivExteriorPower R M) z = (PiTensorProduct.lift ↑(exteriorPower.ιMulti R 2)) ((tensorProductEquivTensorSquare R M) ↑z)

The forward map of TauCeti.antisymmetricTensorsEquivExteriorPower is the wedge map.

@[simp]

theorem TauCeti.coe_antisymmetricTensorsEquivExteriorPower_symm_apply (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x : ↥(⋀[R]^2 M)) : ↑((antisymmetricTensorsEquivExteriorPower R M).symm x) = (tensorProductEquivTensorSquare R M).symm ((exteriorPower.toTensorSquare R M) x)

The inverse of TauCeti.antisymmetricTensorsEquivExteriorPower is the exterior-square embedding.

theorem TauCeti.coe_antisymmetricTensorsEquivExteriorPower_symm_ιMulti (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x y : M) : ↑((antisymmetricTensorsEquivExteriorPower R M).symm ((exteriorPower.ιMulti R 2) ![x, y])) = ⅟2 • (x ⊗ₜ[R] y - y ⊗ₜ[R] x)

The antisymmetrizer, explicitly: the antisymmetric tensor matching x ∧ y is ⅟2 • (x ⊗ₜ y - y ⊗ₜ x).

theorem TauCeti.antisymmetricTensorsEquivExteriorPower_apply_tmul_sub_tmul (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (x y : M) : (antisymmetricTensorsEquivExteriorPower R M) ⟨x ⊗ₜ[R] y - y ⊗ₜ[R] x, ⋯⟩ = 2 • (exteriorPower.ιMulti R 2) ![x, y]

The wedge map, explicitly: the antisymmetrization of x ⊗ₜ y wedges to 2 • (x ∧ y).

theorem exteriorPower.lift_ιMulti_comp_piTensorProduct_map (R : Type) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : (PiTensorProduct.lift ↑(ιMulti R 2) ∘ₗ PiTensorProduct.map fun (x : Fin 2) => f) = map 2 f ∘ₗ PiTensorProduct.lift ↑(ιMulti R 2)

The wedge map is natural in the module.

theorem TauCeti.symmetricTensorsEquivSymmetricPower_symmetricTensorsRestrict (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (z : ↥(symmetricTensors R M)) : (symmetricTensorsEquivSymmetricPower R M) ((symmetricTensorsRestrict f) z) = (SymmetricPower.map f) ((symmetricTensorsEquivSymmetricPower R M) z)

The symmetric comparison is equivariant: the restriction of f ⊗ f to the symmetric tensors is SymmetricPower.map f. With TauCeti.symmetricTensorsEquivSymmetricPower this is what makes the symmetric tensors a symmetric square of representations, not only of modules.

theorem TauCeti.antisymmetricTensorsEquivExteriorPower_antisymmetricTensorsRestrict (R : Type) (M : Type v) [CommRing R] [Invertible 2] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (z : ↥(antisymmetricTensors R M)) : (antisymmetricTensorsEquivExteriorPower R M) ((antisymmetricTensorsRestrict f) z) = (exteriorPower.map 2 f) ((antisymmetricTensorsEquivExteriorPower R M) z)

The exterior comparison is equivariant: the restriction of f ⊗ f to the antisymmetric tensors is exteriorPower.map 2 f.