The exponential series in ring extensions of the rational numbers
Content created by malarbol.
Created on 2026-09-18.
Last modified on 2026-09-18.
module ring-theory.exponential-series-ring-extensions-rational-numbers where
Imports
open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.binary-sum-decompositions-natural-numbers open import elementary-number-theory.binomial-coefficients open import elementary-number-theory.distance-natural-numbers open import elementary-number-theory.factorials open import elementary-number-theory.integers open import elementary-number-theory.natural-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.reciprocal-factorials open import elementary-number-theory.ring-of-rational-numbers open import elementary-number-theory.semiring-of-natural-numbers open import elementary-number-theory.strict-inequality-natural-numbers open import foundation.action-on-identifications-functions open import foundation.binary-transport open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-extensionality open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.universe-levels open import linear-algebra.finite-sequences-in-rings open import ring-theory.binomial-theorem-rings open import ring-theory.commuting-elements-rings open import ring-theory.convolution-sequences-rings open import ring-theory.convolution-sequences-semirings open import ring-theory.integer-multiples-of-elements-rings open import ring-theory.invertible-elements-rings open import ring-theory.multiples-of-elements-rings open import ring-theory.powers-of-elements-rings open import ring-theory.ring-extensions-rational-numbers open import ring-theory.rings open import ring-theory.semirings open import ring-theory.sequences-rings open import ring-theory.sums-of-finite-families-of-elements-rings open import ring-theory.sums-of-finite-sequences-of-elements-rings open import univalent-combinatorics.classical-finite-types open import univalent-combinatorics.counting open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types
Idea
The
exponential series¶
in a ring extension of ℚ R
is the series with coefficients n ↦ 1/n!.
For any x ∈ R, the sequence of terms of the exponential series at x is the
sequence exp(x) : n ↦ xⁿ/n!. Note that exp(x) is not an element of R but a
sequence in R, namely the sequence of coefficients of the formal power series
exp(xT) = ∑ₙ (xⁿ/n!) Tⁿ; no convergence is involved.
The sequence of terms of the exponential series satisfies the two following conditions:
exp(0) = 1, where1is the unit of the convolution product, i.e., the Kronecker delta at0:δ₀ = (1, 0, 0, ...)- if
x , y ∈ Rcommute, thenexp(x + y) = exp(x) ⋆ exp(y)where⋆denotes the convolution product.
Definitions
The sequence of coefficients of the exponential series
module _ {l : Level} (R : Rational-Extension-Ring l) where coefficient-exponential-series-Rational-Extension-Ring : type-sequence-Ring (ring-Rational-Extension-Ring R) coefficient-exponential-series-Rational-Extension-Ring = map-initial-hom-Rational-Extension-Ring R ∘ inv-factorial-ℕ
The sequence of terms of the exponential series
module _ {l : Level} (R : Rational-Extension-Ring l) where term-ev-exponential-series-Rational-Extension-Ring : type-Rational-Extension-Ring R → type-sequence-Ring (ring-Rational-Extension-Ring R) term-ev-exponential-series-Rational-Extension-Ring x n = mul-Rational-Extension-Ring R ( coefficient-exponential-series-Rational-Extension-Ring R n) ( power-Ring (ring-Rational-Extension-Ring R) n x)
Properties
The exponential of zero is one
The sequence of terms of exp(0) is (1, 0, 0, 0, ...), the unit of the
convolution product.
module _ {l : Level} (R : Rational-Extension-Ring l) where abstract htpy-term-ev-zero-exponential-series-Rational-Extension-Ring : term-ev-exponential-series-Rational-Extension-Ring R ( zero-Ring (ring-Rational-Extension-Ring R)) ~ one-Ring (convolution-sequence-Ring (ring-Rational-Extension-Ring R)) htpy-term-ev-zero-exponential-series-Rational-Extension-Ring zero-ℕ = right-unit-law-mul-Ring (ring-Rational-Extension-Ring R) _ ∙ ap ( map-initial-hom-Rational-Extension-Ring R) ( compute-zero-inv-factorial-ℕ) ∙ preserves-one-initial-hom-Rational-Extension-Ring R htpy-term-ev-zero-exponential-series-Rational-Extension-Ring (succ-ℕ n) = ap ( mul-Rational-Extension-Ring R ( coefficient-exponential-series-Rational-Extension-Ring R (succ-ℕ n))) ( power-succ-Ring (ring-Rational-Extension-Ring R) n _ ∙ right-zero-law-mul-Ring (ring-Rational-Extension-Ring R) _) ∙ right-zero-law-mul-Ring ( ring-Rational-Extension-Ring R) ( coefficient-exponential-series-Rational-Extension-Ring R (succ-ℕ n))
Relation with binomial coefficients
For any n ∈ ℕ and i ≤ n,
1/i! * 1/(n - i)! ＝ (binomial-coefficient n i) · 1/n!
where · denotes the multiple in the ring.
module _ {l : Level} (R : Rational-Extension-Ring l) where abstract compute-mul-binomial-coefficient-exponential-series-Rational-Extension-Ring : (n : ℕ) → (i : Fin (succ-ℕ n)) → mul-Rational-Extension-Ring R ( coefficient-exponential-series-Rational-Extension-Ring R ( nat-Fin (succ-ℕ n) i)) ( coefficient-exponential-series-Rational-Extension-Ring R ( dist-ℕ (nat-Fin (succ-ℕ n) i) n)) ＝ multiple-Ring ( ring-Rational-Extension-Ring R) ( binomial-coefficient-Fin n i) ( coefficient-exponential-series-Rational-Extension-Ring R n) compute-mul-binomial-coefficient-exponential-series-Rational-Extension-Ring n i = inv (preserves-mul-initial-hom-Rational-Extension-Ring R) ∙ ap ( map-initial-hom-Rational-Extension-Ring R) ( inv ( binomial-coefficient-multiple-split-inv-factorial-formula-ℕ ( n) ( nat-Fin (succ-ℕ n) i) ( dist-ℕ (nat-Fin (succ-ℕ n) i) n) ( inv ( is-difference-dist-ℕ ( nat-Fin (succ-ℕ n) i) ( n) ( upper-bound-nat-Fin n i))))) ∙ ap ( map-initial-hom-Rational-Extension-Ring R) ( inv ( integer-multiple-int-Ring ( ring-ℚ) ( binomial-coefficient-Fin n i) ( inv-factorial-ℕ n))) ∙ preserves-integer-multiples-hom-Ring ( ring-ℚ) ( ring-Rational-Extension-Ring R) ( initial-hom-Rational-Extension-Ring R) ( int-ℕ (binomial-coefficient-Fin n i)) ( inv-factorial-ℕ n) ∙ ( integer-multiple-int-Ring ( ring-Rational-Extension-Ring R) ( binomial-coefficient-Fin n i) ( coefficient-exponential-series-Rational-Extension-Ring R n))
Interchange rule for the product of terms of exponential series
For any i j : ℕ,
(1/i!)(1/j!) (xⁱyʲ) ＝ (xⁱ/i!) (yʲ/j!)
module _ {l : Level} (R : Rational-Extension-Ring l) (x y : type-Rational-Extension-Ring R) (i j : ℕ) where abstract interchange-mul-term-exponential-series-Rational-Extension-Ring : mul-Rational-Extension-Ring R ( mul-Rational-Extension-Ring R ( coefficient-exponential-series-Rational-Extension-Ring R i) ( coefficient-exponential-series-Rational-Extension-Ring R j)) ( mul-Rational-Extension-Ring R ( power-Ring (ring-Rational-Extension-Ring R) i x) ( power-Ring (ring-Rational-Extension-Ring R) j y)) ＝ mul-Rational-Extension-Ring R ( term-ev-exponential-series-Rational-Extension-Ring R x i) ( term-ev-exponential-series-Rational-Extension-Ring R y j) interchange-mul-term-exponential-series-Rational-Extension-Ring = associative-mul-Ring (ring-Rational-Extension-Ring R) _ _ _ ∙ ap ( mul-Rational-Extension-Ring R _) ( inv (associative-mul-Ring (ring-Rational-Extension-Ring R) _ _ _)) ∙ ap ( λ z → mul-Rational-Extension-Ring R ( coefficient-exponential-series-Rational-Extension-Ring R i) ( mul-Rational-Extension-Ring R z ( power-Ring (ring-Rational-Extension-Ring R) j y))) ( is-central-map-initial-hom-Rational-Extension-Ring ( R) ( inv-factorial-ℕ j) ( power-Ring (ring-Rational-Extension-Ring R) i x)) ∙ ap ( mul-Rational-Extension-Ring R _) ( associative-mul-Ring (ring-Rational-Extension-Ring R) _ _ _) ∙ inv (associative-mul-Ring (ring-Rational-Extension-Ring R) _ _ _)
Additive properties of the exponential series
The sequence of terms of the exponential series of the sum of commuting elements
in a ring is the convolution product of the exponential series of each summand;
i.e., if x and y commute, for any n : ℕ,
(x + y)ⁿ/n! = Σ_{i + j = n} (xⁱ/i!) (yʲ/j!)
so
exp(x + y) = exp(x) ⋆ exp(y)
module _ {l : Level} (R : Rational-Extension-Ring l) (x y : type-Rational-Extension-Ring R) (H : commute-Ring (ring-Rational-Extension-Ring R) x y) where abstract htpy-term-ev-add-mul-convolution-exponential-series-Rational-Extension-Ring : term-ev-exponential-series-Rational-Extension-Ring R ( add-Rational-Extension-Ring R x y) ~ mul-convolution-sequence-Ring ( ring-Rational-Extension-Ring R) ( term-ev-exponential-series-Rational-Extension-Ring R x) ( term-ev-exponential-series-Rational-Extension-Ring R y) htpy-term-ev-add-mul-convolution-exponential-series-Rational-Extension-Ring n = ap ( mul-Rational-Extension-Ring R ( coefficient-exponential-series-Rational-Extension-Ring R n)) ( binomial-theorem-Ring (ring-Rational-Extension-Ring R) n x y H) ∙ left-distributive-mul-binomial-sum-fin-sequence-type-Ring ( ring-Rational-Extension-Ring R) ( n) ( coefficient-exponential-series-Rational-Extension-Ring R n) ( term-xy) ∙ htpy-sum-fin-sequence-type-Ring ( ring-Rational-Extension-Ring R) ( succ-ℕ n) ( inv ∘ htpy-expand-term-binomial-exponential) ∙ inv ( eq-sum-finite-sum-count-Ring ( ring-Rational-Extension-Ring R) ( Fin-Finite-Type (succ-ℕ n)) ( count-Fin (succ-ℕ n)) ( expand-term-binomial-exponential)) ∙ sum-equiv-finite-Ring ( ring-Rational-Extension-Ring R) ( Fin-Finite-Type (succ-ℕ n)) ( finite-type-binary-sum-decomposition-ℕ n) ( equiv-count-binary-sum-decomposition-ℕ n) ( expand-term-binomial-exponential) ∙ htpy-sum-finite-Ring ( ring-Rational-Extension-Ring R) ( finite-type-binary-sum-decomposition-ℕ n) ( htpy-interchange-expand-term-binomial-exponential) where term-xy : fin-sequence-type-Ring ( ring-Rational-Extension-Ring R) ( succ-ℕ n) term-xy i = mul-Rational-Extension-Ring R ( power-Ring ( ring-Rational-Extension-Ring R) ( nat-Fin (succ-ℕ n) i) ( x)) ( power-Ring ( ring-Rational-Extension-Ring R) ( dist-ℕ (nat-Fin (succ-ℕ n) i) n) ( y)) term-binomial-exponential : fin-sequence-type-Ring ( ring-Rational-Extension-Ring R) ( succ-ℕ n) term-binomial-exponential i = multiple-Ring ( ring-Rational-Extension-Ring R) ( binomial-coefficient-Fin n i) ( mul-Rational-Extension-Ring R ( coefficient-exponential-series-Rational-Extension-Ring R n) ( term-xy i)) expand-term-binomial-exponential : fin-sequence-type-Ring ( ring-Rational-Extension-Ring R) ( succ-ℕ n) expand-term-binomial-exponential i = mul-Rational-Extension-Ring R ( mul-Rational-Extension-Ring R ( coefficient-exponential-series-Rational-Extension-Ring R ( nat-Fin (succ-ℕ n) i)) ( coefficient-exponential-series-Rational-Extension-Ring R ( dist-ℕ (nat-Fin (succ-ℕ n) i) n))) ( term-xy i) htpy-expand-term-binomial-exponential : expand-term-binomial-exponential ~ term-binomial-exponential htpy-expand-term-binomial-exponential i = ap ( λ z → mul-Rational-Extension-Ring R z (term-xy i)) ( compute-mul-binomial-coefficient-exponential-series-Rational-Extension-Ring ( R) ( n) ( i)) ∙ left-mul-multiple-Ring ( ring-Rational-Extension-Ring R) ( binomial-coefficient-Fin n i) ( coefficient-exponential-series-Rational-Extension-Ring R n) ( term-xy i) htpy-interchange-expand-term-binomial-exponential : (ij@(i , j , K) : binary-sum-decomposition-ℕ n) → expand-term-binomial-exponential ( map-inv-equiv (equiv-count-binary-sum-decomposition-ℕ n) ij) ＝ mul-Rational-Extension-Ring R ( term-ev-exponential-series-Rational-Extension-Ring R x i) ( term-ev-exponential-series-Rational-Extension-Ring R y j) htpy-interchange-expand-term-binomial-exponential ij@(i , j , K) = binary-tr ( λ u v → expand-term-binomial-exponential idx ＝ mul-Rational-Extension-Ring R ( term-ev-exponential-series-Rational-Extension-Ring R x u) ( term-ev-exponential-series-Rational-Extension-Ring R y v)) ( lemma-i) ( ap (λ k → dist-ℕ k n) lemma-i ∙ inv (rewrite-left-add-dist-ℕ j i n K)) ( interchange-mul-term-exponential-series-Rational-Extension-Ring ( R) ( x) ( y) ( nat-Fin (succ-ℕ n) idx) ( dist-ℕ (nat-Fin (succ-ℕ n) idx) n)) where idx : Fin (succ-ℕ n) idx = map-inv-equiv (equiv-count-binary-sum-decomposition-ℕ n) ij lemma-i : nat-Fin (succ-ℕ n) idx ＝ i lemma-i = ap pr1 ( is-section-map-inv-equiv ( equiv-count-binary-sum-decomposition-ℕ n) ij)
Exponential series are invertible elements of the convolution ring
module _ {l : Level} (R : Rational-Extension-Ring l) (x : type-Rational-Extension-Ring R) where abstract htpy-left-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring : mul-convolution-sequence-Ring ( ring-Rational-Extension-Ring R) ( term-ev-exponential-series-Rational-Extension-Ring R ( neg-Ring (ring-Rational-Extension-Ring R) x)) ( term-ev-exponential-series-Rational-Extension-Ring R x) ~ one-Ring (convolution-sequence-Ring (ring-Rational-Extension-Ring R)) htpy-left-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring n = inv ( htpy-term-ev-add-mul-convolution-exponential-series-Rational-Extension-Ring ( R) ( neg-Ring (ring-Rational-Extension-Ring R) x) ( x) ( symmetric-commute-Ring ( ring-Rational-Extension-Ring R) ( x) ( neg-Ring (ring-Rational-Extension-Ring R) x) ( commute-neg-Ring ( ring-Rational-Extension-Ring R) ( refl-commute-Ring (ring-Rational-Extension-Ring R) x))) ( n)) ∙ ap ( λ u → term-ev-exponential-series-Rational-Extension-Ring R u n) ( left-inverse-law-add-Ring (ring-Rational-Extension-Ring R) x) ∙ htpy-term-ev-zero-exponential-series-Rational-Extension-Ring R n left-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring : mul-convolution-sequence-Ring ( ring-Rational-Extension-Ring R) ( term-ev-exponential-series-Rational-Extension-Ring R ( neg-Ring (ring-Rational-Extension-Ring R) x)) ( term-ev-exponential-series-Rational-Extension-Ring R x) ＝ one-Ring (convolution-sequence-Ring (ring-Rational-Extension-Ring R)) left-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring = eq-htpy htpy-left-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring htpy-right-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring : mul-convolution-sequence-Ring ( ring-Rational-Extension-Ring R) ( term-ev-exponential-series-Rational-Extension-Ring R x) ( term-ev-exponential-series-Rational-Extension-Ring R ( neg-Ring (ring-Rational-Extension-Ring R) x)) ~ one-Ring (convolution-sequence-Ring (ring-Rational-Extension-Ring R)) htpy-right-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring n = inv ( htpy-term-ev-add-mul-convolution-exponential-series-Rational-Extension-Ring ( R) ( x) ( neg-Ring (ring-Rational-Extension-Ring R) x) ( commute-neg-Ring ( ring-Rational-Extension-Ring R) ( refl-commute-Ring (ring-Rational-Extension-Ring R) x)) ( n)) ∙ ap ( λ u → term-ev-exponential-series-Rational-Extension-Ring R u n) ( right-inverse-law-add-Ring (ring-Rational-Extension-Ring R) x) ∙ htpy-term-ev-zero-exponential-series-Rational-Extension-Ring R n right-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring : mul-convolution-sequence-Ring ( ring-Rational-Extension-Ring R) ( term-ev-exponential-series-Rational-Extension-Ring R x) ( term-ev-exponential-series-Rational-Extension-Ring R ( neg-Ring (ring-Rational-Extension-Ring R) x)) ＝ one-Ring (convolution-sequence-Ring (ring-Rational-Extension-Ring R)) right-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring = eq-htpy htpy-right-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring is-invertible-mul-convolution-exponential-series-Rational-Extension-Ring : is-invertible-element-Ring ( convolution-sequence-Ring (ring-Rational-Extension-Ring R)) ( term-ev-exponential-series-Rational-Extension-Ring R x) pr1 is-invertible-mul-convolution-exponential-series-Rational-Extension-Ring = term-ev-exponential-series-Rational-Extension-Ring R ( neg-Ring (ring-Rational-Extension-Ring R) x) pr2 is-invertible-mul-convolution-exponential-series-Rational-Extension-Ring = ( right-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring , left-inverse-law-mul-convolution-exponential-series-Rational-Extension-Ring)
External links
- Natural exponential function at Wikidata
- exponential map at Lab
- Exponential function at Wikipedia
Recent changes
- 2026-09-18. malarbol. Exponential series in ring extensions of Q (#1996).