The constituents of a restriction to a normal subgroup share one hom-space dimension

Let N be a normal subgroup of G and let ρ be an irreducible representation of G on V. Restricting ρ to N breaks it into irreducible constituents, and TauCeti/RepresentationTheory/Induction/Clifford/Orbit/Basic.lean identifies which constituents occur: they are the translates TauCeti.Representation.conjSubrep ρ g σ of any one of them, so they form a single G-orbit. This file supplies the other half of Clifford's theorem: they all have hom spaces of one common dimension, which over a splitting field is their common multiplicity.

The quantity compared throughout is Module.finrank k (S →ₗ[k[N]] M). It is the classical multiplicity of a simple k[N]-module S in M only when k splits S: in general it is the multiplicity times Module.finrank k of the division ring End_{k[N]}(S). Accordingly TauCeti/RingTheory/Semisimple/Multiplicity.lean identifies it with a count of the factors isomorphic to S only for an algebraically closed k, a finite-dimensional S and a finite decomposition of M, the case in which that division ring is k itself. Everything below instead compares two such dimensions for two constituents of the same restriction, and that comparison is a transport statement rather than a counting one: it needs no decomposition of the restriction, no algebraically closed field and no finiteness, so no such hypothesis is imposed, and the statements say only that the dimensions agree. Whenever ρ is irreducible and V is finite-dimensional the restriction is semisimple (TauCeti.Representation.isSemisimpleRepresentation_comp_subtype), so there is a decomposition to count there; if in addition k splits the constituents, the common dimension produced below is literally the classical multiplicity e.

What makes the transport work is the one identity Clifford theory runs on, ρ g ∘ ρ n = ρ (g n g⁻¹) ∘ ρ g (Representation.apply_conjNormal_inv, read in the other direction). On the restriction viewed as a module over k[N], it says that translation by ρ g (Representation.asModuleConjEquiv) is not k[N]-linear but semilinear over the conjugation automorphism MonoidAlgebra.conjNormalAlgAut k k N g of k[N] (Representation.asModuleConjEquiv_smul). A single semilinear map would not act on hom spaces at all; but conjugating a map f -- precomposing with translation by ρ g and postcomposing with translation back by ρ g⁻¹ -- twists it by conjNormalAlgAut g and then by conjNormalAlgAut g⁻¹, and those two twists cancel. So Representation.conjHom really does land in k[N]-linear maps, and it is a k-linear isomorphism of hom spaces (Representation.conjHomEquiv).

Combining the transport with the single-orbit theorem gives the common dimension: any two minimal N-stable subspaces are translates of one another up to isomorphism, so their hom spaces have equal dimension. The same argument on the subspaces themselves, where the twist is invisible because only the k-action is retained, shows that all the constituents have the same dimension as well; there it is TauCeti.Representation.conjSubrepEquiv from Clifford/Basic.lean that does the work.

Main definitions

• Representation.asModuleConjEquiv: translation by ρ g, as a k-linear automorphism of the restriction to N viewed as a k[N]-module.
• Representation.conjSubrepMap: translation restricted to a pair of N-subrepresentations that it maps into one another.
• Representation.conjHom, Representation.conjHomₗ and Representation.conjHomEquiv: the induced transport of hom spaces, as a function, as a k-linear map, and as a k-linear isomorphism.

Main statements

• Representation.asModuleConjEquiv_smul: translation is semilinear over MonoidAlgebra.conjNormalAlgAut.
• Representation.finrank_linearMap_conjSubrep and Representation.finrank_asSubmodule_conjSubrep: a translate has a hom space of the same dimension, and is itself of the same dimension.
• Representation.finrank_linearMap_eq_of_isAtom: Clifford's theorem, multiplicity form -- any simple k[N]-submodule of the restriction of an irreducible representation has a hom space of the same dimension as that of a given minimal N-stable subspace; Representation.finrank_linearMap_eq_of_isAtom_of_isAtom is the form comparing two minimal N-stable subspaces. Over a splitting field this says that the constituents occur with the same multiplicity.
• Representation.finrank_asSubmodule_eq_of_isAtom_of_isAtom: they also all have the same dimension.
• Representation.finrank_linearMap_pos and Representation.exists_forall_finrank_linearMap_eq: over a finite-dimensional V that common dimension is a positive natural number e, which over a splitting field is the e of the classical statement Res_N W ≅ e · ⨁ᵢ {}^{gᵢ} V.

Implementation notes

The k[N]-module carrying the restriction is Representation.asModule (ρ.comp N.subtype), a type synonym for V, and its constituents are presented as Subrepresentation.asSubmodule of atoms of the lattice of N-subrepresentations, exactly as in Orbit/Basic.lean; the two presentations are matched by Subrepresentation.isSimpleModule_asSubmodule_iff. Because the synonym is not syntactically V, translation is packaged as the bundled asModuleConjEquiv and not used as the bare ρ g: that is what puts the k[N]-scalar actions in the statements below on the type where they are found.

The declarations here extend Mathlib's Representation namespace, so they are declared into it directly rather than into TauCeti.Representation, which would lose dot notation and be rejected by scripts/lint-dot-notation.py. The transport itself asks only for a commutative base semiring and an additive commutative monoid; a field enters only where the single-orbit theorem of Orbit/Basic.lean does.

References

This proves the multiplicity half of the Clifford's theorem milestone of Layer 5 of TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md: "its irreducible N-constituents form a single G-orbit, all with the same multiplicity e". The remaining part of that milestone, the packaged decomposition Res_N W ≅ e · ⨁ᵢ {}^{gᵢ} V indexed by a transversal of the inertia group, is not proved here.

The mathematics is the classical argument of C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, §49.

noncomputable def Representation.asModuleConjEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} (ρ : Representation k G V) (g : G) : asModule (MonoidHom.comp ρ N.subtype) ≃ₗ[k] asModule (MonoidHom.comp ρ N.subtype)

Translation by ρ g, read on the restriction to N viewed as a module over k[N]. As a map of k-modules it is an isomorphism, with inverse translation by ρ g⁻¹; it is not k[N]-linear, only semilinear over MonoidAlgebra.conjNormalAlgAut k k N g (Representation.asModuleConjEquiv_smul).

theorem Representation.asModuleConjEquiv_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} (ρ : Representation k G V) (g : G) (v : asModule (MonoidHom.comp ρ N.subtype)) : (ρ.asModuleConjEquiv g) v = (ρ g) v

Translation is given by ρ g. Not a simp lemma: rewriting with it moves a term off the type synonym Representation.asModule, where the k[N]-action lives.

@[simp]

theorem Representation.asModuleConjEquiv_symm {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} (ρ : Representation k G V) (g : G) : (ρ.asModuleConjEquiv g).symm = ρ.asModuleConjEquiv g⁻¹

Translating back by ρ g⁻¹ inverts translating by ρ g.

@[simp]

theorem Representation.asModuleConjEquiv_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) (g : G) (a : MonoidAlgebra k ↥N) (v : asModule (MonoidHom.comp ρ N.subtype)) : (ρ.asModuleConjEquiv g) (a • v) = ((MonoidAlgebra.conjNormalAlgAut k k N) g) a • (ρ.asModuleConjEquiv g) v

Translation is semilinear over conjugation. Moving a group-algebra scalar across translation by ρ g conjugates it: this is the conjugation identity Representation.apply_conjNormal_inv, read in the other direction and extended from the basis to all of k[N] by linearity. It is the reason a single translation does not act on k[N]-linear maps, and the reason a conjugate pair of translations does.

noncomputable def Representation.conjSubrepMap {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} (ρ : Representation k G V) {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (x : ↥σ.asSubmodule) : ↥τ.asSubmodule

Translation by ρ g, restricted to a pair of N-subrepresentations that it maps into one another: it sends a vector of σ to its translate, read as a vector of τ. The target τ is an explicit part of the data -- which translate is being landed in is part of what the map is -- and h is the accompanying proof that the translate does land in it.

@[simp]

theorem Representation.coe_conjSubrepMap {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} {ρ : Representation k G V} {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (x : ↥σ.asSubmodule) : ↑(ρ.conjSubrepMap g h x) = (ρ.asModuleConjEquiv g) ↑x

The underlying vector of a translated vector.

@[simp]

theorem Representation.conjSubrepMap_zero {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} {ρ : Representation k G V} {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) : ρ.conjSubrepMap g h 0 = 0

Translation on subrepresentations takes 0 to 0.

@[simp]

theorem Representation.conjSubrepMap_add {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} {ρ : Representation k G V} {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (x y : ↥σ.asSubmodule) : ρ.conjSubrepMap g h (x + y) = ρ.conjSubrepMap g h x + ρ.conjSubrepMap g h y

Translation on subrepresentations is additive.

@[simp]

theorem Representation.conjSubrepMap_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (a : MonoidAlgebra k ↥N) (x : ↥σ.asSubmodule) : ρ.conjSubrepMap g h (a • x) = ((MonoidAlgebra.conjNormalAlgAut k k N) g) a • ρ.conjSubrepMap g h x

Translation on subrepresentations is semilinear over conjugation.

@[simp]

theorem Representation.conjSubrepMap_inv_self_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} {ρ : Representation k G V} {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (h' : ∀ v ∈ τ, (ρ g⁻¹) v ∈ σ) (x : ↥σ.asSubmodule) : ρ.conjSubrepMap g⁻¹ h' (ρ.conjSubrepMap g h x) = x

Translating and translating back is the identity on σ.

@[simp]

theorem Representation.conjSubrepMap_self_inv_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} {ρ : Representation k G V} {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (h' : ∀ v ∈ τ, (ρ g⁻¹) v ∈ σ) (y : ↥τ.asSubmodule) : ρ.conjSubrepMap g h (ρ.conjSubrepMap g⁻¹ h' y) = y

Translating back and translating is the identity on τ.

noncomputable def Representation.conjHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (f : ↥τ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)) : ↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)

Transporting a hom space along a translation. Precomposing with translation by ρ g and postcomposing with translation back by ρ g⁻¹ turns a k[N]-linear map out of τ into one out of σ. Each translation is only semilinear over k[N], but the two twists are conjNormalAlgAut g and conjNormalAlgAut g⁻¹, which cancel, so the composite is k[N]-linear again.

@[simp]

theorem Representation.conjHom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (f : ↥τ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)) (x : ↥σ.asSubmodule) : (ρ.conjHom g h f) x = (ρ.asModuleConjEquiv g⁻¹) (f (ρ.conjSubrepMap g h x))

Evaluation of a transported map.

noncomputable def Representation.conjHomₗ {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) : (↥τ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)) →ₗ[k] ↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)

Representation.conjHom bundled as a k-linear map of hom spaces.

@[simp]

theorem Representation.conjHomₗ_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (f : ↥τ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)) : (ρ.conjHomₗ g h) f = ρ.conjHom g h f

The bundled transport is the unbundled one.

noncomputable def Representation.conjHomEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (h' : ∀ v ∈ τ, (ρ g⁻¹) v ∈ σ) : (↥τ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)) ≃ₗ[k] ↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)

The hom spaces out of two translates are k-linearly isomorphic. Translation by ρ g identifies the space of k[N]-linear maps out of τ with the space of k[N]-linear maps out of σ, with inverse the transport along translation by ρ g⁻¹.

@[simp]

theorem Representation.conjHomEquiv_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (h' : ∀ v ∈ τ, (ρ g⁻¹) v ∈ σ) (f : ↥τ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)) : (ρ.conjHomEquiv g h h') f = ρ.conjHom g h f

Evaluation of the transport isomorphism.

@[simp]

theorem Representation.conjHomEquiv_symm_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] {ρ : Representation k G V} {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (g : G) (h : ∀ v ∈ σ, (ρ g) v ∈ τ) (h' : ∀ v ∈ τ, (ρ g⁻¹) v ∈ σ) (f : ↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)) : (ρ.conjHomEquiv g h h').symm f = ρ.conjHom g⁻¹ h' f

The inverse of the transport isomorphism is the transport along translation by ρ g⁻¹.

@[simp]

theorem Representation.finrank_linearMap_conjSubrep {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : Module.finrank k (↥(TauCeti.Representation.conjSubrep ρ g σ).asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)) = Module.finrank k (↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype))

A translate has a hom space of the same dimension. The hom space out of conjSubrep ρ g σ and the hom space out of σ have the same dimension over k. No irreducibility, finiteness or algebraic closedness is involved: this is transport along translation. For an atom over a splitting field the dimension is the multiplicity of the constituent, and the statement then says that a translate occurs with the same multiplicity.

@[simp]

theorem Representation.finrank_asSubmodule_conjSubrep {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : Module.finrank k ↥(TauCeti.Representation.conjSubrep ρ g σ).asSubmodule = Module.finrank k ↥σ.asSubmodule

A translate has the same dimension. This is the k-linear content of TauCeti.Representation.conjSubrepEquiv, whose underlying map is again translation by ρ g.

theorem Representation.finrank_linearMap_eq_of_isAtom {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible] {σ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (hσ : IsAtom σ) (T : Submodule (MonoidAlgebra k ↥N) (asModule (MonoidHom.comp ρ N.subtype))) [IsSimpleModule (MonoidAlgebra k ↥N) ↥T] : Module.finrank k (↥T →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)) = Module.finrank k (↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype))

Clifford's theorem, multiplicity form. Every simple k[N]-submodule of the restriction of an irreducible representation has a hom space of the same dimension as that of a given minimal N-stable subspace; over a splitting field this says that the two constituents occur in the restriction with the same multiplicity. By the single-orbit theorem the submodule is isomorphic to a translate of the subspace, and a translate transports.

theorem Representation.finrank_linearMap_eq_of_isAtom_of_isAtom {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible] {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (hσ : IsAtom σ) (hτ : IsAtom τ) : Module.finrank k (↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)) = Module.finrank k (↥τ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype))

Clifford's theorem, multiplicity form, for two minimal subspaces. The hom spaces of any two minimal N-stable subspaces of an irreducible representation have the same dimension; over a splitting field this says that the two constituents occur in the restriction with the same multiplicity.

theorem Representation.finrank_asSubmodule_eq_of_isAtom_of_isAtom {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible] {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (hσ : IsAtom σ) (hτ : IsAtom τ) : Module.finrank k ↥σ.asSubmodule = Module.finrank k ↥τ.asSubmodule

The constituents all have the same dimension. The companion of the multiplicity statement: by the single-orbit theorem the minimal N-stable subspaces of an irreducible representation are translates of one another up to isomorphism, and translation is a k-linear isomorphism.

theorem Representation.finrank_linearMap_pos {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {N : Subgroup G} (ρ : Representation k G V) [FiniteDimensional k V] {σ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (hσ : σ ≠ ⊥) : 0 < Module.finrank k (↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype))

A nonzero N-subrepresentation has a positive-dimensional hom space. This is TauCeti.finrank_linearMap_pos_of_ne_bot read on the restriction; for an atom over a splitting field it says that the constituent occurs with positive multiplicity.

theorem Representation.exists_forall_finrank_linearMap_eq {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible] [FiniteDimensional k V] : ∃ (e : ℕ), 0 < e ∧ ∀ (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)), IsAtom σ → Module.finrank k (↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N] asModule (MonoidHom.comp ρ N.subtype)) = e

Clifford's theorem, the common multiplicity. For a finite-dimensional irreducible ρ there is a positive natural number e such that the hom space of every irreducible N-constituent of the restriction has dimension e. The restriction is semisimple (TauCeti.Representation.isSemisimpleRepresentation_comp_subtype), so over a splitting field this e is the e of the classical decomposition Res_N W ≅ e · ⨁ᵢ {}^{gᵢ} V.