Commit 2026-03-22 21:51 87f8e604

feat: compatible (pairs of) derivations form a Lie algebra (#36651) Given a map of $R$-algebras $\sigma: A\to A'$, a derivation $X$ of $A$ is called compatible with a Derivation $X'$ of $A'$, if $\sigma\circ X =X'\circ \sigma$. Given two such pairs $(X,X')$ and $(Y,Y')$, their Lie brackets $([X,Y], [X',Y'])$ again form such a pair. This concept is relevant in differential geometry, where $A$, $A'$ are the algebras of smooth functions on manifolds and $\sigma$ comes from a smooth map between manifolds. (In this case one calls the vector fields (= Derivations) 'related'). This concept can be encoded by the fact that the compatible Derivations form a Lie subalgebra of the direct sum of the derivations of $A$ with the derivations of $A'$. In this PR we add this fact, along with a convenient way to express the direct sum of two Lie algebras, as a special case of their semidirect sum. (There already is a direct sum construction for aribtrary families of Lie algebras in Mathlib.Algebra.Lie.DirectSum), but I don't know if there is a very convenient way to use it in the binary case.