chore(RingTheory/Localization): golfs and generalizations

[alreadydone]

• In RingTheory/LocalProperties/Basic: add some lemmas connecting localization of submodules and localization of ideals, and use results about the former to golf results about the latter.

• In RingTheory/Localization/Module: golf a proof using the recently introduced IsLocalization.linearMap_compatibleSMul.

• In Algebra/Module/Projective, Algebra/Module/LocalizedModule/IsLocalization, RingTheory/Localization/Submodule: generalize from AddCommGroup/CommRing to AddCommMonoid/CommSemiring. Also golf a lemma statement in the second file.

• RingTheory/Localization/Algebra, RingTheory/Localization/Ideal: add two TODOs that are not done here for import reasons.

---

Originally in #19118

[github-actions]

PR summary bbf202a522

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.LocalProperties.Basic	1314	1315	+1 (+0.08%)

Import changes for all files

Files	Import difference
57 files Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.Localization.Finiteness Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Finite Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Pullbacks Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.RingTheory.RingHom.Integral Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.RingTheory.Localization.Free Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.Trace.Quotient Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.RingTheory.LocalProperties.Reduced Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.AlgebraicGeometry.Stalk Mathlib.RingTheory.LocalProperties.Basic Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.RingTheory.RingHom.Surjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.Etale	1
23 files Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.Cyclotomic.Three Mathlib.RingTheory.Unramified.Field Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.RingTheory.DedekindDomain.Different Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.RingTheory.DedekindDomain.PID Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.AdeleRing	2

---

Declarations diff

+ Algebra.idealMap_eq_ofEq_comp_toLocalized₀
+ Ideal.localized'_eq_map
+ Ideal.localized₀_eq_restrictScalars_map
+ Ideal.mem_of_localization_maximal
+ instance {A} [CommSemiring A] [Algebra R A] [IsLocalization S A] :
- instance {A} [CommRing A] [Algebra R A] [IsLocalization S A] :

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
1557	-1	erw

Current commit bbf202a522
Reference commit 961ee9dbff

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).