The inertia group of a representation of a normal subgroup

Let N be a normal subgroup of G. Conjugation makes G act on FDRep k N (TauCeti.conjNormalFDRepMulAction), and the inertia group of A : FDRep k N is the stabilizer of the isomorphism class of A,

inertia A = {g : G | {}^g A ≅ A}.

This is not MulAction.stabilizer G A, which asks for {}^g A = A on the nose; the two are compared in TauCeti.stabilizer_le_inertia. Instead, isomorphism classes of objects of a category are Mathlib's CategoryTheory.Skeleton, and conjugation descends to them because it is a functor; that descent is the MulAction instance TauCeti.conjNormalFDRepSkeletonMulAction of the conjugation file, and inertia A is literally MulAction.stabilizer G (toSkeleton A). Everything else — that the inertia group is a subgroup, that it only depends on the isomorphism class, and that conjugating the representation conjugates it — is then Mathlib's generic stabilizer API.

The inertia group contains N (TauCeti.le_inertia), because conjugating by an element n of N itself is an inner twist: A.ρ n intertwines {}^n A with A (TauCeti.conjNormalFDRepIso). Together with the normality of N inside inertia A, which Mathlib's Subgroup.normal_subgroupOf instance supplies for any subgroup of G, this is what makes the quotient inertia A / N — where the Clifford-theory obstruction lives — available.

The inertia group and its basic properties need no irreducibility hypothesis. Irreducibility enters only in Representation.IntertwiningMap.mem_inertia, where Schur's lemma turns a nonzero intertwiner into an isomorphism, and later when Clifford's theorem identifies the constituents of a restriction with a single G-orbit.

Main definitions

• TauCeti.inertia: the inertia group of a representation of a normal subgroup.

Main statements

• TauCeti.mem_inertia_iff: membership in the inertia group is the existence of an isomorphism {}^g A ≅ A.
• TauCeti.mem_inertia_iff_exists_linearEquiv: equivalently, conjugation by g on N is implemented by an invertible operator on A.
• Representation.IntertwiningMap.mem_inertia: a nonzero intertwiner from an irreducible representation to one of its conjugates puts the conjugating element in the inertia group.
• Representation.IntertwiningMap.inv_mem_inertia_of_comp_ne_zero: if an intertwiner from V followed by one from a conjugate back to V is nonzero, the inverse conjugator is in the inertia group.
• TauCeti.le_inertia: the inertia group contains N.
• TauCeti.inertia_congr: isomorphic representations have the same inertia group, so the inertia group is an invariant of the isomorphism class.
• TauCeti.inertia_conjNormalFDRep: conjugating the representation conjugates its inertia group.
• TauCeti.char_conj_eq_of_mem_inertia: the character of A is invariant under conjugation by an element of the inertia group.

References

This file builds the inertia group of Layer 5 (Clifford theory over a normal subgroup) of TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md, which asks for "the inertia (stabilizer) group inertia V ≤ G of an irreducible V : FDRep k N is {g : G | {}^g V ≅ V}, a subgroup containing N", and pins inertia, mem_inertia_iff and le_inertia in the accompanying Suggested.lean.

noncomputable def TauCeti.inertia {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (A : FDRep k ↥N) : Subgroup G

The inertia group of A : FDRep k N, for N a normal subgroup of G: the elements of G whose conjugate representation {}^g A is isomorphic to A, i.e. the stabilizer of the isomorphism class of A under conjNormalFDRepSkeletonMulAction.

See TauCeti.mem_inertia_iff for the description as {g | {}^g A ≅ A}, and TauCeti.stabilizer_le_inertia for the comparison with the stabilizer of A itself.

Equations

• TauCeti.inertia A = MulAction.stabilizer G (CategoryTheory.toSkeleton A)

@[simp]

theorem TauCeti.mem_inertia_iff {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] {A : FDRep k ↥N} {g : G} : g ∈ inertia A ↔ Nonempty (conjNormalFDRep g A ≅ A)

An element lies in the inertia group exactly when it conjugates the representation to an isomorphic one.

theorem TauCeti.stabilizer_le_inertia {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (A : FDRep k ↥N) : MulAction.stabilizer G A ≤ inertia A

The inertia group of A contains the elements fixing A on the nose.

theorem TauCeti.le_inertia {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (A : FDRep k ↥N) : N ≤ inertia A

The inertia group contains the normal subgroup: conjugating by an element of N is an inner twist, so it fixes the isomorphism class.

theorem TauCeti.inertia_congr {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] {A B : FDRep k ↥N} (e : A ≅ B) : inertia A = inertia B

Isomorphic representations have the same inertia group: the inertia group depends only on the isomorphism class of A, which — once A is irreducible — is a point of Irr(N).

theorem TauCeti.inertia_conjNormalFDRep {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (g : G) (A : FDRep k ↥N) : inertia (conjNormalFDRep g A) = MulAut.conj g • inertia A

Conjugating the representation conjugates the inertia group: I({}^g A) = g I(A) g⁻¹.

Equivalently the inertia groups along a G-orbit in Irr(N) are all conjugate, so they share an index; that index is the number of constituents in Clifford's theorem.

theorem TauCeti.char_conj_eq_of_mem_inertia {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Field k] {A : FDRep k ↥N} {g : G} (hg : g ∈ inertia A) (x : ↥N) : A.character ⟨g⁻¹ * ↑x * g, ⋯⟩ = A.character x

The character of A is invariant under conjugation by an element of its inertia group: χ(g⁻¹xg) = χ(x) for g ∈ inertia A and x : N.

This is the character shadow of mem_inertia_iff, and the form in which Clifford's theorem uses the inertia group.

theorem TauCeti.mem_inertia_iff_exists_linearEquiv {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Field k] {A : FDRep k ↥N} {g : G} : g ∈ inertia A ↔ ∃ (a : ↑A.V ≃ₗ[k] ↑A.V), ∀ (n : ↥N) (x : ↑A.V), a ((A.ρ n) x) = (A.ρ ((MulAut.conjNormal g) n)) (a x)

Membership in the inertia group, read on operators: g ∈ inertia A exactly when conjugation by g on N is implemented by an invertible operator a on A, that is, a ∘ A.ρ n = A.ρ (g n g⁻¹) ∘ a for all n : N. Such an a is an isomorphism {}^g A ≅ A read on the common underlying space.

theorem Representation.IntertwiningMap.mem_inertia {k : Type u_1} {G : Type u_2} [Field k] [Group G] {N : Subgroup G} [N.Normal] {V : FDRep k ↥N} [CategoryTheory.Simple V] {g : G} (q : IntertwiningMap V.ρ (TauCeti.conjNormalFDRep g V).ρ) (hq : q ≠ 0) : g ∈ TauCeti.inertia V

A nonzero intertwiner into a conjugate puts the conjugating element in the inertia group. If V is irreducible and some intertwiner from V to {}^g V is nonzero, then Schur's lemma makes it an isomorphism, so g ∈ inertia V.

theorem Representation.IntertwiningMap.inv_mem_inertia_of_comp_ne_zero {k : Type u_1} {G : Type u_2} [Field k] [Group G] {N : Subgroup G} [N.Normal] {V : FDRep k ↥N} [CategoryTheory.Simple V] {W : Type u_3} [AddCommMonoid W] [Module k W] {σ : Representation k (↥N) W} {s : G} (p : IntertwiningMap (MonoidHom.comp σ (MulEquiv.toMonoidHom (MulAut.conjNormal s⁻¹))) V.ρ) (g : IntertwiningMap V.ρ σ) (hpg : p.toLinearMap ∘ₗ g.toLinearMap ≠ 0) : s⁻¹ ∈ TauCeti.inertia V

If an intertwiner g : V → σ followed by an intertwiner p from the conjugate of σ by s⁻¹ back to V is nonzero, then the composite is a nonzero intertwiner V → {}^{s⁻¹} V, so s⁻¹ lies in the inertia group TauCeti.inertia V of V.