Documentation

Mathlib.RingTheory.Nilpotent.Exp

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 #

Tags #

algebra, exponential map, nilpotent

source
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
    Instances For
      source
      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
      source
      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
      source
      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
      source
      @[simp]
      theorem IsNilpotent.exp_zero {A : Type u_1} [Ring A] [Module ℚ A] :
      exp 0 = 1
      source
      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
      source
      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
      source
      theorem IsNilpotent.isUnit_exp {A : Type u_1} [Ring A] [Module ℚ A] {a : A} (h : IsNilpotent a) :
      IsUnit (exp a)
      source
      @[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.

      source
      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)
      source
      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
      source
      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
      source
      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