[Merged by Bors] - feat(RingTheory/AdicCompletion): comparison with tensor product by chrisflav · Pull Request #14358 · leanprover-community/mathlib4

chrisflav · 2024-07-02T14:57:18Z

We construct the natural map AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M for any
R-module M and ideal I and show that it is an isomorphism for M = R^n and surjective if M is a finite R-module.

Co-authored-by: Judith Ludwig ludwig@mathi.uni-heidelberg.de

depends on: [Merged by Bors] - chore(RingTheory/AdicCompletion): manual instances #14534

For context: In the next PR we conclude from this one that this above map is an isomorphism for R Noetherian and M finite and deduce from this that AdicCompletion I R is a flat R-algebra if R is Noetherian.

github-actions · 2024-07-02T14:57:58Z

PR summary e87de9ea0e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.LinearAlgebra.TensorProduct.Pi`	752
`Mathlib.RingTheory.AdicCompletion.AsTensorProduct`	1170

Declarations diff

+ Pi.single_apply_smul
+ ofTensorProduct
+ ofTensorProductBil
+ ofTensorProductEquivOfPiFintype
+ ofTensorProduct_bijective_of_pi_of_fintype
+ ofTensorProduct_naturality
+ ofTensorProduct_surjective_of_fg
+ ofTensorProduct_tmul
+ piScalarRight
+ piScalarRightHom
+ piScalarRightHom_tmul
+ piScalarRightInv
+ piScalarRight_apply
+ piScalarRight_symm_single

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>

Mathlib/LinearAlgebra/TensorProduct/Pi.lean

Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean

riccardobrasca · 2024-07-03T10:46:46Z

I have the impression the file AsTensorProduct is quite slow.

!bench

chrisflav · 2024-07-03T12:54:30Z

!bench

leanprover-bot · 2024-07-03T14:13:32Z

Here are the benchmark results for commit 27167c3.
There were no significant changes against commit aa30cf9.

chrisflav · 2024-07-04T08:24:36Z

Benchmark seems to be okay, but I agree the file is slow (and the last PR in this series will make it slower still). I think it's the module instance of AdicCompletion I M over AdicCompletion I R that is slow, this was already visible in the algebra file and I think it's because of the many quotient rings involved. Do you think it is okay for now @riccardobrasca?
(In the future, might it help to introduce IsAdicCompletion I M which eliminates the explicit quotient construction?)

riccardobrasca · 2024-07-04T08:31:50Z

Benchmark seems to be okay, but I agree the file is slow (and the last PR in this series will make it slower still). I think it's the module instance of AdicCompletion I M over AdicCompletion I R that is slow, this was already visible in the algebra file and I think it's because of the many quotient rings involved. Do you think it is okay for now @riccardobrasca? (In the future, might it help to introduce IsAdicCompletion I M which eliminates the explicit quotient construction?)

Can you open a discussion on Zulip about the slowness? We surely want IsAdicCompletion, but also AdicCompletion (to complete a given ring), and maybe it is worth to start investigating now.

chrisflav · 2024-07-04T08:33:48Z

Benchmark seems to be okay, but I agree the file is slow (and the last PR in this series will make it slower still). I think it's the module instance of AdicCompletion I M over AdicCompletion I R that is slow, this was already visible in the algebra file and I think it's because of the many quotient rings involved. Do you think it is okay for now @riccardobrasca? (In the future, might it help to introduce IsAdicCompletion I M which eliminates the explicit quotient construction?)

Can you open a discussion on Zulip about the slowness? We surely want IsAdicCompletion, but also AdicCompletion (to complete a given ring), and maybe it is worth to start investigating now.

Okay, I will do that after the weekend, since I will be away from a computer until Monday.

chrisflav · 2024-07-08T20:27:58Z

!bench

leanprover-bot · 2024-07-08T21:22:01Z

Here are the benchmark results for commit b134ed1.
There were significant changes against commit aa30cf9:

  Benchmark                                          Metric         Change
  ========================================================================
- ~Mathlib.RingTheory.AdicCompletion.Algebra         instructions    14.0%
- ~Mathlib.RingTheory.AdicCompletion.Basic           instructions    29.6%
+ ~Mathlib.RingTheory.AdicCompletion.Functoriality   instructions   -61.6%

This reverts commit ddef0a4.

…m/adic-tensorproduct.2

chrisflav · 2024-07-08T23:26:20Z

!bench

leanprover-bot · 2024-07-09T00:36:49Z

Here are the benchmark results for commit 00f96b9.
There were significant changes against commit 86414a8:

  Benchmark                                          Metric         Change
  ========================================================================
- ~Mathlib.RingTheory.AdicCompletion.Algebra         instructions    20.8%
- ~Mathlib.RingTheory.AdicCompletion.Basic           instructions    47.7%
+ ~Mathlib.RingTheory.AdicCompletion.Functoriality   instructions   -60.2%

leanprover-bot · 2024-07-09T14:02:16Z

Here are the benchmark results for commit abf5c56.
There were significant changes against commit 86414a8:

  Benchmark                                          Metric         Change
  ========================================================================
- ~Mathlib.RingTheory.AdicCompletion.Algebra         instructions    30.9%
- ~Mathlib.RingTheory.AdicCompletion.Basic           instructions    36.4%
+ ~Mathlib.RingTheory.AdicCompletion.Functoriality   instructions   -61.7%

This reverts commit 571a2f2.

This reverts commit 95d1ee9.

…m/adic-tensorproduct.2

chrisflav · 2024-07-11T09:21:47Z

!bench

leanprover-bot · 2024-07-11T10:29:56Z

Here are the benchmark results for commit d63433d.
There were significant changes against commit 86414a8:

  Benchmark                                          Metric         Change
  ========================================================================
+ ~Mathlib.RingTheory.AdicCompletion.Algebra         instructions   -15.3%
+ ~Mathlib.RingTheory.AdicCompletion.Functoriality   instructions   -64.1%

ghost · 2024-07-11T16:21:53Z

This PR/issue depends on:

~~[Merged by Bors] - chore(RingTheory/AdicCompletion): manual instances #14534~~
By Dependent Issues (🤖). Happy coding!

…duct.2

chrisflav · 2024-07-11T21:47:20Z

@riccardobrasca: The speed-up PR #14534 has been merged now (quick summary: currently no big speed-up, but when #11521 lands, this will also make the AsTensorProduct file fast). Anything else I should address for this PR?

riccardobrasca · 2024-07-12T09:14:05Z

Thanks for having investigated this!

bors merge

We construct the natural map `AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M` for any `R`-module `M` and ideal `I` and show that it is an isomorphism for `M = R^n` and surjective if `M` is a finite `R`-module. Co-authored-by: Judith Ludwig <ludwig@mathi.uni-heidelberg.de>

mathlib-bors · 2024-07-12T10:19:45Z

Pull request successfully merged into master.

Build succeeded:

chrisflav · 2024-07-12T10:20:38Z

Thanks for the review!

chrisflav added 2 commits July 2, 2024 16:52

adic completion as tensor product

6956dbb

fix mathlib

e371dcc

chrisflav added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels Jul 2, 2024

fix docstring

25025e5

riccardobrasca self-assigned this Jul 2, 2024

chrisflav mentioned this pull request Jul 2, 2024

[Merged by Bors] - feat(RingTheory/AdicCompletion): adic completion of Noetherian ring is flat #14366

Closed

1 task

riccardobrasca reviewed Jul 3, 2024

View reviewed changes

chrisflav added 2 commits July 3, 2024 14:51

review suggestions

9f162bc

fix

27167c3

chrisflav added 3 commits July 8, 2024 17:28

squeeze some simps

ab77062

speed up

b134ed1

try speedup

db687bf

ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 8, 2024

remove noncomputable for comparision

ddef0a4

chrisflav added 3 commits July 8, 2024 23:32

Revert "remove noncomputable for comparision"

e53302d

This reverts commit ddef0a4.

review suggestions

20fe104

Merge remote-tracking branch 'origin/chrisflav-adic-speedup' into jlc…

00f96b9

…m/adic-tensorproduct.2

change back to manual instances

6b20ecb

chrisflav added 9 commits July 9, 2024 20:35

Revert "add docstrings"

b348370

This reverts commit 571a2f2.

Revert "irreducible"

203b115

This reverts commit 95d1ee9.

add suppress compilation

dc8cc0f

revert back to injective constructors

aa28ef2

remove irreducibles, add suppress compilation

d40f0b5

use fast_instance

1c0a05f

ignore shake

400c96f

Merge remote-tracking branch 'origin/chrisflav-adic-speedup' into jlc…

22d317d

…m/adic-tensorproduct.2

fix

d63433d

ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 11, 2024

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 11, 2024

chrisflav added 2 commits July 11, 2024 19:08

Merge remote-tracking branch 'origin/master' into jlcm/adic-tensorpro…

25105a5

…duct.2

fix

fe2267a

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 11, 2024

chrisflav added 2 commits July 11, 2024 19:50

remove fast instances

5241c01

fix

e87de9e

github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 12, 2024

mathlib-bors bot changed the title ~~feat(RingTheory/AdicCompletion): comparison with tensor product~~ [Merged by Bors] - feat(RingTheory/AdicCompletion): comparison with tensor product Jul 12, 2024

mathlib-bors bot closed this Jul 12, 2024

mathlib-bors bot deleted the jlcm/adic-tensorproduct.2 branch July 12, 2024 10:19

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

Conversation

chrisflav commented Jul 2, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jul 2, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary e87de9ea0e

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

riccardobrasca commented Jul 3, 2024

Uh oh!

chrisflav commented Jul 3, 2024

Uh oh!

leanprover-bot commented Jul 3, 2024

Uh oh!

chrisflav commented Jul 4, 2024

Uh oh!

riccardobrasca commented Jul 4, 2024

Uh oh!

chrisflav commented Jul 4, 2024

Uh oh!

chrisflav commented Jul 8, 2024

Uh oh!

leanprover-bot commented Jul 8, 2024

Uh oh!

chrisflav commented Jul 8, 2024

Uh oh!

leanprover-bot commented Jul 9, 2024

Uh oh!

leanprover-bot commented Jul 9, 2024

Uh oh!

chrisflav commented Jul 11, 2024

Uh oh!

leanprover-bot commented Jul 11, 2024

Uh oh!

ghost commented Jul 11, 2024

Uh oh!

chrisflav commented Jul 11, 2024

Uh oh!

riccardobrasca commented Jul 12, 2024

Uh oh!

mathlib-bors bot commented Jul 12, 2024

Uh oh!

chrisflav commented Jul 12, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

chrisflav commented Jul 2, 2024 •

edited

Loading

github-actions bot commented Jul 2, 2024 •

edited

Loading