Documentation

TauCeti.RepresentationTheory.SymmetricAlgebra.Tor

Invariants of Tor' over the polynomial invariants #

Let ρ be a representation of a group G on a module M over a commutative ring R, and let A = Sym(M)^G be the invariant subalgebra of the symmetric algebra S = Sym M. Every ρ g acts on S by an A-linear map, since it fixes A pointwise; this is the representation Representation.symmetricAlgebraOverInvariants of G on the A-module S, whose invariants are A itself (both in TauCeti.RepresentationTheory.SymmetricAlgebra.Basic). Every additive functor F on A-modules therefore carries an action of G on F(S), by CategoryTheory.Functor.mapRepresentation.

The main example is F = Tor'ₙ^A(N, -), Mathlib's CategoryTheory.Tor', which derives the tensor product in its first variable N. When G is finite and #G is invertible in R, the invariants of Tor'ₙ^A(N, S) are Tor'ₙ^A(N, A), which vanishes in positive degrees because A is the tensor unit. So Tor'ₙ₊₁^A(N, S) has no nonzero invariant element (Representation.invariants_mapRepresentation_Tor'_symmetricAlgebraOverInvariants).

Divided differences interact with this action. If m - ρ g m is a multiple of ℓ for every m, and ℓ is a nonzerodivisor of S, the divided-difference operator δ_g is A-linear and satisfies 1 - g = m_ℓ ∘ δ_g on S, so the same identity holds after applying any additive functor (Representation.map_symmetricAlgebraDividedDifference_comp_map_mulLeft, in TauCeti.RepresentationTheory.SymmetricAlgebra.DividedDifference). Combining the two facts: if G is generated by elements s of this kind, such as pseudoreflections of a vector space V acting on Sym(V*), then an element of Tor'ₙ₊₁^A(N, S) killed by every δ_s is fixed by every generator, hence invariant, hence zero (Representation.eq_zero_of_forall_Tor'_map_symmetricAlgebraDividedDifference_eq_zero).

The divided differences lower degrees, so every element of S is killed by all sufficiently long composites of them (Representation.iSup_wordKer_symmetricAlgebraDividedDifference_eq_top), and this local nilpotence passes to Tor'ₙ^A(N, S) (CategoryTheory.iSup_wordKer_Tor'_map_eq_top). An element killed by all composites of length d + 1 is sent by every δ_s to one killed by all composites of length d, so by induction on d every element vanishes: Tor'ₙ₊₁^A(N, S) = 0 for every A-module N (Representation.isZero_Tor'_succ_symmetricAlgebra). No grading of Tor' is needed for this.

This is the vanishing step of the homological proof that the invariants of a finite group generated by pseudoreflections in characteristic zero form a polynomial algebra (Chevalley, Shephard–Todd), where it is applied to the residue field N = A ⧸ A₊.

Main results #

References #

source
theorem Representation.invariants_mapRepresentation_Tor'_symmetricAlgebraOverInvariants {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)] (N : ModuleCat ↥ρ.symmetricAlgebraInvariants) (n : ℕ) :
(((CategoryTheory.Tor' (ModuleCat ↥ρ.symmetricAlgebraInvariants) (n + 1)).obj N).mapRepresentation ρ.symmetricAlgebraOverInvariants).invariants = ⊥

Tor'ₙ₊₁(N, Sym M) has no nonzero invariants. Let G be finite with #G invertible in R, and let A = Sym(M)^G. For every A-module N, the action of G on Tor'ₙ₊₁^A(N, Sym M) induced by its action on Sym M has no nonzero invariant element. Indeed these invariants are Tor'ₙ₊₁^A(N, A), by CategoryTheory.Functor.invariants_mapRepresentation, and this vanishes since A is the tensor unit.

source
theorem Representation.eq_zero_of_forall_Tor'_map_symmetricAlgebraDividedDifference_eq_zero {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))) (N : ModuleCat ↥ρ.symmetricAlgebraInvariants) (n : ℕ) (x : ↑(((CategoryTheory.Tor' (ModuleCat ↥ρ.symmetricAlgebraInvariants) (n + 1)).obj N).obj ↧(SymmetricAlgebra R M))) (hx : ∀ (i : ι), (ModuleCat.Hom.hom (((CategoryTheory.Tor' (ModuleCat ↥ρ.symmetricAlgebraInvariants) (n + 1)).obj N).map (ModuleCat.ofHom (ρ.symmetricAlgebraDividedDifference (s i) (ℓ i) ⋯ ⋯)))) x = 0) :
x = 0

Elements of Tor'ₙ₊₁(N, Sym M) killed by divided differences vanish. Let G be finite with #G invertible in R, generated by a family s i such that m - ρ (s i) m is a multiple of ℓ i for every m, where ℓ i is a nonzerodivisor of Sym M. Over A = Sym(M)^G, if an element of Tor'ₙ₊₁^A(N, Sym M) is killed by the map induced by every divided-difference operator δ_(s i), then it is zero: it is fixed by every s i, by the operator identity 1 - s i = m_(ℓ i) ∘ δ_(s i), hence invariant.

source
theorem Representation.isZero_Tor'_succ_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))) (N : ModuleCat ↥ρ.symmetricAlgebraInvariants) (n : ℕ) :
CategoryTheory.Limits.IsZero (((CategoryTheory.Tor' (ModuleCat ↥ρ.symmetricAlgebraInvariants) (n + 1)).obj N).obj ↧(SymmetricAlgebra R M))

Tor'ₙ₊₁(N, Sym M) vanishes for a group generated by elements with divided differences. Let G be finite with #G invertible in R, generated by a family s i such that m - ρ (s i) m is a multiple of ℓ i for every m, where ℓ i is a nonzerodivisor of Sym M. Then over A = Sym(M)^G, Tor'ₙ₊₁^A(N, Sym M) = 0 for every A-module N; for N = A ⧸ A₊ this is the vanishing of Tor'₁^A(A ⧸ A₊, Sym M).

The hypotheses hold for a finite group generated by pseudoreflections s i of a vector space V over a field in which #G is invertible, acting on the polynomial functions Sym(V*), with ℓ i a nonzero linear form vanishing on the hyperplane fixed by s i.