The permutation representation as an induced representation

For a subgroup H of a group G, inducing the trivial H-representation along H.subtype gives the permutation representation of G on the left cosets G ⧸ H, and its character is the number of fixed cosets, cast into the coefficient field.

More generally, for subgroups D ≤ C ≤ G, inducing the permutation representation of C on C ⧸ (D ⊓ C) gives the permutation representation of G on G ⧸ D: a permutation representation on cosets can be induced in stages.

Feeding the first identification into the projection formula of TauCeti/RepresentationTheory/Induction/Projection.lean gives the classical description of inducing a restricted representation, Ind_H^G (Res_H^G Y) ≅ k[G ⧸ H] ⊗ Y.

Main definitions

• TauCeti.indTrivialEquiv: the equivalence of representations Ind_H^G (trivial) ≃ k[G ⧸ H].
• TauCeti.indTrivialIso: the same statement in Rep k G.
• TauCeti.indOfMulActionQuotientEquiv: for D ≤ C, the equivalence of representations Ind_C^G k[C ⧸ (D ⊓ C)] ≃ k[G ⧸ D].
• TauCeti.indResProjection: the corollary Ind_H^G (Res_H^G Y) ≅ k[G ⧸ H] ⊗ Y of the projection formula TauCeti.indProjection.

Main statements

• TauCeti.char_ofMulAction: the character of a permutation representation at g is the number of points fixed by g, cast into k.
• TauCeti.char_ind_trivial: the character of Ind_H^G (trivial) at g is the number of cosets fixed by g, cast into k.

Both statements are equalities in k, so in positive characteristic they determine the fixed-point count only modulo the characteristic.

Implementation notes

Mathlib's Representation.ind is built as the coinvariants of k[G] ⊗[k] A, so the coset orientation is a proof obligation rather than a convention: the H-action being quotiented out is left translation on k[G], whose orbits are the right cosets Hx, while G acts by right translation by the inverse. The equivalence below therefore sends ⟦single x r ⊗ₜ a⟧ to single ⟦x⁻¹⟧ (a • r); inversion is what converts right cosets carrying a right action into Mathlib's left-coset quotient G ⧸ H with its left action. In the same way TauCeti.indOfMulActionQuotientEquiv sends ⟦single x 1 ⊗ₜ single ⟦c⟧ s⟧ to single ⟦x⁻¹ * c⟧ s.

References

• J.-P. Serre, Linear Representations of Finite Groups, §2.1 (the permutation character) and §3.3 (inducing the unit representation, and the projection formula).

noncomputable def TauCeti.indTrivialEquiv (k : Type u) [CommRing k] {G : Type v} [Group G] (H : Subgroup G) : (Representation.ind H.subtype (Representation.trivial k (↥H) k)).Equiv (Representation.ofMulAction k G (G ⧸ H))

The permutation representation. Inducing the trivial representation of a subgroup H ≤ G along H.subtype gives the permutation representation of G on the left cosets G ⧸ H.

Equations

• TauCeti.indTrivialEquiv k H = Representation.Equiv.mk (LinearEquiv.ofLinearMap (TauCeti.indTrivialToQuotient✝ k H) (TauCeti.quotientToIndTrivial✝ k H) ⋯ ⋯) ⋯

@[simp]

theorem TauCeti.indTrivialEquiv_apply_mk (k : Type u) [CommRing k] {G : Type v} [Group G] (H : Subgroup G) (x : G) (a : k) : (indTrivialEquiv k H) ((Representation.IndV.mk H.subtype (Representation.trivial k (↥H) k) x) a) = MonoidAlgebra.single (↑x⁻¹) a

The generator computation rule for TauCeti.indTrivialEquiv.

@[simp]

theorem TauCeti.indTrivialEquiv_symm_apply_single (k : Type u) [CommRing k] {G : Type v} [Group G] (H : Subgroup G) (x : G) (r : k) : (indTrivialEquiv k H).symm (MonoidAlgebra.single (↑x) r) = r • (Representation.IndV.mk H.subtype (Representation.trivial k (↥H) k) x⁻¹) 1

The generator computation rule for the inverse of TauCeti.indTrivialEquiv.

noncomputable def TauCeti.indTrivialIso (k : Type u) [CommRing k] {G : Type v} [Group G] (H : Subgroup G) : Rep.ind H.subtype (Rep.trivial k (↥H) k) ≅ Rep.ofMulAction k G (G ⧸ H)

The permutation representation, in Rep k G: inducing the trivial representation of a subgroup H ≤ G gives the permutation representation on the left cosets G ⧸ H.

Equations

• TauCeti.indTrivialIso k H = Rep.mkIso (TauCeti.indTrivialEquiv k H)

@[simp]

theorem TauCeti.indTrivialIso_hom_hom_apply_mk (k : Type u) [CommRing k] {G : Type v} [Group G] (H : Subgroup G) (x : G) (a : k) : (Rep.Hom.hom (indTrivialIso k H).hom) ((Representation.IndV.mk H.subtype (Representation.trivial k (↥H) k) x) a) = MonoidAlgebra.single (↑x⁻¹) a

The generator computation rule for TauCeti.indTrivialIso: it sends ⟦single x 1 ⊗ₜ a⟧ to single ⟦x⁻¹⟧ a.

@[simp]

theorem TauCeti.indTrivialIso_inv_hom_apply_single (k : Type u) [CommRing k] {G : Type v} [Group G] (H : Subgroup G) (x : G) (r : k) : (Rep.Hom.hom (indTrivialIso k H).inv) (MonoidAlgebra.single (↑x) r) = r • (Representation.IndV.mk H.subtype (Representation.trivial k (↥H) k) x⁻¹) 1

The computation rule for the inverse of TauCeti.indTrivialIso on the standard basis of k[G ⧸ H].

instance TauCeti.instFiniteIndTrivial (k : Type u) [CommRing k] {G : Type v} [Group G] (H : Subgroup G) [Finite (G ⧸ H)] : Module.Finite k (Representation.IndV H.subtype (Representation.trivial k (↥H) k))

Ind_H^G (trivial) is a finite module whenever H has finite index.

noncomputable def TauCeti.indOfMulActionQuotientEquiv (k : Type u) [CommRing k] {G : Type v} [Group G] {C D : Subgroup G} (h : D ≤ C) : (Representation.ind C.subtype (Representation.ofMulAction k (↥C) (↥C ⧸ D.subgroupOf C))).Equiv (Representation.ofMulAction k G (G ⧸ D))

Induction of a coset permutation representation. For subgroups D ≤ C ≤ G, inducing the permutation representation of C on its cosets C ⧸ (D ⊓ C) along C.subtype gives the permutation representation of G on G ⧸ D. For D = C this is TauCeti.indTrivialEquiv up to the identification of k[C ⧸ ⊤] with the trivial representation.

Equations

• TauCeti.indOfMulActionQuotientEquiv k h = Representation.Equiv.mk (LinearEquiv.ofLinearMap (TauCeti.indQuotientToQuotient✝ k) (TauCeti.quotientToIndQuotient✝ k h) ⋯ ⋯) ⋯

@[simp]

theorem TauCeti.indOfMulActionQuotientEquiv_apply_mk (k : Type u) [CommRing k] {G : Type v} [Group G] {C D : Subgroup G} (h : D ≤ C) (x : G) (c : ↥C) (s : k) : (indOfMulActionQuotientEquiv k h) ((Representation.IndV.mk C.subtype (Representation.ofMulAction k (↥C) (↥C ⧸ D.subgroupOf C)) x) (MonoidAlgebra.single (↑c) s)) = MonoidAlgebra.single (↑(x⁻¹ * ↑c)) s

The generator computation rule for TauCeti.indOfMulActionQuotientEquiv: it sends ⟦single x 1 ⊗ₜ single ⟦c⟧ s⟧ to single ⟦x⁻¹ * c⟧ s.

@[simp]

theorem TauCeti.indOfMulActionQuotientEquiv_symm_apply_single (k : Type u) [CommRing k] {G : Type v} [Group G] {C D : Subgroup G} (h : D ≤ C) (x : G) (r : k) : (indOfMulActionQuotientEquiv k h).symm (MonoidAlgebra.single (↑x) r) = r • (Representation.IndV.mk C.subtype (Representation.ofMulAction k (↥C) (↥C ⧸ D.subgroupOf C)) x⁻¹) (MonoidAlgebra.single (↑1) 1)

The generator computation rule for the inverse of TauCeti.indOfMulActionQuotientEquiv.

noncomputable def TauCeti.indResProjection {k G : Type u} [CommRing k] [Group G] {H : Subgroup G} (Y : Rep.{u, u, u} k G) : Rep.ind H.subtype (Rep.res H.subtype Y) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (Rep.ofMulAction k G (G ⧸ H)) Y

Induction of a restriction. For a subgroup H ≤ G, restricting a G-representation to H and inducing back up tensors it with the permutation representation on the cosets, Ind_H^G (Res_H^G Y) ≅ k[G ⧸ H] ⊗ Y. This is TauCeti.indProjection applied to the trivial H-representation, followed by TauCeti.indTrivialIso.

Equations

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

@[simp]

theorem TauCeti.indResProjection_hom_hom_apply {k G : Type u} [CommRing k] [Group G] {H : Subgroup G} (Y : Rep.{u, u, u} k G) (x : G) (y : ↑Y) : (Rep.Hom.hom (indResProjection Y).hom) ((Representation.IndV.mk H.subtype (Rep.res H.subtype Y).ρ x) y) = MonoidAlgebra.single (↑x⁻¹) 1 ⊗ₜ[k] (Y.ρ x⁻¹) y

TauCeti.indResProjection on generators: the coset orientation is the one inherited from TauCeti.indTrivialIso, which sends ⟦x ⊗ₜ a⟧ to single ⟦x⁻¹⟧ a.

@[simp]

theorem TauCeti.char_ofMulAction (k : Type u) [Field k] {G : Type v} [Monoid G] (X : Type w) [MulAction G X] [Finite X] (g : G) : (Representation.ofMulAction k G X).character g = ↑(Nat.card { x : X // g • x = x })

The permutation character. The character of the permutation representation k[X] at g is the number of points of X fixed by g, cast into k.

@[simp]

theorem TauCeti.char_ind_trivial (k : Type u) [Field k] {G : Type v} [Group G] (H : Subgroup G) [Finite (G ⧸ H)] (g : G) : (Representation.ind H.subtype (Representation.trivial k (↥H) k)).character g = ↑(Nat.card { q : G ⧸ H // g • q = q })

The permutation character of an induced trivial representation. The character of Ind_H^G (trivial) at g is the number of cosets in G ⧸ H fixed by g, cast into k.