Invariants of the dual representation

The inverse automorphism of the dual representation is the transpose of the original representation's automorphism.

The dual ρ.dual of a representation acts on functionals by ψ ↦ ψ ∘ ρ g⁻¹, so a functional invariant for it is exactly one that the action of G on the space leaves unchanged: ψ (ρ g u) = ψ u. That characterization of membership in ρ.dual.invariants is all a construction out of an invariant functional, or of one, ever needs.

Counting those invariants needs the character machinery. The character of the dual is the character of ρ read along g⁻¹, and summing over the group is unchanged by inversion, so the two averages agree: the dual has as many invariants as the representation itself. Averaging characters produces identities in k and nothing more, so that count is stated first in k, needing only an invertible |G|; in characteristic p it is an identity of residues, and it is the injectivity of ℕ → k in characteristic zero that turns it into an equality of dimensions.

Main results

• TauCeti.Representation.mem_invariants_dual_iff: a functional is invariant for ρ.dual exactly when the action of G leaves it unchanged, with TauCeti.Representation.apply_of_mem_invariants_dual the elimination direction.
• TauCeti.Representation.finrank_invariants_dual: the dual of a representation has as many invariants as the representation, as an identity in k whenever |G| is invertible (TauCeti.Representation.finrank_invariants_dual_cast) and as natural numbers in characteristic zero.

References

• Character theory roadmap, Layer 7, “Invariant bilinear forms”: the invariant forms of ρ are the intertwiners into ρ.dual, so counting them is counting invariants of a dual.

theorem Representation.generalLinearEquiv_dual_asGroupHom_symm {R : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring R] [Group G] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) (g : G) : ((LinearMap.GeneralLinearGroup.generalLinearEquiv R (Module.Dual R V)) (ρ.dual.asGroupHom g)).symm = ((LinearMap.GeneralLinearGroup.generalLinearEquiv R V) (ρ.asGroupHom g)).dualMap

The inverse linear automorphism of the dual representation is the transpose of the original representation's linear automorphism.

Invariant functionals

theorem TauCeti.Representation.mem_invariants_dual_iff {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {ψ : Module.Dual k V} : ψ ∈ ρ.dual.invariants ↔ ∀ (g : G) (u : V), ψ ((ρ g) u) = ψ u

A functional is invariant for the dual of a representation exactly when the action of G leaves it unchanged.

theorem TauCeti.Representation.apply_of_mem_invariants_dual {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {ψ : Module.Dual k V} (hψ : ψ ∈ ρ.dual.invariants) (g : G) (u : V) : ψ ((ρ g) u) = ψ u

A functional invariant for the dual of a representation is unchanged by the action.

Counting the invariants of a dual

theorem TauCeti.Representation.finrank_invariants_dual_cast {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [Finite G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Invertible ↑(Nat.card G)] (ρ : Representation k G V) : ↑(Module.finrank k ↥ρ.dual.invariants) = ↑(Module.finrank k ↥ρ.invariants)

The dual of a representation has as many invariants as the representation, as an identity in k: both counts average the same character, one along g and the other along g⁻¹.

Averaging characters only ever produces identities in k. In characteristic p this is one of residues; see TauCeti.Representation.finrank_invariants_dual for the characteristic-zero form, where the two counts agree as natural numbers.

theorem TauCeti.Representation.finrank_invariants_dual {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [Finite G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [CharZero k] (ρ : Representation k G V) : Module.finrank k ↥ρ.dual.invariants = Module.finrank k ↥ρ.invariants

The dual of a representation has as many invariants as the representation, as natural numbers. Characteristic zero is what lifts TauCeti.Representation.finrank_invariants_dual_cast from an identity in k.