Commit 2024-07-21 22:30 1de6cfb6

View on Github →

feat(RingTheory/Localization): localization of algebra maps and commutation with kernels (#14086) Adds API for localizing algebra maps, in general form and specialized to IsLocalization.Away. Also shows that localization commutes with kernels.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/Algebra.lean

added def AlgHom.toKerIsLocalization

added theorem AlgHom.toKerIsLocalization_apply

added theorem AlgHom.toKerIsLocalization_isLocalizedModule

added theorem IsLocalization.ker_map

added theorem IsLocalization.mapₐ_coe

added theorem IsLocalization.mapₐ_injective_of_injective

added theorem IsLocalization.mapₐ_surjective_of_surjective

added def RingHom.toKerIsLocalization

added theorem RingHom.toKerIsLocalization_apply

added theorem RingHom.toKerIsLocalization_isLocalizedModule

Modified Mathlib/RingTheory/Localization/Finiteness.lean

added theorem Module.Finite.Ideal.fg_of_localizationSpan

added theorem Module.Finite.RingHom.ker_fg_of_localizationSpan