Derivations and powers of ideals

A derivation that preserves two ideals also preserves their product: the Leibniz rule places its two summands in the product by differentiating one factor at a time. Consequently, a derivation preserving an ideal preserves every power of that ideal.

The stronger condition that the whole range of a derivation lies in an ideal automatically gives the required stability: a derivation taking values in an ideal I preserves every power I ^ n. An ideal here is a left ideal; when I is moreover two-sided, so is each I ^ n, and the derivation then descends to the quotient by that power along Ado.derivationQuotientHom.

Main results

• Ado.mem_stableDerivations_mul: a derivation preserving two ideals preserves their product.
• Ado.mem_stableDerivations_pow: a derivation preserving an ideal preserves all its powers.
• Ado.mem_stableDerivations_pow_of_range_le: if the range of a derivation lies in an ideal, every power of that ideal is stable under the derivation.

Implementation notes

Stability is phrased throughout as membership in the Lie subalgebra Ado.stableDerivations, the form in which Ado.derivationQuotientHom consumes it, rather than as a bare Set.MapsTo. The stabilizer is indexed by a submodule over the base ring, so an ideal I of A enters it as I.restrictScalars R.

theorem Ado.mem_stableDerivations_mul (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] {D : ↥(derivationLieAlgebra R A)} {I J : Ideal A} (hI : D ∈ stableDerivations R (Submodule.restrictScalars R I)) (hJ : D ∈ stableDerivations R (Submodule.restrictScalars R J)) : D ∈ stableDerivations R (Submodule.restrictScalars R (I * J))

A derivation preserving two ideals preserves their product.

theorem Ado.mem_stableDerivations_pow (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] {D : ↥(derivationLieAlgebra R A)} {I : Ideal A} (hI : D ∈ stableDerivations R (Submodule.restrictScalars R I)) (n : ℕ) : D ∈ stableDerivations R (Submodule.restrictScalars R (I ^ n))

A derivation preserving an ideal preserves each power of that ideal.

theorem Ado.mem_stableDerivations_pow_of_range_le (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] {D : ↥(derivationLieAlgebra R A)} {I : Ideal A} (hD : LinearMap.range ↑D ≤ Submodule.restrictScalars R I) (n : ℕ) : D ∈ stableDerivations R (Submodule.restrictScalars R (I ^ n))

If the range of a derivation lies in an ideal, then every power of that ideal is stable under the derivation.