Derivations vanish on idempotents #
Every derivation of a commutative ring kills its idempotents: differentiating e = e² gives
D e = 2 e • D e, and multiplying by e then shows e • D e = 0.
Geometrically, an idempotent is locally constant on the spectrum, so its differential vanishes. For an affine group, this says that a tangent vector at the identity does not see the other connected components.
theorem
Derivation.apply_eq_zero_of_isIdempotentElem
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommSemiring R]
[CommRing A]
[Algebra R A]
[AddCommGroup M]
[Module A M]
[Module R M]
(D : Derivation R A M)
{e : A}
(he : IsIdempotentElem e)
:
A derivation vanishes on every idempotent.