The exponential specialization of a monoid algebra

The functional equation e^{aX} e^{bX} = e^{(a+b)X} of the exponential power series (PowerSeries.exp_mul_exp_eq_exp_add) says that a ↦ e^{aX} is a homomorphism from the additive group of a ℚ-algebra R to the multiplicative monoid of R⟦X⟧. Composed with an additive map φ : M →+ R and extended linearly, it turns the monoid algebra k[M] into power series:

∑ c_m e^m ↦ ∑ c_m e^{φ(m) X}.

This is the exponential specialization of k[M] along φ. It is the device by which a formal identity in a group algebra, such as the Weyl character formula, is turned into a numerical identity between its coefficients: the constant coefficient of the image is the sum of the coefficients (the augmentation), and the higher coefficients are the moments ∑ c_m φ(m)^n / n!.

Main definitions

• PowerSeries.expMonoidHom: a ↦ e^{aX} as a monoid homomorphism Multiplicative R →* R⟦X⟧.
• AddMonoidAlgebra.expAlgHom φ: the exponential specialization k[M] →ₐ[k] R⟦X⟧ along an additive map φ : M →+ R.

Main results

• PowerSeries.constantCoeff_rescale: rescaling the variable keeps the constant coefficient.
• AddMonoidAlgebra.expAlgHom_single: e^m ↦ e^{φ(m) X}.
• AddMonoidAlgebra.constantCoeff_expAlgHom: the constant coefficient of the exponential specialization is the sum of the coefficients.

@[simp]

theorem PowerSeries.constantCoeff_rescale {R : Type u_1} [CommSemiring R] (a : R) (f : PowerSeries R) : constantCoeff ((rescale a) f) = constantCoeff f

Rescaling the variable does not change the constant coefficient.

noncomputable def PowerSeries.expMonoidHom (R : Type u_1) [CommRing R] [Algebra ℚ R] : Multiplicative R →* PowerSeries R

The exponential a ↦ e^{aX} as a monoid homomorphism Multiplicative R →* R⟦X⟧. That this is a homomorphism is the functional equation PowerSeries.exp_mul_exp_eq_exp_add.

Equations

• PowerSeries.expMonoidHom R = { toFun := fun (a : Multiplicative R) => (PowerSeries.rescale (Multiplicative.toAdd a)) (PowerSeries.exp R), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem PowerSeries.expMonoidHom_apply {R : Type u_1} [CommRing R] [Algebra ℚ R] (a : Multiplicative R) : (expMonoidHom R) a = (rescale (Multiplicative.toAdd a)) (exp R)

The exponential monoid homomorphism sends a to the exponential series rescaled by a.

theorem PowerSeries.expMonoidHom_ofAdd {R : Type u_1} [CommRing R] [Algebra ℚ R] (a : R) : (expMonoidHom R) (Multiplicative.ofAdd a) = (rescale a) (exp R)

e^{aX} is the exponential series rescaled by a.

noncomputable def AddMonoidAlgebra.expAlgHom {k : Type u_1} [CommSemiring k] {M : Type u_2} [AddMonoid M] {R : Type u_3} [CommRing R] [Algebra ℚ R] [Algebra k R] (φ : M →+ R) : AddMonoidAlgebra k M →ₐ[k] PowerSeries R

The exponential specialization of the monoid algebra k[M] along an additive map φ : M →+ R: the k-algebra homomorphism k[M] →ₐ[k] R⟦X⟧ sending e^m to e^{φ(m) X}. Its constant coefficient is the augmentation ∑ c_m e^m ↦ ∑ c_m (AddMonoidAlgebra.constantCoeff_expAlgHom), and its higher coefficients are the moments of the coefficients against φ.

Equations

• AddMonoidAlgebra.expAlgHom φ = (AddMonoidAlgebra.lift k (PowerSeries R) M) ((PowerSeries.expMonoidHom R).comp (AddMonoidHom.toMultiplicative φ))

@[simp]

theorem AddMonoidAlgebra.expAlgHom_single {k : Type u_1} [CommSemiring k] {M : Type u_2} [AddMonoid M] {R : Type u_3} [CommRing R] [Algebra ℚ R] [Algebra k R] (φ : M →+ R) (m : M) (c : k) : (expAlgHom φ) (single m c) = (algebraMap k (PowerSeries R)) c * (PowerSeries.rescale (φ m)) (PowerSeries.exp R)

The exponential specialization sends c e^m to c e^{φ(m) X}, the scalar c acting through algebraMap k R⟦X⟧.

The scalar is written as a ring element rather than as c • _: for k = ℤ the scalar action of ℤ on R⟦X⟧ through the algebra structure is not syntactically the action n • p elaborates to, whereas algebraMap ℤ R⟦X⟧ n simplifies to the cast (n : R⟦X⟧).

@[simp]

theorem AddMonoidAlgebra.constantCoeff_expAlgHom {k : Type u_1} [CommSemiring k] {M : Type u_2} [AddMonoid M] {R : Type u_3} [CommRing R] [Algebra ℚ R] [Algebra k R] (φ : M →+ R) (f : AddMonoidAlgebra k M) : PowerSeries.constantCoeff ((expAlgHom φ) f) = (algebraMap k R) (f.coeff.sum fun (x : M) (c : k) => c)

The constant coefficient of the exponential specialization is the sum of the coefficients: the specialization at X = 0 is the augmentation of the monoid algebra.