Finite reflection invariants, degrees, and Weyl exponents

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremMolien's formula#

the image in K⟦X⟧ of the Hilbert series of the invariant subalgebra is the average over the group of the inverses of det(1 - t g | M), the reverse of the characteristic polynomial of ρ g: Hilb(Sym(M)^G, t) = #G⁻¹ ∑_{g ∈ G} det(1 - t g | M)⁻¹.

The field K is arbitrary, subject only to #G being invertible in it; in characteristic zero this determines the Hilbert series.

Representation.mk_finrank_symmetricAlgebraInvariants_inf_homogeneousSubmodule_eq_sum_inv_reverse_charpoly.{u_1,
    u_2, u_3}
  {K : Type u_1} {G : Type u_2} {M : Type u_3} [Field K] [Group G] [AddCommGroup M]
  [_root_.Module K M] [FiniteDimensional K M] (ρ : Representation K G M) [Fintype G]
  [Invertible ↑(Fintype.card G)] :
  (PowerSeries.mk fun n =>
      ↑(Module.finrank K
          ↥(Subalgebra.toSubmodule ρ.symmetricAlgebraInvariants ⊓
              TauCeti.SymmetricAlgebra.homogeneousSubmodule K M n))) =
    ⅟↑(Fintype.card G) • ∑ g, (↑(ρ g).charpoly.reverse)⁻¹
Lean

Formalized in Tau Ceti as Representation.mk_finrank_symmetricAlgebraInvariants_inf_homogeneousSubmodule_eq_sum_inv_reverse_charpoly.

Other forms

Molien's formula, trace form. Formalized in Tau Ceti as Representation.mk_finrank_symmetricAlgebraInvariants_inf_homogeneousSubmodule.

Representation.mk_finrank_symmetricAlgebraInvariants_inf_homogeneousSubmodule.{u_1, u_2, u_3}
  {K : Type u_1} {G : Type u_2} {M : Type u_3} [Field K] [Group G] [AddCommGroup M]
  [_root_.Module K M] [FiniteDimensional K M] (ρ : Representation K G M) [Fintype G]
  [Invertible ↑(Fintype.card G)] :
  (PowerSeries.mk fun n =>
      ↑(Module.finrank K
          ↥(Subalgebra.toSubmodule ρ.symmetricAlgebraInvariants ⊓
              TauCeti.SymmetricAlgebra.homogeneousSubmodule K M n))) =
    ⅟↑(Fintype.card G) •
      ∑ g,
        PowerSeries.mk fun n =>
          (LinearMap.trace K ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule K M n))
            (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ (ρ g) n)

Molien's formula, degreewise. Formalized in Tau Ceti as Representation.finrank_symmetricAlgebraInvariants_inf_homogeneousSubmodule.

Representation.finrank_symmetricAlgebraInvariants_inf_homogeneousSubmodule.{u_1, u_2, u_3}
  {K : Type u_1} {G : Type u_2} {M : Type u_3} [Field K] [Group G] [AddCommGroup M]
  [_root_.Module K M] [FiniteDimensional K M] (ρ : Representation K G M) [Fintype G]
  [Invertible ↑(Fintype.card G)] (n : ℕ) :
  ↑(Module.finrank K
        ↥(Subalgebra.toSubmodule ρ.symmetricAlgebraInvariants ⊓
            TauCeti.SymmetricAlgebra.homogeneousSubmodule K M n)) =
    ⅟↑(Fintype.card G) *
      ∑ g,
        (LinearMap.trace K ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule K M n))
          (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ (ρ g) n)
Sources
LeanRepresentation.mk_finrank_symmetricAlgebraInvariants_inf_homogeneousSubmodule_eq_sum_inv_reverse_charpoly · Representation.mk_finrank_symmetricAlgebraInvariants_inf_homogeneousSubmodule · Representation.finrank_symmetricAlgebraInvariants_inf_homogeneousSubmodule
Uses 2 · Used by 1
Statement usesRepresentation.symmetricAlgebraInvariants
Proof usesThe graded trace formula for an endomorphism of finite order
Used byThe converse of the Chevalley–Shephard–Todd theorem

TheoremNoether's finiteness theorem (TauCeti.FixedPoints.finiteType_subalgebra)#

Over a Noetherian base ring R, the invariants of a finite group acting on a finite-type R-algebra form a finite-type R-algebra.

TauCeti.FixedPoints.finiteType_subalgebra.{u_1, u_2, u_3} (R : Type u_1) (A : Type u_2)
  (G : Type u_3) [CommRing R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A]
  [SMulCommClass G R A] [IsNoetherianRing R] [Algebra.FiniteType R A] [Finite G] :
  Algebra.FiniteType R ↥(FixedPoints.subalgebra R A G)
Lean

Formalized in Tau Ceti as TauCeti.FixedPoints.finiteType_subalgebra.

Sources
LeanTauCeti.FixedPoints.finiteType_subalgebra
Used by 1
Used byNoether's finiteness theorem (Representation.finiteType_symmetricAlgebraInvariants)

TheoremNoether's degree bound#

If a family x, finite or not, generates a commutative algebra A over a ℚ-algebra R, then the invariants of a finite group G acting on A are generated by the orbit sums ∑_{g ∈ G} g • x^d of the monomials x^d of total degree at most |G|.

TauCeti.FixedPoints.subalgebra_eq_adjoin_sum_smul_prod_pow.{u_1, u_2, u_3, u_4} {R : Type u_1}
  {A : Type u_2} {G : Type u_3} [CommRing R] [Algebra ℚ R] [CommRing A] [Algebra R A] [Fintype G]
  {ι : Type u_4} [Group G] [MulSemiringAction G A] [SMulCommClass G R A] (x : ι → A)
  (hx : Algebra.adjoin R (Set.range x) = ⊤) :
  FixedPoints.subalgebra R A G =
    Algebra.adjoin R
      ((fun d => ∑ g, g • d.prod fun i n => x i ^ n) '' {d | Finsupp.degree d ≤ Fintype.card G})
Lean

Formalized in Tau Ceti as TauCeti.FixedPoints.subalgebra_eq_adjoin_sum_smul_prod_pow.

Sources
LeanTauCeti.FixedPoints.subalgebra_eq_adjoin_sum_smul_prod_pow
Uses 1 · Used by 1
Proof usesNewton's identities for a multiset
Used byThe homogeneous Noether bound

TheoremInvariant polynomials detect orbits#

Two vectors have the same value on every invariant polynomial function exactly when they lie in the same orbit.

Representation.forall_mem_symmetricAlgebraInvariants_lift_eval_eq_iff.{u_1, u_2, u_3} {K : Type u_1}
  {G : Type u_2} {V : Type u_3} [Field K] [Group G] [Finite G] [AddCommGroup V] [_root_.Module K V]
  (ρ : Representation K G V) {v w : V} :
  (∀ p ∈ ρ.dual.symmetricAlgebraInvariants,
      (SymmetricAlgebra.lift ((Module.Dual.eval K V) v)) p =
        (SymmetricAlgebra.lift ((Module.Dual.eval K V) w)) p) ↔
    ∃ g, (ρ g) v = w
Lean

Formalized in Tau Ceti as Representation.forall_mem_symmetricAlgebraInvariants_lift_eval_eq_iff.

Sources
LeanRepresentation.forall_mem_symmetricAlgebraInvariants_lift_eval_eq_iff
Uses 1 · Used by 1
Statement usesRepresentation.symmetricAlgebraInvariants
Used byThe fibre over the vertex is the origin

TheoremThe fibre over the vertex is the origin#

Every homogeneous invariant polynomial function of positive degree vanishes at v exactly when v = 0.

Representation.forall_homogeneous_mem_symmetricAlgebraInvariants_lift_eval_eq_zero_iff.{u_1, u_2,
    u_3}
  {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [Finite G] [AddCommGroup V]
  [_root_.Module K V] (ρ : Representation K G V) {v : V} :
  (∀ (n : ℕ),
      0 < n →
        ∀ p ∈ ρ.dual.symmetricAlgebraInvariants,
          p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K (Module.Dual K V) n →
            (SymmetricAlgebra.lift ((Module.Dual.eval K V) v)) p = 0) ↔
    v = 0
Lean

Formalized in Tau Ceti as Representation.forall_homogeneous_mem_symmetricAlgebraInvariants_lift_eval_eq_zero_iff.

Sources
LeanRepresentation.forall_homogeneous_mem_symmetricAlgebraInvariants_lift_eval_eq_zero_iff
Uses 2
Statement usesRepresentation.symmetricAlgebraInvariants
Proof usesInvariant polynomials detect orbits

TheoremRepresentation.radical_symmetricAlgebraHilbertIdeal_of_isReduced#

For a finite group over a reduced base, the radical of the Hilbert ideal is the irrelevant ideal.

Representation.radical_symmetricAlgebraHilbertIdeal_of_isReduced.{u_1, u_2, u_3} {R : Type u_1}
  {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [Finite G] [AddCommMonoid M]
  [_root_.Module R M] (ρ : Representation R G M) [IsReduced R] :
  ρ.symmetricAlgebraHilbertIdeal.radical =
    (HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)).toIdeal
Lean

Formalized in Tau Ceti as Representation.radical_symmetricAlgebraHilbertIdeal_of_isReduced.

Sources
LeanRepresentation.radical_symmetricAlgebraHilbertIdeal_of_isReduced
Uses 1
Statement usesRepresentation.symmetricAlgebraInvariants

TheoremFiniteness of the coinvariant algebra#

For a finite group acting on a finitely generated module, the coinvariant algebra Sym M ⧸ A₊ · Sym M is a finite R-module: it is of finite type, and generated by nilpotent, hence integral, elements.

Representation.moduleFinite_quotient_symmetricAlgebraHilbertIdeal.{u_1, u_2, u_3} {R : Type u_1}
  {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [Finite G] [AddCommMonoid M]
  [_root_.Module R M] (ρ : Representation R G M) [Module.Finite R M] :
  Module.Finite R (SymmetricAlgebra R M ⧸ ρ.symmetricAlgebraHilbertIdeal)
Lean

Formalized in Tau Ceti as Representation.moduleFinite_quotient_symmetricAlgebraHilbertIdeal.

Sources
LeanRepresentation.moduleFinite_quotient_symmetricAlgebraHilbertIdeal
Uses 1 · Used by 1
Statement usesRepresentation.symmetricAlgebraInvariants
Used byChevalley's theorem: the coinvariant algebra of a reflection group is the regular representation

DefinitionRepresentation.symmetricAlgebraInvariants#

The invariant subalgebra Sym(M)^G: the elements of Sym M fixed by the induced action of every element of G, that is, the fixed subalgebra FixedPoints.subalgebra of the bundled action.

Representation.symmetricAlgebraInvariants.{u_1, u_2, u_3} {R : Type u_1} {G : Type u_2}
  {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [_root_.Module R M]
  (ρ : Representation R G M) : Subalgebra R (SymmetricAlgebra R M)
Lean

Formalized in Tau Ceti as Representation.symmetricAlgebraInvariants.

Sources
LeanRepresentation.symmetricAlgebraInvariants
Used by 14
Used byChevalley's restriction theorem, image form · Harish-Chandra surjectivity with a degree bound · Finiteness of the coinvariant algebra · Invariant polynomials detect orbits · Molien's formula · Representation.radical_symmetricAlgebraHilbertIdeal_of_isReduced · Representation.symmetricAlgebraReynolds · The fibre over the vertex is the origin · Chevalley's theorem: the coinvariant algebra of a reflection group is the regular representation · Graded Nakayama lemma for polynomial invariants · Noether's finiteness theorem (Representation.finiteType_symmetricAlgebraInvariants) · The Chevalley–Shephard–Todd theorem · The converse of the Chevalley–Shephard–Todd theorem · The homogeneous Noether bound

DefinitionRepresentation.symmetricAlgebraReynolds#

The Reynolds operator p ↦ #G⁻¹ • ∑ g, g • p, from Sym M onto the invariant subalgebra. It is linear over the invariant subalgebra and restricts to the identity on it, but it is generally not multiplicative.

Representation.symmetricAlgebraReynolds.{u_1, u_2, u_3} {R : Type u_1} {G : Type u_2} {M : Type u_3}
  [CommRing R] [Group G] [AddCommMonoid M] [_root_.Module R M] (ρ : Representation R G M)
  [Fintype G] [Invertible ↑(Fintype.card G)] :
  SymmetricAlgebra R M →ₗ[↥ρ.symmetricAlgebraInvariants] ↥ρ.symmetricAlgebraInvariants
Lean

Formalized in Tau Ceti as Representation.symmetricAlgebraReynolds.

Sources
LeanRepresentation.symmetricAlgebraReynolds
Uses 1 · Used by 2
Statement usesRepresentation.symmetricAlgebraInvariants
Used byChevalley's restriction theorem, image form · Harish-Chandra surjectivity with a degree bound

TheoremThe graded trace formula for an endomorphism of finite order#

The graded trace formula for an endomorphism of finite order of a finite-dimensional vector space over an arbitrary field: if f ^ n = 1 with n nonzero in K, then (∑ₘ tr(f | Symᵐ V) tᵐ) * det(1 - t f) = 1.

No eigenvalue of f need lie in K: over an algebraic closure f becomes diagonalizable, and both factors commute with scalar extension (Module.End.trace_homogeneousSubmoduleMapₛₗ_baseChange, LinearMap.charpoly_baseChange).

Module.End.mk_trace_homogeneousSubmoduleMapₛₗ_mul_reverse_charpoly_of_pow_eq_one.{u_1, u_2}
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [_root_.Module K V]
  [FiniteDimensional K V] {f : Module.End K V} {n : ℕ} (hn : ↑n ≠ 0) (hf : f ^ n = 1) :
  (PowerSeries.mk fun m =>
        (LinearMap.trace K ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule K V m))
          (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ f m)) *
      ↑(LinearMap.charpoly f).reverse =
    1
Lean

Formalized in Tau Ceti as Module.End.mk_trace_homogeneousSubmoduleMapₛₗ_mul_reverse_charpoly_of_pow_eq_one.

Sources
LeanModule.End.mk_trace_homogeneousSubmoduleMapₛₗ_mul_reverse_charpoly_of_pow_eq_one
Used by 1
Used byMolien's formula

DefinitionSymmetricAlgebra.dividedDifference#

The divided-difference operator p ↦ (p - σ p) / ℓ on the symmetric algebra, for a linear endomorphism σ of M such that m - σ m is a multiple of ℓ for every m, and an element ℓ that is a nonzerodivisor in Sym M. It is characterized by ι ℓ * dividedDifference σ ℓ hσ hℓ p = p - σ p (SymmetricAlgebra.dividedDifference_eq_iff).

SymmetricAlgebra.dividedDifference.{u_1, u_2} {R : Type u_1} {M : Type u_2} [CommRing R]
  [AddCommGroup M] [_root_.Module R M] (σ : M →ₗ[R] M) (ℓ : M) (hσ : ∀ (m : M), m - σ m ∈ R ∙ ℓ)
  (hℓ : IsLeftRegular ((SymmetricAlgebra.ι R M) ℓ)) :
  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M
Lean

Formalized in Tau Ceti as SymmetricAlgebra.dividedDifference.

Sources
LeanSymmetricAlgebra.dividedDifference
Used by 2
Used byChevalley's theorem: the coinvariant algebra of a reflection group is the regular representation · The Chevalley–Shephard–Todd theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.