[Merged by Bors] - feat: differentials as an object in ModuleCat

[joelriou]

In this PR, given a morphism f : A ⟶ B in the category CommRingCat, and M : ModuleCat B, we define the type M.Derivation f of derivations with values in M relative to f. We also construct the module of differentials CommRingCat.KaehlerDifferential f : ModuleCat B and the corresponding derivation. (These are basically "bundled" versions of the unbundled constructions already in mathlib.)

---

This is extended to presheaves of modules in #14014.

[github-actions]

PR summary 22a9b26562

Import changes

No significant changes to the import graph

---

Declarations diff

+ D
+ Derivation
+ KaehlerDifferential
+ SMulCommClass.of_commMonoid
+ d
+ d_add
+ d_map
+ d_mul
+ desc
+ desc_d
+ ext
+ map
+ map_d
+ mk

You can run this locally as follows

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

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

[joelriou]

Thanks @erdOne for the reviews. I could not make certain definitions global instances (because it would break other parts on mathlib), but by declaring them as a local instance in the main file, it works fine.

[erdOne]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style