The Young permutation module of the shape (n-1, 1)

Among the Young permutation modules M^μ of the symmetric group, the shape μ = (n-1, 1) is the one whose tabloids carry no information beyond a single label: a tabloid of that shape is a splitting of the n labels into a row of n-1 and a row of 1, so it is named by the label sent to the short row. This file records exactly that, in the form the rest of the theory uses it: the Young subgroup of (n-1, 1) is the stabilizer of a point, so M^{(n-1,1)} is the natural permutation module ℚ[Fin n] on the n labels, and hence the trivial representation plus the standard one.

The shape is TauCeti.Nat.Partition.singletonSecondRow n, the partition (n+1, 1) of n+2; the offset keeps both parts positive without a hypothesis on n. The structural fact this file rests on is proved with the rest of the Young-subgroup theory, in TauCeti.RepresentationTheory.Symmetric.YoungSubgroup: the two blocks of (n+1, 1) are all the labels but the last one and the last one alone, so TauCeti.youngSubgroup_singletonSecondRow identifies the Young subgroup with the stabilizer of Fin.last (n+1).

Everything here is transport. The cosets of a point stabilizer of a transitive action are the points (TauCeti.quotientStabilizerEquiv), equivariantly, and an equivariant equivalence of G-sets induces an isomorphism of the permutation representations they carry (TauCeti.ofMulActionIsoCongr). Reading the two invariants of M^{(n-1,1)} through that isomorphism replaces the multinomial dimension n! / (n-1)! by n, and the count of fixed tabloids by the count of fixed points -- the natural permutation character. Splitting ℚ[Fin (n+2)] into the invariant line and the augmentation subrepresentation (TauCeti.ofMulActionEquivProdAugmentation) then decomposes M^{(n-1,1)} as the trivial representation plus the standard representation. On characters that decomposition is the point-stabilizer identity TauCeti.char_ind_trivial_stabilizer_eq_one_add_char_standardRepresentation.

Main definitions

• TauCeti.singletonSecondRowTabloidEquiv: the tabloids of (n+1, 1) are the labels, the coset of g naming g applied to the last label.
• TauCeti.permutationModuleSingletonSecondRowIso: hence M^{(n+1,1)} is ℚ[Fin (n+2)].
• TauCeti.permutationModuleSingletonSecondRowEquivProd: M^{(n-1,1)} = triv ⊕ standard, an equivalence of representations onto the product of the trivial representation on ℚ and the standard representation, computed by TauCeti.permutationModuleSingletonSecondRowEquivProd_apply as the splitting of ℚ[Fin (n+2)] at the transported vector and inverted by TauCeti.permutationModuleSingletonSecondRowEquivProd_symm_apply, which reassembles a pair as the corresponding multiple of the sum of the standard basis plus the given vector.

Main results

• TauCeti.finrank_permutationModule_singletonSecondRow: M^{(n+1,1)} has dimension n+2.
• TauCeti.char_permutationModule_singletonSecondRow: its character counts fixed points, and TauCeti.char_permutationModule_singletonSecondRow_eq_one_add_char_standardRepresentation: that character is 1 plus the character of the standard representation.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapter 4, where M^{(n-1,1)} is the permutation module on the n labels.
• W. Fulton, Young Tableaux, Section 7.2.

The permutation module of the shape (n+1, 1)

noncomputable def TauCeti.singletonSecondRowTabloidEquiv (n : ℕ) : Equiv.Perm (Fin (n + 2)) ⧸ youngSubgroup (Nat.Partition.singletonSecondRow n) ≃ Fin (n + 2)

The tabloids of the shape (n+1, 1) are the points. The Young subgroup of (n+1, 1) is the stabilizer of the last label, so the coset of g names the point g sends that label to.

Equations

• TauCeti.singletonSecondRowTabloidEquiv n = (Subgroup.quotientEquivOfEq ⋯).trans (TauCeti.quotientStabilizerEquiv (Equiv.Perm (Fin (n + 2))) (Fin.last (n + 1)))

@[simp]

theorem TauCeti.singletonSecondRowTabloidEquiv_mk (n : ℕ) (g : Equiv.Perm (Fin (n + 2))) : (singletonSecondRowTabloidEquiv n) ↑g = g (Fin.last (n + 1))

The tabloid named by g is the point g sends the last label to.

@[simp]

theorem TauCeti.singletonSecondRowTabloidEquiv_smul (n : ℕ) (σ : Equiv.Perm (Fin (n + 2))) (q : Equiv.Perm (Fin (n + 2)) ⧸ youngSubgroup (Nat.Partition.singletonSecondRow n)) : (singletonSecondRowTabloidEquiv n) (σ • q) = σ • (singletonSecondRowTabloidEquiv n) q

The identification of the (n+1, 1)-tabloids with the points is equivariant.

noncomputable def TauCeti.permutationModuleSingletonSecondRowIso (n : ℕ) : permutationModule (Nat.Partition.singletonSecondRow n) ≅ Rep.ofMulAction ℚ (Equiv.Perm (Fin (n + 2))) (Fin (n + 2))

The Young permutation module of (n+1, 1) is the natural permutation module. Since the (n+1, 1)-tabloids are the points of Fin (n+2), the module M^{(n+1,1)} is ℚ[Fin (n+2)] with the symmetric group permuting the standard basis.

Equations

• TauCeti.permutationModuleSingletonSecondRowIso n = TauCeti.ofMulActionIsoCongr ℚ (TauCeti.singletonSecondRowTabloidEquiv n) ⋯

@[simp]

theorem TauCeti.permutationModuleSingletonSecondRowIso_hom_hom_single (n : ℕ) (g : Equiv.Perm (Fin (n + 2))) (r : ℚ) : (Rep.Hom.hom (permutationModuleSingletonSecondRowIso n).hom) (MonoidAlgebra.single (↑g) r) = MonoidAlgebra.single (g (Fin.last (n + 1))) r

The isomorphism sends the tabloid named by g to the point g moves the last label to.

@[simp]

theorem TauCeti.permutationModuleSingletonSecondRowIso_inv_hom_single (n : ℕ) (x : Fin (n + 2)) (r : ℚ) : (Rep.Hom.hom (permutationModuleSingletonSecondRowIso n).inv) (MonoidAlgebra.single x r) = MonoidAlgebra.single ((singletonSecondRowTabloidEquiv n).symm x) r

The inverse isomorphism sends a point back to the tabloid naming it.

@[simp]

theorem TauCeti.finrank_permutationModule_singletonSecondRow (n : ℕ) : Module.finrank ℚ ↑(permutationModule (Nat.Partition.singletonSecondRow n)) = n + 2

The Young permutation module of (n+1, 1) has dimension n+2, the number of points, rather than the multinomial coefficient (n+2)! / (n+1)! in the shape it is presented by.

theorem TauCeti.char_permutationModule_singletonSecondRow (n : ℕ) (σ : Equiv.Perm (Fin (n + 2))) : (permutationModule (Nat.Partition.singletonSecondRow n)).ρ.character σ = ↑(Nat.card { x : Fin (n + 2) // σ x = x })

The character of M^{(n+1,1)} counts fixed points. In the tabloid presentation the character counts fixed tabloids; for the shape (n+1, 1) those are the points of Fin (n+2), so it is the natural permutation character.

The decomposition M^{(n+1,1)} = triv ⊕ standard

noncomputable def TauCeti.permutationModuleSingletonSecondRowEquivProd (n : ℕ) : (permutationModule (Nat.Partition.singletonSecondRow n)).ρ.Equiv ((Representation.trivial ℚ (Equiv.Perm (Fin (n + 2))) ℚ).prod (standardRepresentation ℚ (Fin (n + 2))))

The Young permutation module of (n+1, 1) is the trivial representation plus the standard representation. Transporting M^{(n+1,1)} to ℚ[Fin (n+2)] along TauCeti.permutationModuleSingletonSecondRowIso and splitting the latter along TauCeti.ofMulActionEquivProdAugmentation -- the invariant line, which carries the trivial representation on ℚ itself, is a complement of the augmentation subrepresentation, n+2 being invertible in ℚ -- decomposes it as a product of two representations, the second being the standard representation by TauCeti.toRepresentation_augmentationSubrepresentation. In short, M^{(n-1,1)} = triv ⊕ standard.

Equations

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

@[simp]

theorem TauCeti.permutationModuleSingletonSecondRowEquivProd_apply (n : ℕ) (v : ↑(permutationModule (Nat.Partition.singletonSecondRow n))) : (permutationModuleSingletonSecondRowEquivProd n) v = (ofMulActionEquivProdAugmentation ℚ (Equiv.Perm (Fin (n + 2))) (Fin (n + 2)) ⋯) ((Rep.Hom.hom (permutationModuleSingletonSecondRowIso n).hom) v)

The decomposition is the splitting of ℚ[Fin (n+2)], read through the identification of the tabloids with the labels. The two components of a vector are therefore computed by TauCeti.ofMulActionEquivProdAugmentation_apply_fst and TauCeti.coe_ofMulActionEquivProdAugmentation_apply_snd at the vector of ℚ[Fin (n+2)] that TauCeti.permutationModuleSingletonSecondRowIso transports it to, which for the tabloid named by g is the standard basis vector of g (Fin.last (n+1)).

@[simp]

theorem TauCeti.permutationModuleSingletonSecondRowEquivProd_symm_apply (n : ℕ) (v : ℚ × ↥(augmentationSubrepresentation ℚ (Equiv.Perm (Fin (n + 2))) (Fin (n + 2))).toSubmodule) : (permutationModuleSingletonSecondRowEquivProd n).symm v = (Rep.Hom.hom (permutationModuleSingletonSecondRowIso n).inv) (v.1 • permutationSum ℚ (Fin (n + 2)) + ↑v.2)

A pair is reassembled into a tabloid vector by adding a multiple of the sum of the standard basis. Inverting the splitting of ℚ[Fin (n+2)] sends a scalar c and a vector w of the standard representation to c • permutationSum ℚ (Fin (n+2)) + w, by TauCeti.ofMulActionEquivProdAugmentation_symm_apply; the identification of the labels with the tabloids then carries that back to M^{(n+1,1)}.

theorem TauCeti.char_permutationModule_singletonSecondRow_eq_one_add_char_standardRepresentation (n : ℕ) (σ : Equiv.Perm (Fin (n + 2))) : (permutationModule (Nat.Partition.singletonSecondRow n)).ρ.character σ = 1 + (standardRepresentation ℚ (Fin (n + 2))).character σ

The character of M^{(n+1,1)} is 1 plus the character of the standard representation. This is the character-level form of the decomposition TauCeti.permutationModuleSingletonSecondRowEquivProd, and it is a specialization of the point-stabilizer identity TauCeti.char_ind_trivial_stabilizer_eq_one_add_char_standardRepresentation.