Graded traces modulo a homogeneous regular element

Let A be a nonnegatively graded algebra over a field, with finite-dimensional pieces. Suppose T preserves the grading, commutes with multiplication by a homogeneous regular element f of degree d, and induces Q on A/(f). Then the trace series of Q is the trace series of T multiplied by 1 - t^d.

In particular, a graded algebra automorphism fixing f satisfies the multiplication compatibility. Applied to group elements and invariant relations, this is the equivariant one-relation exact-sequence formula for computing graded coinvariant characters. Unlike a Hilbert series, its coefficients record the action of each element, not only dimensions. No finite-order, characteristic-zero, or positivity assumption on d is needed.

The maps are linear, rather than necessarily multiplicative, so the result also applies to endomorphisms of the multiplication/quotient exact sequence. Compatibility with the quotient map supplies preservation of the quotient pieces.

Iterating over a homogeneous weakly regular sequence multiplies the trace series by one factor 1 - t^d for each element. Here T need only commute with multiplication by the elements of the sequence; it then preserves the ideal they generate, and induces the endomorphism of each intermediate quotient used in the induction.

Main results

• trace_quotientPiece_span_singleton_add: trace additivity in degrees at least d.
• trace_quotientPiece_span_singleton_of_lt: traces are unchanged below d.
• mk_trace_quotientPiece_span_singleton: the trace-series identity.
• trace_quotientPiece_of_eq_bot: quotienting by the zero ideal does not change traces.
• mk_trace_quotientPiece_sup_span_singleton: the trace-series identity for one further element, regular modulo a homogeneous ideal.
• mk_trace_quotientPiece_of_isWeaklyRegular: the trace-series identity for a homogeneous weakly regular sequence.

References

• R. P. Stanley, Invariants of finite groups and their applications to combinatorics, Bull. Amer. Math. Soc. (N.S.) 1 (1979), §3.

The exact sequences are those of HilbertSeries.RegularElement; trace additivity uses LinearMap.trace_eq_add_of_exact. The induction over a sequence follows the dimension version mk_finrank_quotientPiece_of_isWeaklyRegular in HilbertSeries.RegularSequence.

theorem TauCeti.GradedAlgebra.trace_quotientPiece_span_singleton_of_lt {k : Type u_1} {A : Type u_2} [CommRing A] [CommRing k] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] {f : A} {d : ℕ} (T : A →ₗ[k] A) (Q : A ⧸ Ideal.span {f} →ₗ[k] A ⧸ Ideal.span {f}) (hT : ∀ (n : ℕ), ∀ x ∈ 𝒜 n, T x ∈ 𝒜 n) (hQ : ∀ (x : A), Q ((Ideal.Quotient.mk (Ideal.span {f})) x) = (Ideal.Quotient.mk (Ideal.span {f})) (T x)) (hf : f ∈ 𝒜 d) {n : ℕ} (hn : n < d) : (LinearMap.trace k ↥(quotientPiece 𝒜 (Ideal.span {f}) n)) (Q.restrict ⋯) = (LinearMap.trace k ↥(𝒜 n)) (T.restrict ⋯)

Below the degree of a homogeneous relation, a compatible quotient endomorphism has the same trace as the original endomorphism. Regularity and finite-dimensionality are not needed for this statement, and the coefficient ring need not be a field.

theorem TauCeti.GradedAlgebra.trace_quotientPiece_span_singleton_add {k : Type u_1} {A : Type u_2} [CommRing A] [Field k] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] {f : A} {d : ℕ} (T : A →ₗ[k] A) (Q : A ⧸ Ideal.span {f} →ₗ[k] A ⧸ Ideal.span {f}) (hT : ∀ (n : ℕ), ∀ x ∈ 𝒜 n, T x ∈ 𝒜 n) (hQ : ∀ (x : A), Q ((Ideal.Quotient.mk (Ideal.span {f})) x) = (Ideal.Quotient.mk (Ideal.span {f})) (T x)) (hf : f ∈ 𝒜 d) (hreg : IsLeftRegular f) (hmul : ∀ (x : A), T (f * x) = f * T x) (n : ℕ) [Module.Finite k ↥(𝒜 (d + n))] : (LinearMap.trace k ↥(quotientPiece 𝒜 (Ideal.span {f}) (d + n))) (Q.restrict ⋯) + (LinearMap.trace k ↥(𝒜 n)) (T.restrict ⋯) = (LinearMap.trace k ↥(𝒜 (d + n))) (T.restrict ⋯)

The trace in degree d + n before quotienting is the sum of the quotient trace and the original degree-n trace, for an endomorphism commuting with multiplication by the homogeneous regular relation.

theorem TauCeti.GradedAlgebra.mk_trace_quotientPiece_span_singleton {k : Type u_1} {A : Type u_2} [CommRing A] [Field k] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] {f : A} {d : ℕ} (T : A →ₗ[k] A) (Q : A ⧸ Ideal.span {f} →ₗ[k] A ⧸ Ideal.span {f}) (hT : ∀ (n : ℕ), ∀ x ∈ 𝒜 n, T x ∈ 𝒜 n) (hQ : ∀ (x : A), Q ((Ideal.Quotient.mk (Ideal.span {f})) x) = (Ideal.Quotient.mk (Ideal.span {f})) (T x)) [∀ (n : ℕ), Module.Finite k ↥(𝒜 n)] (hf : f ∈ 𝒜 d) (hreg : IsLeftRegular f) (hmul : ∀ (x : A), T (f * x) = f * T x) : (PowerSeries.mk fun (n : ℕ) => (LinearMap.trace k ↥(quotientPiece 𝒜 (Ideal.span {f}) n)) (Q.restrict ⋯)) = (PowerSeries.mk fun (n : ℕ) => (LinearMap.trace k ↥(𝒜 n)) (T.restrict ⋯)) * (1 - PowerSeries.X ^ d)

Quotienting by a homogeneous regular element of degree d multiplies the graded trace series by 1 - t^d, provided the endomorphism commutes with multiplication by that element. The coefficients lie in the original field, in arbitrary characteristic.

theorem TauCeti.GradedAlgebra.trace_quotientPiece_of_eq_bot {k : Type u_1} {A : Type u_2} [CommRing A] [CommRing k] [Algebra k A] (𝒜 : ℕ → Submodule k A) (T : A →ₗ[k] A) (hT : ∀ (n : ℕ), ∀ x ∈ 𝒜 n, T x ∈ 𝒜 n) {J : Ideal A} (hJ : J = ⊥) (Q : A ⧸ J →ₗ[k] A ⧸ J) (hQ : ∀ (x : A), Q ((Ideal.Quotient.mk J) x) = (Ideal.Quotient.mk J) (T x)) (n : ℕ) : (LinearMap.trace k ↥(quotientPiece 𝒜 J n)) (Q.restrict ⋯) = (LinearMap.trace k ↥(𝒜 n)) (T.restrict ⋯)

Quotienting by the zero ideal does not change the traces of a compatible endomorphism. The family 𝒜 need not be a grading.

theorem TauCeti.GradedAlgebra.mk_trace_quotientPiece_sup_span_singleton {k : Type u_1} {A : Type u_2} [CommRing A] [Field k] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] (T : A →ₗ[k] A) (hT : ∀ (n : ℕ), ∀ x ∈ 𝒜 n, T x ∈ 𝒜 n) [∀ (n : ℕ), Module.Finite k ↥(𝒜 n)] {I : Ideal A} (hI : Submodule.IsHomogeneous I 𝒜) {f : A} {d : ℕ} (hf : f ∈ 𝒜 d) (hreg : IsLeftRegular ((Ideal.Quotient.mk I) f)) (hmul : ∀ (x : A), T (f * x) = f * T x) (Q₀ : A ⧸ I →ₗ[k] A ⧸ I) (hQ₀ : ∀ (x : A), Q₀ ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk I) (T x)) (J : Ideal A) (hJ : I ⊔ Ideal.span {f} = J) (Q : A ⧸ J →ₗ[k] A ⧸ J) (hQ : ∀ (x : A), Q ((Ideal.Quotient.mk J) x) = (Ideal.Quotient.mk J) (T x)) : (PowerSeries.mk fun (n : ℕ) => (LinearMap.trace k ↥(quotientPiece 𝒜 J n)) (Q.restrict ⋯)) = (PowerSeries.mk fun (n : ℕ) => (LinearMap.trace k ↥(quotientPiece 𝒜 I n)) (Q₀.restrict ⋯)) * (1 - PowerSeries.X ^ d)

Quotienting further by a homogeneous element f of degree d, regular modulo a homogeneous ideal I (its class is left-regular in A ⧸ I), multiplies the graded trace series by 1 - t^d, provided the endomorphism T commutes with multiplication by f. Here Q₀ and Q are the endomorphisms induced by T on A ⧸ I and on A ⧸ J, where J = I ⊔ (f).

theorem TauCeti.GradedAlgebra.mk_trace_quotientPiece_of_isWeaklyRegular {k : Type u_1} {A : Type u_2} [CommRing A] [Field k] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] (T : A →ₗ[k] A) (hT : ∀ (n : ℕ), ∀ x ∈ 𝒜 n, T x ∈ 𝒜 n) [∀ (n : ℕ), Module.Finite k ↥(𝒜 n)] (fs : List (A × ℕ)) (hhom : ∀ p ∈ fs, p.1 ∈ 𝒜 p.2) (hreg : RingTheory.Sequence.IsWeaklyRegular A (List.map Prod.fst fs)) (hmul : ∀ p ∈ fs, ∀ (x : A), T (p.1 * x) = p.1 * T x) (J : Ideal A) (hJ : Ideal.ofList (List.map Prod.fst fs) = J) (Q : A ⧸ J →ₗ[k] A ⧸ J) (hQ : ∀ (x : A), Q ((Ideal.Quotient.mk J) x) = (Ideal.Quotient.mk J) (T x)) : (PowerSeries.mk fun (n : ℕ) => (LinearMap.trace k ↥(quotientPiece 𝒜 J n)) (Q.restrict ⋯)) = (PowerSeries.mk fun (n : ℕ) => (LinearMap.trace k ↥(𝒜 n)) (T.restrict ⋯)) * (List.map (fun (p : A × ℕ) => 1 - PowerSeries.X ^ p.2) fs).prod

Quotienting by a homogeneous weakly regular sequence multiplies the graded trace series by one factor 1 - t^d for each element, provided the endomorphism T commutes with multiplication by every element of the sequence; Q is the endomorphism it induces on the quotient. The quotient is taken by any ideal J equal to the ideal generated by the sequence, such as an ideal defined independently and shown to be generated by it. A list of element-degree pairs keeps the degrees attached to their chosen elements, including when an element is zero or has degree zero. The coefficients lie in the original field, in arbitrary characteristic.