Commit 2024-07-15 10:42 ba693824

View on Github →

feat(RingTheory/Localization): more API and kernels of localized maps (#14751) This PR adds various API lemmas on localization. In particular it computes the kernel of a localized map as the localization of the kernel.

Estimated changes

Modified Mathlib/Algebra/Algebra/Hom.lean

added theorem Algebra.algebraMapSubmonoid_le_comap

added theorem Algebra.algebraMapSubmonoid_map_eq

Modified Mathlib/Algebra/Module/LocalizedModule.lean

added theorem IsLocalizedModule.map_mk'

Modified Mathlib/Algebra/Module/Submodule/Localization.lean

added theorem LinearMap.ker_localizedMap_eq_localized'_ker

added theorem LinearMap.localized'_ker_eq_ker_localizedMap

added theorem LinearMap.toKerLocalized_isLocalizedModule

added theorem Submodule.mem_localized'

Modified Mathlib/GroupTheory/MonoidLocalization.lean

added theorem Submonoid.LocalizationMap.map_surjective_of_surjective

Modified Mathlib/RingTheory/Ideal/Maps.lean

added def Algebra.idealMap

Modified Mathlib/RingTheory/Localization/Away/Basic.lean

added theorem IsLocalization.Away.mapₐ_apply

added theorem IsLocalization.Away.mapₐ_injective_of_injective

added theorem IsLocalization.Away.mapₐ_surjective_of_surjective

Modified Mathlib/RingTheory/Localization/Basic.lean

added theorem IsLocalization.map_surjective_of_surjective

Modified Mathlib/RingTheory/Localization/Ideal.lean

added theorem IsLocalization.mk'_mem_map_algebraMap_iff

Modified Mathlib/RingTheory/Localization/Module.lean

added theorem LinearMap.extendScalarsOfIsLocalization_apply'