Documentation

TauCeti.RingTheory.DividedPowerAlgebra.Exp

The divided-power exponential #

For a module M over a commutative semiring R and a commutative R-algebra S, this file defines the divided-power exponential exp(x) = ∑_d γ_d(x) X ^ d of x : S ⊗[R] M, a power series with coefficients in S ⊗[R] Γ_R(M). It is determined by exp(s ⊗ m) = ∑ₙ (s ^ n ⊗ dp R n m) X ^ n and exp(x + y) = exp(x) * exp(y), and its coefficients satisfy the divided-power relations γ₀ = 1 and γₘ * γₙ = (m + n).choose m • γₘ₊ₙ.

Main declarations #

Implementation notes #

The Roby relations dp_add, dp_mul and dp_smul say exactly that the formula exp(s ⊗ m) = ∑ₙ (s ^ n ⊗ dp R n m) X ^ n is multiplicative in each of s and m, and balanced, so that exp is a well-defined map from S ⊗[R] M to the multiplicative monoid of power series.

References #

source
noncomputable def DividedPowerAlgebra.exp {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra R S] (x : TensorProduct R S M) :
PowerSeries (TensorProduct R S (DividedPowerAlgebra R M))

The divided-power exponential exp(x) = ∑_d γ_d(x) X ^ d of x : S ⊗[R] M, a power series with coefficients in S ⊗[R] Γ_R(M). It is the additive-to-multiplicative map determined by exp(s ⊗ m) = ∑ₙ (s ^ n ⊗ dp R n m) X ^ n (coeff_exp_tmul, exp_zero, exp_add).

Instances For
    source
    @[simp]
    theorem DividedPowerAlgebra.coeff_exp_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra R S] (s : S) (m : M) (n : ℕ) :
    (PowerSeries.coeff n) (exp (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m

    The coefficients of the exponential of a pure tensor: exp(s ⊗ m) = ∑ₙ (s ^ n ⊗ dp R n m) X ^ n.

    source
    @[simp]
    theorem DividedPowerAlgebra.exp_zero {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra R S] :
    exp 0 = 1

    The exponential of 0 is 1.

    source
    theorem DividedPowerAlgebra.exp_add {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra R S] (x y : TensorProduct R S M) :
    exp (x + y) = exp x * exp y

    The exponential turns sums into products.

    source
    theorem DividedPowerAlgebra.exp_rTensor {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra R S] {T : Type u_4} [CommSemiring T] [Algebra R T] (φ : S →ₐ[R] T) (x : TensorProduct R S M) :
    exp ((LinearMap.rTensor M φ.toLinearMap) x) = (PowerSeries.map (Algebra.TensorProduct.rTensor (DividedPowerAlgebra R M) φ).toRingHom) (exp x)

    The exponential is natural in the algebra S.

    source
    theorem DividedPowerAlgebra.exp_smul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra R S] (s : S) (x : TensorProduct R S M) :
    exp (s • x) = (PowerSeries.rescale (s ⊗ₜ[R] 1)) (exp x)

    Scalar multiplication by s rescales the exponential by s ⊗ 1.

    source
    @[simp]
    theorem DividedPowerAlgebra.constantCoeff_exp {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra R S] (x : TensorProduct R S M) :
    PowerSeries.constantCoeff (exp x) = 1

    The constant coefficient of the exponential is 1: the divided-power relation γ₀ = 1.

    source
    theorem DividedPowerAlgebra.coeff_exp_mul_coeff_exp {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra R S] (x : TensorProduct R S M) (m n : ℕ) :
    (PowerSeries.coeff m) (exp x) * (PowerSeries.coeff n) (exp x) = (m + n).choose m • (PowerSeries.coeff (m + n)) (exp x)

    The coefficients of the exponential multiply like divided powers: γₘ(x) * γₙ(x) = (m + n).choose m • γₘ₊ₙ(x).