feat(RingTheory/Derivation/Basic): define lifting a derivation via an algebra homomorphism

[Command-Master]

---

[github-actions]

PR summary 4844c6d42c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ liftOfRightInverse
+ liftOfRightInverse_apply
+ liftOfSurjective
+ liftOfSurjective_apply

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[kbuzzard]

Looking at this PR, it's descending a derivation on A to a derivation on M along a surjection, and the descent (possibly) depends on an auxiliary set-theoretic section. Is it true that the construction is independent of the choice of section?

[Command-Master]

Apologies, I don't know those terms. Are you asking if the defined derivation is independent of which inverse is taken? It is, because if f a = f b then f (a - b) = 0 so by hd f (d (a - b)) = 0, or f (d a) = f (d b)