Symmetric Algebra

Results named in Tau Ceti's TauCeti.RepresentationTheory.SymmetricAlgebra modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremChevalley's theorem: the coinvariant algebra of a reflection group is the regular representation#

If a finite group G acts faithfully on a finite-dimensional vector space V over a field of characteristic zero and is generated by pseudoreflections, then the coinvariant algebra of the polynomial functions Sym(V*), as an ungraded representation, is equivalent to the regular representation K[G].

Representation.nonempty_equiv_coinvariantAlgebra_dual_leftRegular_of_pseudoreflectionSubgroup_eq_top.{u_1,
    u_2, u_3}
  {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V]
  [_root_.Module K V] [FiniteDimensional K V] (ρ : Representation K G V) [Finite G] [CharZero K]
  (hG : ρ.pseudoreflectionSubgroup = ⊤) (hρ : Function.Injective ⇑ρ) :
  Nonempty (ρ.dual.coinvariantAlgebra.Equiv (Representation.leftRegular K G))
Lean

Formalized in Tau Ceti as Representation.nonempty_equiv_coinvariantAlgebra_dual_leftRegular_of_pseudoreflectionSubgroup_eq_top.

Sources
LeanRepresentation.nonempty_equiv_coinvariantAlgebra_dual_leftRegular_of_pseudoreflectionSubgroup_eq_top
Uses 5
Statement usesRepresentation.symmetricAlgebraInvariants
Proof usesFiniteness of the coinvariant algebra · Graded Nakayama lemma for polynomial invariants · Noether's finiteness theorem (Representation.finiteType_symmetricAlgebraInvariants) · SymmetricAlgebra.dividedDifference

TheoremThe Chevalley–Shephard–Todd theorem#

Let a finite group G, whose order is invertible in the field K, act linearly on a finite-dimensional vector space V, and suppose that G is generated by pseudoreflections, the elements whose fixed space is a hyperplane. Then the polynomial invariants Sym(V*)^G form a polynomial algebra on dim V homogeneous invariants f₁, …, fₙ of positive degree: K[X₁, …, Xₙ] → Sym(V*)^G, Xᵢ ↦ fᵢ, is an isomorphism.

Representation.exists_bijective_aeval_symmetricAlgebraInvariants_dual_of_pseudoreflectionSubgroup_eq_top.{u_1,
    u_2, u_3}
  {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [Fintype G] [AddCommGroup V]
  [_root_.Module K V] [FiniteDimensional K V] (ρ : Representation K G V)
  [Invertible ↑(Fintype.card G)] (hG : ρ.pseudoreflectionSubgroup = ⊤) :
  ∃ f,
    (∀ (i : Fin (Module.finrank K V)),
        ∃ d, 0 < d ∧ ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K (Module.Dual K V) d) ∧
      Function.Bijective ⇑(MvPolynomial.aeval f)
Lean

Formalized in Tau Ceti as Representation.exists_bijective_aeval_symmetricAlgebraInvariants_dual_of_pseudoreflectionSubgroup_eq_top.

Other forms

The Chevalley–Shephard–Todd theorem. Formalized in Tau Ceti as Representation.pseudoreflectionSubgroup_eq_top_iff_exists_bijective_aeval_symmetricAlgebraInvariants_dual.

Representation.pseudoreflectionSubgroup_eq_top_iff_exists_bijective_aeval_symmetricAlgebraInvariants_dual.{u_1,
    u_2, u_3}
  {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [CharZero K] [Group G] [Finite G]
  [AddCommGroup V] [_root_.Module K V] [FiniteDimensional K V] (ρ : Representation K G V)
  (hρ : Function.Injective ⇑ρ) :
  ρ.pseudoreflectionSubgroup = ⊤ ↔
    ∃ f,
      (∀ (i : Fin (Module.finrank K V)),
          ∃ d,
            0 < d ∧ ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K (Module.Dual K V) d) ∧
        Function.Bijective ⇑(MvPolynomial.aeval f)
Sources
LeanRepresentation.exists_bijective_aeval_symmetricAlgebraInvariants_dual_of_pseudoreflectionSubgroup_eq_top · Representation.pseudoreflectionSubgroup_eq_top_iff_exists_bijective_aeval_symmetricAlgebraInvariants_dual
Uses 6
Statement usesRepresentation.symmetricAlgebraInvariants
Proof usesThe converse of the Chevalley–Shephard–Todd theorem · The graded Nakayama lemma for generators · Noether's finiteness theorem (Representation.finiteType_symmetricAlgebraInvariants) · Serre's theorem (TauCeti.IsRegularLocalRing.of_hasProjectiveDimensionLE) · SymmetricAlgebra.dividedDifference

TheoremThe converse of the Chevalley–Shephard–Todd theorem#

Let a finite group G act faithfully and linearly on a finite-dimensional vector space V over a field K of characteristic zero. If the polynomial invariants Sym(V*)^G form a polynomial algebra on homogeneous invariants, then G is generated by its pseudoreflections, the elements whose fixed space is a hyperplane.

Representation.pseudoreflectionSubgroup_eq_top_of_bijective_aeval_symmetricAlgebraInvariants_dual.{u_1,
    u_2, u_3, u_4}
  {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [CharZero K] [Group G] [Finite G]
  [AddCommGroup V] [_root_.Module K V] [FiniteDimensional K V] (ρ : Representation K G V)
  (hρ : Function.Injective ⇑ρ) {ι : Type u_4} [Finite ι]
  {f : ι → ↥ρ.dual.symmetricAlgebraInvariants} {d : ι → ℕ}
  (hf : ∀ (i : ι), ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K (Module.Dual K V) (d i))
  (hbij : Function.Bijective ⇑(MvPolynomial.aeval f)) : ρ.pseudoreflectionSubgroup = ⊤
Informally uses
Lean

Formalized in Tau Ceti as Representation.pseudoreflectionSubgroup_eq_top_of_bijective_aeval_symmetricAlgebraInvariants_dual.

Sources
LeanRepresentation.pseudoreflectionSubgroup_eq_top_of_bijective_aeval_symmetricAlgebraInvariants_dual
Uses 2 · Used by 1
Statement usesRepresentation.symmetricAlgebraInvariants
Proof usesMolien's formula
Used byThe Chevalley–Shephard–Todd theorem

TheoremGraded Nakayama lemma for polynomial invariants#

Homogeneous invariants of positive degree whose classes span A₊ ⧸ A₊², where A₊ is the ideal of invariants with zero constant term, generate the invariant algebra Sym(M)^G as an R-algebra.

Representation.adjoin_range_eq_top_of_le_span_sup_sq.{u_1, u_3, u_4, u_5} {R : Type u_1}
  {G : Type u_3} {M : Type u_4} {ι : Type u_5} [CommSemiring R] [Monoid G] [AddCommMonoid M]
  [_root_.Module R M] (ρ : Representation R G M) (f : ι → ↥ρ.symmetricAlgebraInvariants) (d : ι → ℕ)
  (hd : ∀ (i : ι), 0 < d i)
  (hf : ∀ (i : ι), ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (d i))
  (hspan :
    Ideal.under (↥ρ.symmetricAlgebraInvariants)
        (HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)).toIdeal ≤
      Ideal.span (Set.range f) ⊔
        Ideal.under (↥ρ.symmetricAlgebraInvariants)
            (HomogeneousIdeal.irrelevant
                (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)).toIdeal ^
          2) :
  Algebra.adjoin R (Set.range f) = ⊤
Lean

Formalized in Tau Ceti as Representation.adjoin_range_eq_top_of_le_span_sup_sq.

Other forms

Graded Nakayama lemma for the coinvariant algebra. Formalized in Tau Ceti as Representation.span_range_eq_top_of_span_range_mk_eq_top.

Representation.span_range_eq_top_of_span_range_mk_eq_top.{u_1, u_2, u_3, u_4} {R : Type u_1}
  {G : Type u_2} {M : Type u_3} [CommRing R] [Monoid G] [AddCommMonoid M] [_root_.Module R M]
  (ρ : Representation R G M) {ι : Type u_4} (b : ι → SymmetricAlgebra R M)
  (hb : ∀ (i : ι), ∃ d, b i ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M d)
  (hspan :
    Submodule.span R (Set.range (⇑(Ideal.Quotient.mkₐ R ρ.symmetricAlgebraHilbertIdeal) ∘ b)) = ⊤) :
  Submodule.span (↥ρ.symmetricAlgebraInvariants) (Set.range b) = ⊤
Sources
LeanRepresentation.adjoin_range_eq_top_of_le_span_sup_sq · Representation.span_range_eq_top_of_span_range_mk_eq_top
Uses 2 · Used by 1
Statement usesRepresentation.symmetricAlgebraInvariants
Proof usesThe graded Nakayama lemma for generators
Used byChevalley's theorem: the coinvariant algebra of a reflection group is the regular representation

TheoremThe homogeneous Noether bound#

The invariants of a finite linear group over a rational algebra are generated by homogeneous invariants of positive degree at most the group order. This holds without finite generation or freeness of the underlying module.

Representation.symmetricAlgebraInvariants_eq_adjoin_homogeneous.{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] [Algebra ℚ R] :
  ρ.symmetricAlgebraInvariants =
    Algebra.adjoin R
      {p |
        p ∈ ρ.symmetricAlgebraInvariants ∧
          ∃ n, 0 < n ∧ n ≤ Fintype.card G ∧ p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n}
Lean

Formalized in Tau Ceti as Representation.symmetricAlgebraInvariants_eq_adjoin_homogeneous.

Sources
LeanRepresentation.symmetricAlgebraInvariants_eq_adjoin_homogeneous
Uses 2
Statement usesRepresentation.symmetricAlgebraInvariants
Proof usesNoether's degree bound

TheoremNoether's finiteness theorem (Representation.finiteType_symmetricAlgebraInvariants)#

Noether's finiteness theorem for the invariants of a finite group acting on a finitely generated module over a Noetherian ring: the invariant subalgebra is of finite type.

Representation.finiteType_symmetricAlgebraInvariants.{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) [Finite G] [IsNoetherianRing R] [Module.Finite R M] :
  Algebra.FiniteType R ↥ρ.symmetricAlgebraInvariants
Lean

Formalized in Tau Ceti as Representation.finiteType_symmetricAlgebraInvariants.

Sources
LeanRepresentation.finiteType_symmetricAlgebraInvariants
Uses 2 · Used by 2
Statement usesRepresentation.symmetricAlgebraInvariants
Proof usesNoether's finiteness theorem (TauCeti.FixedPoints.finiteType_subalgebra)
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.