Integral exponentials of nilpotent Lie derivations

Let D be a nilpotent derivation of a Lie algebra over ℚ, and let an integral Lie subalgebra be stable under every divided power Dⁿ / n!. The restricted divided powers obey the coefficient-free Leibniz rule. Consequently their finite exponential preserves the Lie bracket after scalar extension to an arbitrary commutative ring, even when factorials are not invertible in that ring.

Main declarations

• LieDerivation.dividedPower_apply_lie: coefficient-free divided-power Leibniz rule.
• TauCeti.integralDividedPower_lie: the rule on the integral Lie subalgebra.
• TauCeti.baseChangeExp_lie: bracket preservation after arbitrary base change.
• TauCeti.baseChangeExpLieEquiv: the resulting Lie algebra automorphism.

theorem LieDerivation.dividedPower_apply_lie {L : Type u} [LieRing L] [LieAlgebra ℚ L] (D : LieDerivation ℚ L L) (n : ℕ) (x y : L) : (TauCeti.Associative.dividedPower n ↑D) ⁅x, y⁆ = ∑ ij ∈ Finset.antidiagonal n, ⁅(TauCeti.Associative.dividedPower ij.1 ↑D) x, (TauCeti.Associative.dividedPower ij.2 ↑D) y⁆

Divided powers of a Lie derivation satisfy the coefficient-free divided-power Leibniz rule.

theorem TauCeti.integralDividedPower_lie {L : Type u} [LieRing L] [LieAlgebra ℚ L] (D : LieDerivation ℚ L L) (M : LieSubalgebra ℤ L) (hM : ∀ (n : ℕ), ∀ x ∈ M, (Associative.dividedPower n ↑D) x ∈ M) (n : ℕ) (x y : ↥M) : (integralDividedPower (↑D) M n ⋯) ⁅x, y⁆ = ∑ ij ∈ Finset.antidiagonal n, ⁅(integralDividedPower (↑D) M ij.1 ⋯) x, (integralDividedPower (↑D) M ij.2 ⋯) y⁆

Restricted integral divided powers inherit the coefficient-free Leibniz rule.

theorem TauCeti.baseChangeExp_lie {L : Type u} [LieRing L] [LieAlgebra ℚ L] {R : Type v} [CommRing R] [Algebra ℤ R] (D : LieDerivation ℚ L L) (M : LieSubalgebra ℤ L) (hM : ∀ (n : ℕ), ∀ x ∈ M, (Associative.dividedPower n ↑D) x ∈ M) (hD : IsNilpotent ↑D) (t : R) (x y : TensorProduct ℤ R ↥M) : (baseChangeExp (↑D) M hM t) ⁅x, y⁆ = ⁅(baseChangeExp (↑D) M hM t) x, (baseChangeExp (↑D) M hM t) y⁆

The integral divided-power exponential preserves the Lie bracket after an arbitrary base change. No finite-dimensionality, flatness, or characteristic assumption is needed on the new base ring.

noncomputable def TauCeti.baseChangeExpLieEquiv {L : Type u} [LieRing L] [LieAlgebra ℚ L] {R : Type v} [CommRing R] [Algebra ℤ R] (D : LieDerivation ℚ L L) (M : LieSubalgebra ℤ L) (hM : ∀ (n : ℕ), ∀ x ∈ M, (Associative.dividedPower n ↑D) x ∈ M) (hD : IsNilpotent ↑D) (t : R) : TensorProduct ℤ R ↥M ≃ₗ⁅R⁆ TensorProduct ℤ R ↥M

The integral divided-power exponential of a nilpotent Lie derivation, after arbitrary base change, as a Lie algebra automorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.baseChangeExpLieEquiv_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {R : Type v} [CommRing R] [Algebra ℤ R] (D : LieDerivation ℚ L L) (M : LieSubalgebra ℤ L) (hM : ∀ (n : ℕ), ∀ x ∈ M, (Associative.dividedPower n ↑D) x ∈ M) (hD : IsNilpotent ↑D) (t : R) (x : TensorProduct ℤ R ↥M) : (baseChangeExpLieEquiv D M hM hD t) x = (baseChangeExp (↑D) M hM t) x

The underlying action of the base-changed Lie exponential is the existing divided-power exponential.

@[simp]

theorem TauCeti.baseChangeExpLieEquiv_zero {L : Type u} [LieRing L] [LieAlgebra ℚ L] {R : Type v} [CommRing R] [Algebra ℤ R] (D : LieDerivation ℚ L L) (M : LieSubalgebra ℤ L) (hM : ∀ (n : ℕ), ∀ x ∈ M, (Associative.dividedPower n ↑D) x ∈ M) (hD : IsNilpotent ↑D) : baseChangeExpLieEquiv D M hM hD 0 = LieEquiv.refl

The Lie exponential at zero is the identity automorphism.

@[simp]

theorem TauCeti.baseChangeExpLieEquiv_trans {L : Type u} [LieRing L] [LieAlgebra ℚ L] {R : Type v} [CommRing R] [Algebra ℤ R] (D : LieDerivation ℚ L L) (M : LieSubalgebra ℤ L) (hM : ∀ (n : ℕ), ∀ x ∈ M, (Associative.dividedPower n ↑D) x ∈ M) (hD : IsNilpotent ↑D) (t u : R) : (baseChangeExpLieEquiv D M hM hD t).trans (baseChangeExpLieEquiv D M hM hD u) = baseChangeExpLieEquiv D M hM hD (t + u)

Lie exponentials compose by adding their parameters.

@[simp]

theorem TauCeti.baseChangeExpLieEquiv_symm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {R : Type v} [CommRing R] [Algebra ℤ R] (D : LieDerivation ℚ L L) (M : LieSubalgebra ℤ L) (hM : ∀ (n : ℕ), ∀ x ∈ M, (Associative.dividedPower n ↑D) x ∈ M) (hD : IsNilpotent ↑D) (t : R) : (baseChangeExpLieEquiv D M hM hD t).symm = baseChangeExpLieEquiv D M hM hD (-t)

The inverse of a Lie exponential is the exponential at the negative parameter.