Inducing the trivial representation from a point stabilizer #
Let α be a finite set and let x₀ : α. The symmetric group Equiv.Perm α acts transitively on
α, so the coset space of the stabilizer of x₀ is α itself, and inducing the trivial
representation of that stabilizer produces the permutation representation of Equiv.Perm α on
α. This file makes that identification, reads off its character as the fixed-point count, and
computes the invariant the permutation representation is pinned down by: the double cosets of the
stabilizer, of which there are exactly two, and hence the self-pairing of the induced character.
The two double cosets are the source of everything else. A permutation either fixes x₀ or does
not, and each of the two possibilities is a single double coset, by
TauCeti.card_doubleCosetQuotient_stabilizer. So ⟨Ind 1, Ind 1⟩ = 2 whenever |Equiv.Perm α|
is invertible in k, and the permutation representation then has exactly two constituents, each
with multiplicity one. When moreover (|α| : k) ≠ 0 those two constituents are named: the
trivial representation on the invariant line, split off by
TauCeti.isCompl_invariantLine_augmentationSubrepresentation, and the standard representation of
TauCeti.RepresentationTheory.Symmetric.Standard, which is irreducible under that same
hypothesis. In the excluded characteristics the character identity
TauCeti.char_ind_trivial_stabilizer_eq_one_add_char_standardRepresentation still holds, but the
invariant line lies inside the standard representation instead of complementing it, so there is no
such splitting.
Main definitions #
TauCeti.indTrivialStabilizerEquivandTauCeti.indTrivialStabilizerIso: inducing the trivial representation of the stabilizer ofx₀gives the permutation representation onα, as an equivalence of representations and as an isomorphism inRep k (Equiv.Perm α). Both are read on generators byTauCeti.indTrivialStabilizerEquiv_apply_mkandTauCeti.indTrivialStabilizerIso_hom_hom_mk.
Main statements #
TauCeti.char_ind_trivial_stabilizer: the character of the induced trivial representation atσis the number of points fixed byσ, andTauCeti.finrank_ind_trivial_stabilizersays the representation has dimension|α|.TauCeti.characterPairing_ind_trivial_stabilizer: for|Equiv.Perm α|invertible ink, its self-pairing is2, the number of double cosets.TauCeti.char_ind_trivial_stabilizer_eq_one_add_char_standardRepresentation: the induced character is the trivial character plus the character of the standard representation. This is an identity of characters and holds in every characteristic; it is a decomposition of representations only under the hypotheses ofTauCeti.isCompl_invariantLine_augmentationSubrepresentation.TauCeti.card_doubleCosetQuotient_stabilizer_fin_four,TauCeti.finrank_ind_trivial_stabilizer_fin_four,TauCeti.finrank_augmentationSubrepresentation_fin_fourandTauCeti.isIrreducible_standardRepresentation_fin_four: theS₄instance -- two double cosets, a4-dimensional induced representation, and a3-dimensional complement, irreducible when4 ≠ 0ink.
Implementation notes #
The two double cosets of the point stabilizer are counted in
TauCeti.GroupTheory.DoubleCoset.PointStabilizer, which is pure group theory, and the
identification of the coset space with α is TauCeti.quotientStabilizerEquiv, in
TauCeti.GroupTheory.GroupAction.Transitive.
The coefficient field and the acted-on set share a universe in the Rep-level isomorphism, since
that compares two objects of one category; the Representation-level statements, which is where
the characters are computed, carry no such constraint.
References #
This is the "Permutation characters and fixed points" worked example of
TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md: "For G = S₄ and H a point
stabilizer S₃, Ind_H^G(trivial) is the natural permutation representation on 4 points; its
character at g is the number of fixed points of g, and ⟨Ind_H^G 1, Ind_H^G 1⟩ = #(H \ G / H) = 2, the two double cosets being the diagonal and off-diagonal H-orbits on the four points, so it
splits as trivial ⊕ (standard 3-dimensional)."
- J.-P. Serre, Linear Representations of Finite Groups, §2.3 and §7.3.
The induced representation is the permutation representation on the points #
Inducing the trivial representation of a point stabilizer. Because Equiv.Perm α acts
transitively on α, inducing the trivial representation of the stabilizer of x₀ gives the
permutation representation of Equiv.Perm α on α itself.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The generator computation rule for TauCeti.indTrivialStabilizerEquiv: the generator carried
by σ goes to the basis vector of the point σ⁻¹ x₀.
The permutation character. The character at σ of the trivial representation of the
stabilizer of x₀ induced up to Equiv.Perm α is the number of points of α fixed by σ.
Not a simp lemma: the general TauCeti.char_ind_trivial is one, and it already rewrites this
left-hand side -- to the number of fixed cosets -- so tagging this specialisation fails the
simpNF linter.
The induced representation has dimension the number of points.
The self-pairing of the permutation character is 2, the number of double cosets of the
point stabilizer. So the permutation representation has exactly two irreducible constituents, each
occurring once.
The permutation character is the trivial character plus the standard one. This is an
identity of characters, and it needs no hypothesis on the characteristic of k. It becomes the
decomposition Ind_H^G 1 ≅ trivial ⊕ standard when (Fintype.card α : k) ≠ 0: that is the
hypothesis under which TauCeti.isCompl_invariantLine_augmentationSubrepresentation splits the
invariant line off the permutation representation and
TauCeti.isIrreducible_standardRepresentation makes the remaining constituent irreducible. When
(Fintype.card α : k) = 0 and 3 ≤ |α| the invariant line instead lies inside the standard
representation, and there is no such splitting.
The Rep-level form #
Objects of Rep k G live over one universe, so the isomorphism form of the identification
constrains the coefficient ring and the acted-on set to share a universe.
Inducing the trivial representation of a point stabilizer, in Rep k (Equiv.Perm α).
Equations
Instances For
The generator computation rule for TauCeti.indTrivialStabilizerIso: it is
TauCeti.indTrivialStabilizerEquiv_apply_mk read in Rep k (Equiv.Perm α).
The S₄ instance #
G = S₄ with H the stabilizer of a point is the worked example: the induced trivial
representation is the natural permutation representation on four points, there are two double
cosets, and over a field in which 4 ≠ 0 the representation splits as the trivial one plus a
three-dimensional irreducible.
The stabilizer of a point of Fin 4 has two double cosets in S₄: the two orbits of S₄ on
ordered pairs of points, the diagonal and the off-diagonal one.
Ind_{S₃}^{S₄} 1 is four-dimensional: it is the permutation representation on four points.
The complementary constituent of Ind_{S₃}^{S₄} 1 is three-dimensional.
The standard representation of S₄ is irreducible over a field in which 4 is nonzero, so
Ind_{S₃}^{S₄} 1 really is the trivial representation plus a three-dimensional irreducible.