[Merged by Bors] - refactor(ring_theory): turn `localization_map` into a typeclass #8119

Vierkantor · 2021-06-29T14:10:11Z

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

src/ring_theory/localization.lean

src/field_theory/minpoly.lean

…e `algebra_map`

With this refactor, you can just use the general statement for fields of fractions

…al ideals

Co-Authored-By: Johan Commelin <johan@commelin.net>

jcommelin

Thanks! This is looking very very good.

src/ring_theory/localization.lean

From a quick grepping it seems `sec` is not used outside of this file

jcommelin

Thanks 🎉 (let's wait for CI)

bors d+

bors · 2021-07-05T12:44:03Z

✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Vierkantor · 2021-07-05T14:13:46Z

bors r+

@justus-springer

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`.](cf3acc9) * 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`](5695924) * `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

bors · 2021-07-05T14:57:46Z

Pull request successfully merged into master.

Build succeeded:

@justus-springer

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`.](cf3acc9) * 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`](5695924) * `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

Vierkantor added the WIP Work in progress label Jun 29, 2021

jcommelin reviewed Jun 29, 2021

View reviewed changes

src/ring_theory/localization.lean Outdated Show resolved Hide resolved

riccardobrasca reviewed Jun 29, 2021

View reviewed changes

src/field_theory/minpoly.lean Outdated Show resolved Hide resolved

Vierkantor added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Jun 30, 2021

Vierkantor and others added 25 commits July 5, 2021 10:11

refactor(ring_theory): turn localization_map into a predicate on th…

cf456ba

…e `algebra_map`

Change arguments to map

40fb3bb

Fix polynomial/gauss_lemma.lean

cae7c79

Fix minpoly.lean

103a4c0

Fix fractional_ideal.lean

203427b

Fix rational_root.lean

8b99673

Fix dickson.lean

4d5457c

Fix ideal/over.lean

1ee8154

WIP

8bd39b6

Fix dedekind_domain.lean

27b672d

Fix algebra/char_p/algebra.lean

8b620d6

Fix

1df1326

Fix structure_sheaf.lean

40579e3

Fix dickson.lean

97f7a60

Fix cyclotomic.lean

3b1f0f4

WIP

0e51705

Fix laurent_series.lean

e1649dc

Fix jacobson.lean

a5de4fe

Fix db files

2be0328

Inline minpoly.{over_int_eq_over_rat,integer_gcd}

225d691

With this refactor, you can just use the general statement for fields of fractions

Lint fix: don't need to assume is_localization for much of fraction…

2faf310

…al ideals

Lint fix: turn these unusable instances into lemmas

0ca7c0a

Lint fix: overlong lines (and a bit of golfing)

729c377

Typo fix: o -> To

02551fe

Co-Authored-By: Johan Commelin <johan@commelin.net>

Don't need this instance

40989d4

Vierkantor requested a review from jcommelin July 5, 2021 10:29

jcommelin reviewed Jul 5, 2021

View reviewed changes

src/ring_theory/localization.lean Outdated Show resolved Hide resolved

Fix docstring

a96dfc9

Vierkantor force-pushed the localization_typeclass branch from 7ee286f to a96dfc9 Compare July 5, 2021 11:46

Define is_localization.sec

7e37591

From a quick grepping it seems `sec` is not used outside of this file

jcommelin approved these changes Jul 5, 2021

View reviewed changes

github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 5, 2021

adamtopaz mentioned this pull request Jul 5, 2021

[Merged by Bors] - feat(category_theory/abelian/ext): Defines Ext functors. #8186

Closed

2 tasks

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jul 5, 2021

bors bot changed the title ~~refactor(ring_theory): turn localization_map into a typeclass~~ [Merged by Bors] - refactor(ring_theory): turn localization_map into a typeclass Jul 5, 2021

bors bot closed this Jul 5, 2021

bors bot deleted the localization_typeclass branch July 5, 2021 14:57

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(ring_theory): turn `localization_map` into a typeclass #8119

[Merged by Bors] - refactor(ring_theory): turn `localization_map` into a typeclass #8119

Vierkantor commented Jun 29, 2021 •

edited

jcommelin left a comment

jcommelin left a comment

bors bot commented Jul 5, 2021

Vierkantor commented Jul 5, 2021

bors bot commented Jul 5, 2021

[Merged by Bors] - refactor(ring_theory): turn localization_map into a typeclass #8119

[Merged by Bors] - refactor(ring_theory): turn localization_map into a typeclass #8119

Conversation

Vierkantor commented Jun 29, 2021 • edited

jcommelin left a comment

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Jul 5, 2021

Vierkantor commented Jul 5, 2021

bors bot commented Jul 5, 2021

[Merged by Bors] - refactor(ring_theory): turn `localization_map` into a typeclass #8119

[Merged by Bors] - refactor(ring_theory): turn `localization_map` into a typeclass #8119

Vierkantor commented Jun 29, 2021 •

edited