[Merged by Bors] - feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations by maddycrim · Pull Request #19042 · leanprover-community/mathlib4

maddycrim · 2024-11-14T18:03:40Z

For lemma isUnit_piRingHom_algebraMap_comp_piEvalRingHom : Let M be a submonoid of a direct product of commutative rings R i, and let M' i denote the projection of M onto each corresponding factor. Given a ring homomorphism from the direct product Π i, R i to the product of the localizations of each R i at M' i, every y : M maps to a unit under this homomorphism.

For theorem bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom : Let M be a submonoid of a direct product of commutative rings R i, and let M' i denote the projection of M onto each factor. Then the canonical map from the localization of the direct product Π i, R i at M to the direct product of the localizations of each R i at M' i is bijective.

Co-authored-by: Yongle Hu <2065545849@qq.com>

Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

alreadydone · 2024-12-23T14:07:25Z

What I said in the previous two comments are true but not the optimal way to refactor the result; I've now done a refactoring in this branch; please merge if it looks good to you. I did prove that a product of localizations is a localization w.r.t. the product submonoid, and I upgraded the main result from injectivity to bijectivity, because the saturation of a submonoid in a finite product is exactly the product of all its projections. I also renamed @maddycrim's two original results to better conform to mathlib naming conventions, and changed the variable names R' S' S to R S S'. If you agree with the renaming please also update the PR message (at the top of this PR).

@jcommelin assigned this to me but I'm no longer comfortable approving this myself, so maybe @kim-em could take another look.

Mathlib/RingTheory/Localization/Pi.lean

kim-em · 2025-01-11T03:39:40Z

@maddycrim, if I understand correctly the ball is in your court on this one. I'll mark awaiting-author, but please ping @alreadydone or myself on Zulip if that's not the case.

* refactor * replace ∀ by Π wherever appropriate * module docstring * shake --------- Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

github-actions · 2025-01-23T21:14:55Z

PR summary be65509fd6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Localization.Pi` (new file)	842

Declarations diff

+ bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom
+ iff_map_piEvalRingHom
+ iff_of_le_of_exists_dvd
+ instance (M : Π i, Submonoid (R i)) [∀ i, IsLocalization (M i) (S i)] :
+ instance (g : I → Type*) [∀ i, CommSemiring (f i)] [∀ i, Semiring (g i)]
+ isUnit_piRingHom_algebraMap_comp_piEvalRingHom

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.

No changes to technical debt.

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

Mathlib/Algebra/Group/Invertible/Basic.lean

kim-em · 2025-01-28T01:20:53Z

bors merge

…duct is a product of localizations (#19042) For lemma ` isUnit_piRingHom_algebraMap_comp_piEvalRingHom` : Let `M` be a submonoid of a direct product of commutative rings `R i`, and let `M' i` denote the projection of `M` onto each corresponding factor. Given a ring homomorphism from the direct product `Π i, R i` to the product of the localizations of each `R i` at `M' i`, every `y : M` maps to a unit under this homomorphism. For theorem `bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom` : Let `M` be a submonoid of a direct product of commutative rings `R i`, and let `M' i` denote the projection of `M` onto each factor. Then the canonical map from the localization of the direct product `Π i, R i` at `M` to the direct product of the localizations of each `R i` at `M' i` is bijective. Co-authored-by: maddycrim <maddycrim84@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Madison Crim <maddycrim84@gmail.com>

mathlib-bors · 2025-01-28T02:04:33Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (294 commits) feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084) feat: separating set in the category of ind-objects (#21082) feat: derivWithin lemmas (#21092) chore(Fintype): golf a proof (#21113) chore: golf using `funext₂` (#21106) chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067) doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations (#21101) doc(ComputeDegree): typos (#21095) ...

* polynomial-sequences: (308 commits) Use the lemma we already added. Minor reordering. This is true even for the trivial ring. Also add the lt versions and the other inj lemma. Also add the basis ne versions. This seems also like it should be simp. Back to sorry free. And the natDegree version. feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) ...

maddycrim and others added 27 commits October 8, 2024 13:57

Adding theorem

34f9122

Apply suggestions from code review

98c8fef

Co-authored-by: Yongle Hu <2065545849@qq.com>

add changes

3bf5571

add instance nilradmaxLocalRing

88b45ab

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

fd626c9

Co-authored-by: Yongle Hu <2065545849@qq.com>

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

67f4ed7

Co-authored-by: Yongle Hu <2065545849@qq.com>

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

b071d27

Co-authored-by: Yongle Hu <2065545849@qq.com>

Increase heartbeat limit to resolve timeout

6c006e8

Increase heartbeat limit to resolve timeout

f7544fa

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

069cf3a

Co-authored-by: Yongle Hu <2065545849@qq.com>

Fixing issue with lean build

93a589d

add heartbeat to resolve timeout error

0cd0276

adding heartbeat

5b71b37

Update Mathlib/RingTheory/Nullstellensatz.lean

c8b95af

Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

2e1336f

Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

16aa1ab

Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>

Merge branch 'master' into MC_localization

984f207

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

d754b08

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

1d7806f

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

fcc2026

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

037ace6

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

fixing error after adding change

c6c8da1

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

d77e334

Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

3bcbef8

Merge branch 'master' into MC_localization

79ebde2

fix merge conflict

1ae98e9

add lemma and theorem

3321366

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc) labels Nov 14, 2024

fix := issue

252c062

alreadydone added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 5, 2024

maddycrim added 5 commits December 5, 2024 16:24

add new file, make changes

d503a4f

merge master

a2f8798

run lake exe mk_all

bfca1f9

fix issue in docstring

5b7f74b

fix imports

c48d19a

maddycrim removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 5, 2024

alreadydone reviewed Dec 23, 2024

View reviewed changes

Mathlib/RingTheory/Localization/Pi.lean Outdated Show resolved Hide resolved

alreadydone changed the title ~~feat(RingTheory/Localization/Defs): localization of a direct product injects into product of localizations~~ feat(RingTheory/Localization/Defs): localization of a finite direct product is a product of localizations Dec 23, 2024

alreadydone changed the title ~~feat(RingTheory/Localization/Defs): localization of a finite direct product is a product of localizations~~ feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations Dec 23, 2024

alreadydone mentioned this pull request Dec 28, 2024

[Merged by Bors] - feat(Algebra/Group): Units in pi types #20279

Closed

kim-em added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 11, 2025

Mc products refactor (#20997)

27be9a7

* refactor * replace ∀ by Π wherever appropriate * module docstring * shake --------- Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

maddycrim removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 23, 2025

Merge branch 'master' into MC_products

e7687a3

alreadydone reviewed Jan 23, 2025

View reviewed changes

Mathlib/Algebra/Group/Invertible/Basic.lean Outdated Show resolved Hide resolved

alreadydone and others added 2 commits January 23, 2025 16:17

Discard changes to Mathlib/Algebra/Group/Invertible/Basic.lean

0e35a3e

change toRingHom to algebraMap and add library

be65509

ghost added the ready-to-merge This PR has been sent to bors. label Jan 28, 2025

mathlib-bors bot changed the title ~~feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations~~ [Merged by Bors] - feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations Jan 28, 2025

mathlib-bors bot closed this Jan 28, 2025

mathlib-bors bot deleted the MC_products branch January 28, 2025 02:04

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations#19042

[Merged by Bors] - feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations#19042
maddycrim wants to merge 55 commits intomasterfrom
MC_products

maddycrim commented Nov 14, 2024 •

edited

Loading

Uh oh!

alreadydone commented Dec 23, 2024 •

edited

Loading

Uh oh!

Uh oh!

kim-em commented Jan 11, 2025

Uh oh!

github-actions bot commented Jan 23, 2025 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

kim-em commented Jan 28, 2025

Uh oh!

mathlib-bors bot commented Jan 28, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

maddycrim commented Nov 14, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

alreadydone commented Dec 23, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

kim-em commented Jan 11, 2025

Uh oh!

github-actions bot commented Jan 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary be65509fd6

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

kim-em commented Jan 28, 2025

Uh oh!

mathlib-bors bot commented Jan 28, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

maddycrim commented Nov 14, 2024 •

edited

Loading

alreadydone commented Dec 23, 2024 •

edited

Loading

github-actions bot commented Jan 23, 2025 •

edited

Loading