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.isUnit_exp 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] [Module ℚ 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_sum {A : Type u_1} [Ring A] [Module ℚ A] {a : A} {k : ℕ} (h : a ^ k = 0) : exp a = ∑ i ∈ Finset.range k, (↑i.factorial)⁻¹ • a ^ i

theorem IsNilpotent.exp_smul_eq_sum {A : Type u_1} [Ring A] [Module ℚ A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module ℚ M] {a : A} {m : M} {k : ℕ} (h : a ^ k • m = 0) (hn : IsNilpotent a) : exp a • m = ∑ i ∈ Finset.range k, (↑i.factorial)⁻¹ • a ^ i • m

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

@[simp]

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

theorem IsNilpotent.exp_mul_exp_neg_self {A : Type u_1} [Ring A] [Module ℚ A] {a : A} (h : IsNilpotent a) : exp a * exp (-a) = 1

theorem IsNilpotent.exp_neg_mul_exp_self {A : Type u_1} [Ring A] [Module ℚ A] {a : A} (h : IsNilpotent a) : exp (-a) * exp a = 1

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

@[deprecated IsNilpotent.isUnit_exp (since := "2025-03-11")]

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

Alias of IsNilpotent.isUnit_exp.

theorem IsNilpotent.map_exp {A : Type u_1} [Ring A] [Module ℚ A] {B : Type u_2} {F : Type u_3} [Ring B] [FunLike F A B] [RingHomClass F A B] [Module ℚ B] {a : A} (ha : IsNilpotent a) (f : F) : f (exp a) = exp (f a)

theorem IsNilpotent.exp_smul {A : Type u_1} [Ring A] [Module ℚ A] {G : Type u_2} [Monoid G] [MulSemiringAction G A] (g : G) {a : A} (ha : IsNilpotent a) : exp (g • a) = g • exp a

theorem Module.End.commute_exp_left_of_commute {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module ℚ M] [Module ℚ N] {fM : End R M} {fN : End R N} {g : M →ₗ[R] N} (hfM : IsNilpotent fM) (hfN : IsNilpotent fN) (h : fN ∘ₗ g = g ∘ₗ fM) : IsNilpotent.exp fN ∘ₗ g = g ∘ₗ IsNilpotent.exp fM

theorem Module.End.exp_mul_of_derivation (R : Type u_4) (B : Type u_5) [CommRing R] [NonUnitalNonAssocRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [Module ℚ B] (D : B →ₗ[R] B) (h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y) (h_nil : IsNilpotent D) (x y : B) : (IsNilpotent.exp D) (x * y) = (IsNilpotent.exp D) x * (IsNilpotent.exp D) y