Inertia groups of codimension-one primes of a symmetric algebra

Let ρ be a representation of a group G on a module M, acting on the symmetric algebra Sym M by Representation.symmetricAlgebraMulSemiringAction. The inertia group P.inertia G of an ideal P of Sym M is the subgroup of elements acting trivially modulo P (Mathlib's Ideal.inertia). Since Sym M is generated by M, an element lies in it exactly when it moves every vector by an element of P. For the prime ideal spanned by a degree-one element ι ℓ, this says that g moves every vector by a multiple of ℓ.

Over a field K, these are the only height-one primes whose inertia group acts nontrivially on M: if g acts nontrivially and lies in the inertia group of a height-one prime P, then P contains the nonzero degree-one element ι (ρ g m - m) for some m, which is prime, so P is spanned by it. Conversely, for finite-dimensional M each nonzero ι ℓ spans a prime of height one (SymmetricAlgebra.height_span_singleton_ι). If moreover G is finite of order invertible in K and ρ is faithful, the inertia group of ι ℓ acts on the line K ∙ ℓ through an injective character, so it is cyclic.

For polynomial functions on a vector space V, take M = V* with the contragredient action ρ.dual. A nonzero linear form ℓ spans the ideal of the hyperplane ker ℓ, and the inertia group of that ideal is the pointwise stabilizer of ker ℓ. Thus a height-one prime of Sym(V*) whose inertia group acts nontrivially on V is the ideal of a hyperplane ker ℓ, its inertia group is the pointwise stabilizer of ker ℓ, and each element of it acting nontrivially on V is a pseudoreflection whose fixed hyperplane is exactly ker ℓ. If moreover G is finite of order invertible in K and acts faithfully, these inertia groups are cyclic.

Consequently the inertia group of every height-one prime of Sym(V*) lies in the subgroup generated by the pseudoreflections together with the kernel of ρ. When ρ is faithful it lies in the subgroup H generated by the pseudoreflections alone (Representation.pseudoreflectionSubgroup, in TauCeti.RepresentationTheory.Pseudoreflection). Let G be finite and V finite-dimensional, and let ρ be faithful. The normal subgroup H gives the factorization V → V/H → V/G of the quotient map, and G ⧸ H acts on the invariants Sym(V*)^H with invariants Sym(V*)^G. Every height-one prime P of Sym(V*)^H lies under a height-one prime Q of Sym(V*), since Sym(V*) is integral over the finitely generated algebra Sym(V*)^H and contraction preserves heights. The inertia group of P in G ⧸ H is the image of the inertia group of Q in G (Ideal.inertia_quotient_eq_bot_iff), so it is trivial. Thus the residual quotient V/H → V/G has trivial inertia at every codimension-one point.

Main results

• Representation.symmetricAlgebra_mem_inertia_iff: g lies in the inertia group of P exactly when ι (ρ g m - m) ∈ P for every m.
• Representation.symmetricAlgebra_mem_inertia_span_singleton_ι_iff: the inertia group of ι ℓ consists of the elements moving every vector by a multiple of ℓ.
• Representation.exists_eq_span_singleton_ι_of_mem_inertia: a height-one prime whose inertia group acts nontrivially is spanned by a nonzero degree-one element.
• Representation.isCyclic_inertia_span_singleton_ι and Representation.isCyclic_inertia_of_height_eq_one: for a faithful representation of a finite group of order invertible in K, these inertia groups are cyclic.
• Representation.mem_dual_inertia_span_singleton_ι_iff_le_fixedSubmodule: for polynomial functions on V, the inertia group of the ideal of ker ℓ is its pointwise stabilizer.
• Representation.exists_eq_span_singleton_ι_and_ker_eq_of_mem_inertia: an element of the inertia group of a height-one prime of Sym(V*) acting nontrivially on V is a pseudoreflection, whose fixed hyperplane cuts out that prime.
• Representation.inertia_le_pseudoreflectionSubgroup_sup_ker and Representation.inertia_le_pseudoreflectionSubgroup: the inertia group of a height-one prime of Sym(V*) lies in the pseudoreflection subgroup, together with the kernel of ρ in general.
• Representation.inertia_quotient_pseudoreflectionSubgroup_eq_bot: for a faithful representation of a finite group, G ⧸ H has trivial inertia at every height-one prime of Sym(V*)^H.

References

• R. Kane, Reflection Groups and Invariant Theory, CMS Books in Mathematics, Springer (2001), § 18.
• L. Smith, Polynomial Invariants of Finite Groups, A K Peters (1995), § 7.4.

theorem Representation.symmetricAlgebra_mem_inertia_iff {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommGroup M] [Module R M] {ρ : Representation R G M} {P : Ideal (SymmetricAlgebra R M)} {g : G} : g ∈ Ideal.inertia G P ↔ ∀ (m : M), (SymmetricAlgebra.ι R M) ((ρ g) m - m) ∈ P

An element g lies in the inertia group of an ideal P of Sym M for the induced action exactly when it moves every degree-one element by an element of P.

theorem Representation.symmetricAlgebra_mem_inertia_span_singleton_ι_iff {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommGroup M] [Module R M] {ρ : Representation R G M} {ℓ : M} {g : G} : g ∈ Ideal.inertia G (Ideal.span {(SymmetricAlgebra.ι R M) ℓ}) ↔ ∀ (m : M), m - (ρ g) m ∈ R ∙ ℓ

An element g lies in the inertia group of the ideal spanned by a degree-one element ι ℓ exactly when it moves every vector by a multiple of ℓ.

theorem Representation.exists_eq_span_singleton_ι_of_mem_inertia {K : Type u_1} {G : Type u_2} {M : Type u_3} [Field K] [Group G] [AddCommGroup M] [Module K M] (ρ : Representation K G M) {P : Ideal (SymmetricAlgebra K M)} [P.IsPrime] (hP : P.height = 1) {g : G} (hg : g ∈ Ideal.inertia G P) (hρg : ρ g ≠ 1) : ∃ (ℓ : M), ℓ ≠ 0 ∧ P = Ideal.span {(SymmetricAlgebra.ι K M) ℓ}

If an element g acting nontrivially on M lies in the inertia group of a height-one prime P of Sym M, then P is spanned by a nonzero degree-one element.

theorem Representation.isCyclic_inertia_span_singleton_ι {K : Type u_1} {G : Type u_2} {M : Type u_3} [Field K] [Group G] [AddCommGroup M] [Module K M] (ρ : Representation K G M) [Finite G] (hG : ↑(Nat.card G) ≠ 0) (hρ : Function.Injective ⇑ρ) {ℓ : M} (hℓ : ℓ ≠ 0) : IsCyclic ↥(Ideal.inertia G (Ideal.span {(SymmetricAlgebra.ι K M) ℓ}))

For a faithful representation of a finite group whose order is invertible in K, the inertia group of the ideal spanned by a nonzero degree-one element ι ℓ is cyclic: it acts on the line K ∙ ℓ through an injective character.

theorem Representation.isCyclic_inertia_of_height_eq_one {K : Type u_1} {G : Type u_2} {M : Type u_3} [Field K] [Group G] [AddCommGroup M] [Module K M] (ρ : Representation K G M) [Finite G] (hG : ↑(Nat.card G) ≠ 0) (hρ : Function.Injective ⇑ρ) {P : Ideal (SymmetricAlgebra K M)} [P.IsPrime] (hP : P.height = 1) : IsCyclic ↥(Ideal.inertia G P)

For a faithful representation of a finite group whose order is invertible in K, the inertia group of every height-one prime of Sym M is cyclic.

theorem Representation.mem_dual_inertia_span_singleton_ι_iff_le_fixedSubmodule {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) {ℓ : Module.Dual K V} {g : G} : g ∈ Ideal.inertia G (Ideal.span {(SymmetricAlgebra.ι K (Module.Dual K V)) ℓ}) ↔ LinearMap.ker ℓ ≤ (ρ g).fixedSubmodule

For polynomial functions on V, the inertia group of the ideal spanned by a linear form ℓ is the pointwise stabilizer of the hyperplane ker ℓ.

theorem Representation.exists_eq_span_singleton_ι_and_ker_eq_of_mem_inertia {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) {P : Ideal (SymmetricAlgebra K (Module.Dual K V))} [P.IsPrime] (hP : P.height = 1) {g : G} (hg : g ∈ Ideal.inertia G P) (hρg : ρ g ≠ 1) : ∃ (ℓ : Module.Dual K V), ℓ ≠ 0 ∧ P = Ideal.span {(SymmetricAlgebra.ι K (Module.Dual K V)) ℓ} ∧ (ρ g - 1).ker = LinearMap.ker ℓ

Let P be a height-one prime of the polynomial functions Sym(V*) on V, and let g lie in its inertia group and act nontrivially on V. Then P is spanned by a nonzero linear form ℓ, and g is a pseudoreflection fixing exactly the hyperplane ker ℓ.

theorem Representation.inertia_le_pseudoreflectionSubgroup_sup_ker {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) {P : Ideal (SymmetricAlgebra K (Module.Dual K V))} [P.IsPrime] (hP : P.height = 1) : Ideal.inertia G P ≤ ρ.pseudoreflectionSubgroup ⊔ MonoidHom.ker ρ

The inertia group of a height-one prime of the polynomial functions Sym(V*) lies in the subgroup generated by the pseudoreflections of ρ and the kernel of ρ: each of its elements either acts trivially on V or is a pseudoreflection.

theorem Representation.inertia_le_pseudoreflectionSubgroup {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) (hρ : Function.Injective ⇑ρ) {P : Ideal (SymmetricAlgebra K (Module.Dual K V))} [P.IsPrime] (hP : P.height = 1) : Ideal.inertia G P ≤ ρ.pseudoreflectionSubgroup

For a faithful representation, the inertia group of a height-one prime of the polynomial functions Sym(V*) lies in the subgroup generated by the pseudoreflections.

theorem Representation.inertia_quotient_pseudoreflectionSubgroup_eq_bot {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) [Finite G] [FiniteDimensional K V] (hρ : Function.Injective ⇑ρ) (P : Ideal ↥(FixedPoints.subalgebra K (SymmetricAlgebra K (Module.Dual K V)) ↥ρ.pseudoreflectionSubgroup)) [P.IsPrime] (hP : P.height = 1) : Ideal.inertia (G ⧸ ρ.pseudoreflectionSubgroup) P = ⊥

The residual quotient has trivial inertia in codimension one. Let ρ be a faithful representation of a finite group G on a finite-dimensional space V, and let H be its pseudoreflection subgroup. Then G ⧸ H acts on the polynomial invariants Sym(V*)^H, and the inertia group of every height-one prime of Sym(V*)^H for this action is trivial. Geometrically, the residual quotient V/H → V/G by G ⧸ H has trivial inertia at every codimension-one point.