Documentation

TauCeti.RepresentationTheory.Tensor.Square

Tensor-square decompositions of representations #

When 2 is invertible, the tensor square of a representation splits into its symmetric and exterior squares. This file lifts the natural linear decomposition to representations. It also proves the two trace identities that this splitting is measured by, over every field, including characteristic two where the decomposition does not split.

The two identities read the same exact sequence ⋀²M → M ⊗ M → Sym²M twice. Reading it against g acting diagonally gives the sum χ(g)² = χ_{Sym²}(g) + χ_{Λ²}(g). Reading it against that same diagonal action composed with the swap of the two tensor factors gives the difference: the swap is -1 on the exterior square and +1 on the symmetric square, while its composite with the diagonal action has trace χ(g²). So χ_{Sym²}(g) - χ_{Λ²}(g) = χ(g²), and adding and subtracting the two identities gives the doubled formulas 2·χ_{Sym²}(g) = χ(g)² + χ(g²) and 2·χ_{Λ²}(g) = χ(g)² - χ(g²). These hold over every field, but they pin down the two characters individually only away from characteristic two: in characteristic two their left sides vanish and the sum and difference identities coincide, so neither character is determined by them.

Main definitions #

Main results #

Implementation notes #

Both trace identities read the exact sequence ⋀²M → M ⊗ M → Sym²M through the same trace additivity LinearMap.trace_eq_add_of_exact, so its hypothesis on the alternating inclusion is named once (TauCeti.TensorSquare.map_comp_toTensorPower) and reused for both readings; the matching hypothesis on the symmetric quotient is SymmetricPower.map_mk read extensionally. The linear-algebra steps stay private, as the file's public interface is the character identities.

References #

source
noncomputable def Representation.tensorSquareEquivSymmetricExterior {R : Type} {G : Type v} {M : Type w} [CommRing R] [Invertible 2] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) :
(ρ.tensorPower 2).Equiv ((ρ.symmetricPower 2).prod (ρ.exteriorPower 2))

The tensor square of a representation is equivalent to the product of its symmetric and exterior squares when 2 is invertible.

Equations
Instances For
    source
    @[simp]
    theorem Representation.tensorSquareEquivSymmetricExterior_toLinearEquiv {R : Type} {G : Type v} {M : Type w} [CommRing R] [Invertible 2] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) :
    ρ.tensorSquareEquivSymmetricExterior.toLinearEquiv = TauCeti.tensorSquareEquivSymmetricExterior R M

    The underlying linear equivalence of the tensor-square decomposition is the natural linear-algebraic decomposition.

    source
    theorem Representation.char_tensorSquare {R : Type} {G : Type v} {M : Type w} [Field R] [Monoid G] [AddCommGroup M] [Module R M] [FiniteDimensional R M] (ρ : Representation R G M) (g : G) :
    ρ.character g ^ 2 = (ρ.symmetricPower 2).character g + (ρ.exteriorPower 2).character g

    Over any field, the tensor-square character is the sum of the symmetric-square and exterior-square characters.

    source
    theorem Representation.char_symmetricSquare_sub_char_exteriorSquare {R : Type} {G : Type v} {M : Type w} [Field R] [Monoid G] [AddCommGroup M] [Module R M] [FiniteDimensional R M] (ρ : Representation R G M) (g : G) :
    (ρ.symmetricPower 2).character g - (ρ.exteriorPower 2).character g = ρ.character (g * g)

    The difference of the two square characters is the character at the square. Over any field, including in characteristic two, χ_{Sym²}(g) - χ_{Λ²}(g) = χ(g²); this is the identity that, together with Representation.char_tensorSquare, gives the doubled formulas for the two characters, which determine them individually away from characteristic two.

    source
    theorem Representation.two_mul_char_symmetricSquare {R : Type} {G : Type v} {M : Type w} [Field R] [Monoid G] [AddCommGroup M] [Module R M] [FiniteDimensional R M] (ρ : Representation R G M) (g : G) :
    2 * (ρ.symmetricPower 2).character g = ρ.character g ^ 2 + ρ.character (g * g)

    The symmetric-square character, without dividing: 2·χ_{Sym²}(g) = χ(g)² + χ(g²).

    source
    theorem Representation.two_mul_char_exteriorSquare {R : Type} {G : Type v} {M : Type w} [Field R] [Monoid G] [AddCommGroup M] [Module R M] [FiniteDimensional R M] (ρ : Representation R G M) (g : G) :
    2 * (ρ.exteriorPower 2).character g = ρ.character g ^ 2 - ρ.character (g * g)

    The exterior-square character, without dividing: 2·χ_{Λ²}(g) = χ(g)² - χ(g²).

    source
    theorem Representation.char_symmetricSquare {R : Type} {G : Type v} {M : Type w} [Field R] [Monoid G] [AddCommGroup M] [Module R M] [FiniteDimensional R M] (ρ : Representation R G M) (g : G) (h2 : 2 ≠ 0) :
    (ρ.symmetricPower 2).character g = (ρ.character g ^ 2 + ρ.character (g * g)) / 2

    The character of the symmetric square, χ_{Sym²}(g) = ½(χ(g)² + χ(g²)), away from characteristic two.

    source
    theorem Representation.char_exteriorSquare {R : Type} {G : Type v} {M : Type w} [Field R] [Monoid G] [AddCommGroup M] [Module R M] [FiniteDimensional R M] (ρ : Representation R G M) (g : G) (h2 : 2 ≠ 0) :
    (ρ.exteriorPower 2).character g = (ρ.character g ^ 2 - ρ.character (g * g)) / 2

    The character of the exterior square, χ_{Λ²}(g) = ½(χ(g)² - χ(g²)), away from characteristic two.