# Commit 2021-07-05 14:14 0b0d8e7e

View on Github →refactor(ring_theory): turn `localization_map`

into a typeclass (#8119)
This PR replaces the previous `localization_map (M : submodule R) Rₘ`

definition (a ring hom `R →+* Rₘ`

that presents `Rₘ`

as the localization of `R`

at `M`

) with a new `is_localization M Rₘ`

typeclass that puts these requirements on `algebra_map R Rₘ`

instead. An important benefit is that we no longer need to mess with `localization_map.codomain`

to put an `R`

-algebra structure on `Rₘ`

, we can just work with `Rₘ`

directly.
The important API changes are in commit 0de78dc, all other commits are simply fixes to the dependent files.
Main changes:

`localization_map`

has been replaced with`is_localization`

, similarly`away_map`

->`is_localization.away`

,`localization_map.at_prime`

->`is_localization.at_prime`

and`fraction_map`

->`is_fraction_ring`

- many declarations taking the
`localization_map`

as a parameter now take`R`

and/or`M`

and/or`Rₘ`

, depending on what can be inferred easily `localization_map.to_map`

has been replaced with`algebra_map R Rₘ`

`localization_map.codomain`

and its instances have been removed (you can now directly use`Rₘ`

)`is_localization.alg_equiv`

generalizes`fraction_map.alg_equiv_of_quotient`

(which has been renamed to`is_fraction_ring.alg_equiv`

)`is_localization.sec`

has been introduced to replace`(to_localization_map _ _).sec`

`localization.of`

have been replaced with`algebra`

and`is_localization`

instances on`localization`

, similarly for`localization.away.of`

,`localization.at_prime.of`

and`fraction_ring.of`

.`int.fraction_map`

is now an instance`rat.is_fraction_ring`

- All files depending on the above definitions have had fixes. These were mostly straightforward, except:
- Some category-theory arrows in
`algebraic_geometry/structure.sheaf`

are now plain`ring_hom`

s. This change was suggested by @justus-springer in order to help the elaborator figure out the arguments to`is_localization`

. - Deleted
`minpoly.over_int_eq_over_rat`

and`minpoly.integer_dvd`

, now you can just use`gcd_domain_eq_field_fractions`

or`gcd_domain_dvd`

respectively. This removes code duplication in`minpoly.lean`

`fractional_ideal`

does not need to assume`is_localization`

everywhere, only for certain specific definitions Things that stay the same:`localization`

,`localization.away`

,`localization.at_prime`

and`fraction_ring`

are still a construction of localizations (although see above for`{localization,localization.away,localization.at_prime,fraction_ring}.of`

) Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Refactoring.20.60localization_map.60