mathlib

0b0d8e7e - refactor(ring_theory): turn `localization_map` into a typeclass (#8119)

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`.](https://github.com/leanprover-community/mathlib/commit/cf3acc925467cc06237a13dbe4264529f9a58850) * 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`](https://github.com/leanprover-community/mathlib/commit/5695924d85710f98ac60a7df91d7dbf27408ca26) * `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