Commit 2021-07-05 14:14 0b0d8e7e

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_homs. 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