Commit 2025-12-05 10:18 e92873e3

View on Github →

chore(Algebra): extract Submonoid.IsLocalizationMap (#29596)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/FinitePresentation.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

added structure AddSubmonoid.IsLocalizationMap

modified structure AddSubmonoid.LocalizationMap

added theorem AddSubmonoid.isLocalizationMap_nat_int

added theorem AddSubmonoid.isLocalizationMap_top_nat_int

added theorem Submonoid.IsLocalizationMap.mulEquiv_comp

added structure Submonoid.IsLocalizationMap

added theorem Submonoid.LocalizationMap.exists_of_eq

added theorem Submonoid.LocalizationMap.map_injective_of_surjOn_or_injective

added theorem Submonoid.LocalizationMap.map_surjective_of_surjOn

added theorem Submonoid.LocalizationMap.subsingleton_of_subsingleton

modified structure Submonoid.LocalizationMap

added theorem Submonoid.isLocalizationMap_id

added theorem Submonoid.isLocalizationMap_iff_bijective

added theorem Submonoid.isLocalizationMap_of_group

Created Mathlib/GroupTheory/MonoidLocalization/Lemmas.lean

added theorem Submonoid.IsLocalizationMap.surj_pi_of_finite

Modified Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean

modified theorem Submonoid.LocalizationMap.subsingleton

deleted def Submonoid.LocalizationMap.toMonoidWithZeroHom

Modified Mathlib/RingTheory/EssentialFiniteness.lean

Modified Mathlib/RingTheory/Extension/Presentation/Submersive.lean

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/Localization/Defs.lean

added theorem IsLocalization.exists_of_eq

modified theorem IsLocalization.injective_iff_isRegular

added theorem IsLocalization.map_units

added theorem IsLocalization.surj

added theorem isLocalization_iff

added theorem isLocalization_iff_isLocalizationMap

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Modified Mathlib/RingTheory/Valuation/ValuationRing.lean