Documentation

TauCeti.RepresentationTheory.Continuous.Square.Character

The characters of the two squares of a continuous representation #

The symmetric square and the exterior square of a representation have characters χ_{Sym²} and χ_{Λ²}; away from characteristic two they are determined by the character of the representation through χ_{Sym²}(g) = ½(χ(g)² + χ(g²)) and χ_{Λ²}(g) = ½(χ(g)² - χ(g²)) (Representation.char_symmetricSquare and Representation.char_exteriorSquare of TauCeti/RepresentationTheory/Tensor/Square.lean). For a representation with continuous operator-valued action those closed formulas exhibit both square characters as continuous functions of g, which is what the first section records.

Neither continuity statement needs the symmetric or exterior square to be assembled as a continuous representation: the closed formulas are used as they stand, so only the continuity of χ and of g ↦ χ(g * g) (ContRepresentation.continuous_character_mul_self) enters.

The second section reads the difference of the two square characters on the squares that TauCeti/RepresentationTheory/Continuous/Square/Basic.lean does assemble as continuous representations, the eigenspaces of the flip inside V ⊗[𝕜] V: there χ_{Sym²}(g) - χ_{Λ²}(g) = χ(g²), which is the linear-algebra identity TauCeti.trace_symmetricTensorsRestrict_sub_trace_antisymmetricTensorsRestrict applied to π g. Subtracting the two closed formulas above gives the same identity on the powers, so the two sections agree wherever both apply.

Main statements #

Implementation notes #

Nothing here needs a group, a measure, or compactness, so the statements are made over a topological monoid; the consumers are TauCeti/RepresentationTheory/Compact/FrobeniusSchur/Basic.lean, where continuity supplies the integrability of the two square characters against Haar measure, and TauCeti/RepresentationTheory/Compact/FrobeniusSchur/InvariantTensors.lean, where the pointwise identity is integrated against it.

The two sections ask different things of the scalars. For the continuity statements they are a complete nontrivially normed field 𝕜 with 2 ≠ 0 — exactly what the trace functional behind ContRepresentation.character and the closed formulas ask for; the consumer instantiates them at ℂ. There 𝕜 is in Type rather than Type* because the symmetric- and exterior-power representations of TauCeti/RepresentationTheory/SymmetricPower.lean and TauCeti/RepresentationTheory/ExteriorPower.lean, whose characters are spoken of, are built over a base ring in Type, so a field in an arbitrary universe would not even let the statements be formed. The hypothesis 2 ≠ 0 is explicit rather than a CharZero-style instance because that is the shape Representation.char_symmetricSquare and Representation.char_exteriorSquare carry. The pointwise identity instead needs the two squares of TauCeti/RepresentationTheory/Continuous/Square/Basic.lean, whose carriers are submodules of an inner product space, so its scalars are RCLike 𝕜, in any universe, and 2 is invertible there by instance.

All declarations sit in the root ContRepresentation namespace, so that π.continuous_character_symmetricPower_two hπ elaborates. The ambient TauCeti constructions this file consumes are brought in by open.

source
theorem ContRepresentation.continuous_character_symmetricPower_two {𝕜 : Type} {G : Type u_1} {V : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (h2 : 2 ≠ 0) :
Continuous fun (g : G) => ((toRepresentation 𝕜 G V π).symmetricPower 2).character g

The symmetric-square character is continuous, being ½(χ(g)² + χ(g²)).

source
theorem ContRepresentation.continuous_character_exteriorPower_two {𝕜 : Type} {G : Type u_1} {V : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (h2 : 2 ≠ 0) :
Continuous fun (g : G) => ((toRepresentation 𝕜 G V π).exteriorPower 2).character g

The exterior-square character is continuous, being ½(χ(g)² - χ(g²)).

source
theorem ContRepresentation.character_symmetricSquare_sub_character_exteriorSquare {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (g : G) :
(π.symmetricSquare.character ⋯) g - (π.exteriorSquare.character ⋯) g = (π.character hπ) (g * g)

The two square characters differ by the character at the square, χ_{Sym²π}(g) - χ_{Λ²π}(g) = χ_π(g²).

This is TauCeti.trace_symmetricTensorsRestrict_sub_trace_antisymmetricTensorsRestrict applied to the operator π g, whose square is π (g * g).