Exponential map on algebras

This file defines the exponential map IsNilpotent.exp on ℚ-algebras. The definition of IsNilpotent.exp a applies to any element a in an algebra over ℚ, though it yields meaningful (non-junk) values only when a is nilpotent.

The main result is IsNilpotent.exp_add_of_commute, which establishes the expected connection between the additive and multiplicative structures of A for commuting nilpotent elements.

Additionally, IsNilpotent.exp_of_nilpotent_is_unit shows that if a is nilpotent in A, then IsNilpotent.exp a is a unit in A.

Note: Although the definition works with ℚ-algebras, the results can be applied to any algebra over a characteristic zero field.

Main definitions

• IsNilpotent.exp

Tags

algebra, exponential map, nilpotent

noncomputable def IsNilpotent.exp {A : Type u_1} [Ring A] [Algebra ℚ A] (a : A) : A

The exponential map on algebras, defined in analogy with the usual exponential series. It provides meaningful (non-junk) values for nilpotent elements.

Equations

• IsNilpotent.exp a = ∑ i ∈ Finset.range (nilpotencyClass a), (↑i.factorial)⁻¹ • a ^ i

theorem IsNilpotent.exp_eq_truncated {A : Type u_1} [Ring A] [Algebra ℚ A] {a : A} {k : ℕ} (h : a ^ k = 0) : ∑ i ∈ Finset.range k, (↑i.factorial)⁻¹ • a ^ i = exp a

theorem IsNilpotent.exp_zero_eq_one {A : Type u_1} [Ring A] [Algebra ℚ A] : exp 0 = 1

theorem IsNilpotent.exp_add_of_commute {A : Type u_1} [Ring A] [Algebra ℚ A] {a b : A} (h₁ : Commute a b) (h₂ : IsNilpotent a) (h₃ : IsNilpotent b) : exp (a + b) = exp a * exp b

theorem IsNilpotent.exp_of_nilpotent_is_unit {A : Type u_1} [Ring A] [Algebra ℚ A] {a : A} (h : IsNilpotent a) : IsUnit (exp a)