Flatness over polynomial invariants

For a finite group whose order is invertible, divided differences for a generating family force the symmetric algebra to be faithfully flat over its invariant subalgebra.

In particular, if a finite group acting on a vector space is generated by elements whose fixed spaces have codimension one, then the polynomial functions Sym(V*) are faithfully flat over their invariants. This supplies the flat extension used in regularity descent for reflection invariants; it does not require polynomial generators for the invariant algebra.

The flatness statement uses vanishing of Mathlib's CategoryTheory.Tor', which derives the first tensor factor. Faithfulness follows from the existing integrality of the symmetric algebra over finite-group invariants.

References

• R. Kane, Reflection Groups and Invariant Theory, Springer (2001), §§ 17–18.
• L. Smith, Polynomial Invariants of Finite Groups, A K Peters (1995), § 7.2.

theorem Representation.flat_symmetricAlgebra {R : Type u} {M : Type v} {G : Type u_1} [CommRing R] [Group G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) [Fintype G] [Invertible ↑(Fintype.card G)] {ι : Type u_2} {s : ι → G} (hs : Subgroup.closure (Set.range s) = ⊤) (ℓ : ι → M) (hσ : ∀ (i : ι) (m : M), m - (ρ (s i)) m ∈ R ∙ ℓ i) (hℓ : ∀ (i : ι), IsLeftRegular ((SymmetricAlgebra.ι R M) (ℓ i))) : Module.Flat (↥ρ.symmetricAlgebraInvariants) (SymmetricAlgebra R M)

A symmetric algebra is flat over its invariants if the group has a generating family admitting divided differences with nonzerodivisor denominators.

theorem Representation.faithfullyFlat_symmetricAlgebra {R : Type u} {M : Type v} {G : Type u_1} [CommRing R] [Group G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) [Fintype G] [Invertible ↑(Fintype.card G)] {ι : Type u_2} {s : ι → G} (hs : Subgroup.closure (Set.range s) = ⊤) (ℓ : ι → M) (hσ : ∀ (i : ι) (m : M), m - (ρ (s i)) m ∈ R ∙ ℓ i) (hℓ : ∀ (i : ι), IsLeftRegular ((SymmetricAlgebra.ι R M) (ℓ i))) : Module.FaithfullyFlat (↥ρ.symmetricAlgebraInvariants) (SymmetricAlgebra R M)

A symmetric algebra is faithfully flat over its invariants if the group has a generating family admitting divided differences with nonzerodivisor denominators.

theorem Representation.faithfullyFlat_symmetricAlgebra_dual_of_finrank_quotient_eq_one {G : Type u_1} [Group G] [Fintype G] {K : Type u_2} {V : Type u_3} [Field K] [AddCommGroup V] [Module K V] (ρ : Representation K G V) [Invertible ↑(Fintype.card G)] {ι : Type u_4} {s : ι → G} (hs : Subgroup.closure (Set.range s) = ⊤) (hcodim : ∀ (i : ι), Module.finrank K (V ⧸ (ρ (s i)).fixedSubmodule) = 1) : Module.FaithfullyFlat (↥ρ.dual.symmetricAlgebraInvariants) (SymmetricAlgebra K (Module.Dual K V))

Polynomial functions on a vector space are faithfully flat over their invariants when the group is generated by elements with codimension-one fixed spaces and its order is invertible in the field. No assumption of finite-dimensionality or faithfulness of the action is needed.

theorem Representation.faithfullyFlat_symmetricAlgebra_dual_of_pseudoreflectionSubgroup_eq_top {G : Type u_1} [Group G] [Fintype G] {K : Type u_2} {V : Type u_3} [Field K] [AddCommGroup V] [Module K V] (ρ : Representation K G V) [Invertible ↑(Fintype.card G)] (hG : ρ.pseudoreflectionSubgroup = ⊤) : Module.FaithfullyFlat (↥ρ.dual.symmetricAlgebraInvariants) (SymmetricAlgebra K (Module.Dual K V))

Polynomial functions on a vector space are faithfully flat over their invariants when the group is generated by pseudoreflections and its order is invertible in the field.