feat(RingTheory/Localization): localization of algebra maps and commutation with kernels

[chrisflav]

Adds API for localizing algebra maps, in general form and specialized to IsLocalization.Away. Also shows that localization commutes with kernels.

---

[github-actions[bot]]

PR summary 6767595b30

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Localization.Finiteness	1
Mathlib.RingTheory.Localization.Algebra	948

---

Declarations diff

+ AlgHom.toKerIsLocalization + AlgHom.toKerIsLocalization_apply + AlgHom.toKerIsLocalization_isLocalizedModule + Algebra.idealMap_isLocalizedModule + IsLocalization.ker_map + RingHom.ker_fg_of_localizationSpan + RingHom.toKerIsLocalization + RingHom.toKerIsLocalization_apply + RingHom.toKerIsLocalization_isLocalizedModule + fg_of_localizationSpan + isLocalization_algebraMapSubmonoid_map_algHom + mapₐ + mapₐ_coe + mapₐ_injective_of_injective + mapₐ_surjective_of_surjective

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>

[erdOne]

Sorry forgot about this PR. Please merge master in case the localization refactor causes some conflicts.

[chrisflav]

Anything else I should address? @erdOne

[chrisflav]

I opened #14751 with the changes to the two files removed.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#14751~~ By Dependent Issues (🤖). Happy coding!

[erdOne]

Thanks! maintainer merge

[github-actions[bot]]

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

[kim-em]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style