Inertia cosets index the constituents in Clifford's theorem

This file identifies the orbit of an irreducible constituent in Clifford's theorem with the left cosets of its inertia group. Concretely, if σ is a minimal subrepresentation of the restriction of an irreducible finite-dimensional representation ρ from G to a normal subgroup N, then the isotypic components of the restriction are indexed by

G ⧸ inertia (FDRep.of σ.toRepresentation).

The construction combines the single-orbit theorem from TauCeti/RepresentationTheory/Induction/Clifford/Orbit/Basic.lean with Mathlib's generic MulAction.orbitEquivQuotientStabilizer. It uses two dictionary bridges: translating σ inside ρ represents the conjugate abstract N-representation carried by σ, and the module of a subrepresentation is canonically equivalent to its associated k[N]-submodule.

Main definitions

• Representation.fdRepIsoConjSubrep: the finite-dimensional representation carried by a translated constituent is isomorphic to the conjugate representation.
• Representation.isotypicComponentsEquivQuotientInertia: the equivalence between the isotypic components of the restriction and the inertia cosets.

The indexed component Representation.conjSubrepIsotypicComponent is defined in Orbit/Basic.lean.

Main results

• Representation.toSkeleton_fdRepOf_conjSubrep: translating a constituent inside ρ and conjugating the abstract N-representation it carries agree on isomorphism classes.
• Representation.mem_inertia_fdRepOf_toRepresentation_iff: a group element lies in the inertia group of a constituent exactly when its translate carries an equivalent k[N]-submodule.
• Representation.isotypicComponentsEquivQuotientInertia_conjSubrepIsotypicComponent: under the equivalence, the component of the translate by g corresponds to the coset of g.
• Representation.isotypicComponentsEquivQuotientInertia_symm_mk: the inverse computation.
• Representation.conjSubrepIsotypicComponent_eq_iff: two translates determine the same component exactly when their quotient lies in the inertia group.
• Representation.card_isotypicComponents_eq_inertia_index: the number of irreducible constituent classes is the index of the inertia group.

Implementation notes

Isotypic components are handled through TauCeti.simpleSubmoduleClassesEquiv, rather than by choosing a simple representative. Isomorphism of subrepresentations is expressed as a k[N]-linear equivalence of their associated submodules; the general bridge to equality in Skeleton (FDRep k N) is TauCeti.toSkeleton_fdRepOf_toRepresentation_eq_iff.

References

This is the orbit-indexing step in Clifford's theorem from Layer 5 of TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md. It prepares the remaining packaged decomposition of the restriction as equal-multiplicity copies of the conjugates indexed by an inertia-group transversal.

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

noncomputable def Representation.fdRepIsoConjSubrep {k : Type u} {G : Type v} [Field k] [Group G] {V : Type u} [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [FiniteDimensional k V] (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : FDRep.of (TauCeti.Representation.conjSubrep ρ g σ).toRepresentation ≅ TauCeti.conjNormalFDRep g (FDRep.of σ.toRepresentation)

A translated constituent carries the conjugate finite-dimensional representation.

theorem Representation.toSkeleton_fdRepOf_conjSubrep {k : Type u} {G : Type v} [Field k] [Group G] {V : Type u} [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [FiniteDimensional k V] (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : CategoryTheory.toSkeleton (FDRep.of (TauCeti.Representation.conjSubrep ρ g σ).toRepresentation) = g • CategoryTheory.toSkeleton (FDRep.of σ.toRepresentation)

Translating a constituent inside the ambient representation agrees, on isomorphism classes, with conjugating the finite-dimensional representation carried by that constituent.

theorem Representation.mem_inertia_fdRepOf_toRepresentation_iff {k : Type u} {G : Type v} [Field k] [Group G] {V : Type u} [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [FiniteDimensional k V] (g : G) (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) : g ∈ TauCeti.inertia (FDRep.of σ.toRepresentation) ↔ Nonempty (↥(TauCeti.Representation.conjSubrep ρ g σ).asSubmodule ≃ₗ[MonoidAlgebra k ↥N] ↥σ.asSubmodule)

Membership in a constituent's inertia group is equivalence of the translated and original associated submodules.

noncomputable def Representation.isotypicComponentsEquivQuotientInertia {k : Type u} {G : Type v} [Field k] [Group G] {V : Type u} [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [FiniteDimensional k V] [ρ.IsIrreducible] (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) (hσ : IsAtom σ) : ↑(isotypicComponents (MonoidAlgebra k ↥N) (asModule (MonoidHom.comp ρ N.subtype))) ≃ G ⧸ TauCeti.inertia (FDRep.of σ.toRepresentation)

The inertia cosets index the isotypic components in Clifford's theorem. A component is sent to the coset of any g whose translated constituent cuts out that component, and generic orbit--stabilizer identifies this with the left cosets of the constituent's inertia group.

@[simp]

theorem Representation.isotypicComponentsEquivQuotientInertia_conjSubrepIsotypicComponent {k : Type u} {G : Type v} [Field k] [Group G] {V : Type u} [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [FiniteDimensional k V] [ρ.IsIrreducible] (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) (hσ : IsAtom σ) (g : G) : (ρ.isotypicComponentsEquivQuotientInertia σ hσ) (ρ.conjSubrepIsotypicComponent σ hσ g) = ↑g

Under the Clifford orbit equivalence, the component of the translate by g corresponds to the coset of g.

@[simp]

theorem Representation.isotypicComponentsEquivQuotientInertia_symm_mk {k : Type u} {G : Type v} [Field k] [Group G] {V : Type u} [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [FiniteDimensional k V] [ρ.IsIrreducible] (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) (hσ : IsAtom σ) (g : G) : (ρ.isotypicComponentsEquivQuotientInertia σ hσ).symm ↑g = ρ.conjSubrepIsotypicComponent σ hσ g

The coset of g is sent back to the component cut out by the translate by g.

@[simp]

theorem Representation.conjSubrepIsotypicComponent_eq_iff {k : Type u} {G : Type v} [Field k] [Group G] {V : Type u} [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [FiniteDimensional k V] [ρ.IsIrreducible] (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) (hσ : IsAtom σ) (g h : G) : ρ.conjSubrepIsotypicComponent σ hσ g = ρ.conjSubrepIsotypicComponent σ hσ h ↔ g⁻¹ * h ∈ TauCeti.inertia (FDRep.of σ.toRepresentation)

Two translates cut out the same isotypic component exactly when they determine the same inertia coset.

theorem Representation.card_isotypicComponents_eq_inertia_index {k : Type u} {G : Type v} [Field k] [Group G] {V : Type u} [AddCommGroup V] [Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [FiniteDimensional k V] [ρ.IsIrreducible] (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)) (hσ : IsAtom σ) : Nat.card ↑(isotypicComponents (MonoidAlgebra k ↥N) (asModule (MonoidHom.comp ρ N.subtype))) = (TauCeti.inertia (FDRep.of σ.toRepresentation)).index

The number of constituent classes is the inertia index. This is the numerical orbit--stabilizer statement underlying the number of summands in Clifford's decomposition.