[Merged by Bors] - refactor(group_theory/monoid_localization): flip the direction of multiplication #15584

eric-wieser · 2022-07-21T09:43:31Z

In a future PR, this will allow localization and module_localization to be defeq.
Mathematically this makes no difference.

For now, only the primed localization.r' is defeq to localized_module.r.

cc @@jjaassoonn

…tiplication This will allow `localization` and `module_localization` to be defeq. Mathematically this makes no difference.

src/group_theory/monoid_localization.lean

…ation-comm

riccardobrasca · 2022-12-24T10:29:19Z

I think this is a good idea to have localization and module_localization defeq. Can you please fix the conflict? Thanks!

alreadydone

Sorry, the review request got buried in my mailbox for 2 weeks and only resurfaced due to @riccardobrasca's latest comment. I've now taken a detailed look at the PR, and marked apparent "regressions" (where proofs get longer, etc.) along the way. These are foremost notes to myself and not to imply anything negative about the PR; I just wanted to understand what's going on, and it would be nice if you could say a few words to clarify things for me. I'm in favor of bringing module and ring localizations closer and I'd like to see it merged, and surely the PR shortens a lot of proofs as well.

src/algebraic_geometry/projective_spectrum/scheme.lean

src/algebraic_geometry/structure_sheaf.lean

src/field_theory/ratfunc.lean

src/ring_theory/graded_algebra/homogeneous_localization.lean

src/ring_theory/localization/at_prime.lean

src/ring_theory/localization/basic.lean

src/ring_theory/localization/localization_localization.lean

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

eric-wieser · 2023-01-09T13:11:25Z

src/field_theory/ratfunc.lean

@@ -137,18 +137,18 @@ of `∀ {p q a : K[X]} (hq : q ≠ 0) (ha : a ≠ 0), f (a * p) (a * q) = f p q)
 -/
 @[irreducible] protected def lift_on {P : Sort v} (x : ratfunc K)
  (f : ∀ (p q : K[X]), P)
-  (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), p * q' = p' * q →
+  (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), q' * p = q * p' →


@jjaassoonn, do you remember why you changed this in dfcc120?

I just tested the original version. Without flipping p and q, the H q.2 q’.2 on line 143 would not compile.

alreadydone · 2023-01-13T08:06:37Z

src/ring_theory/local_properties.lean

-  simp only [mul_assoc, zero_mul] at hm',
-  rw [mul_comm, ← pow_succ, ← mul_pow] at hm',
+  simp only [mul_assoc, zero_mul, mul_zero] at hm',
+  rw [mul_comm, mul_assoc, mul_comm _ ↑m', ← pow_succ, ← mul_pow] at hm',


Suggested change

rw [mul_comm, mul_assoc, mul_comm _ ↑m', ← pow_succ, ← mul_pow] at hm',

rw [← mul_left_comm, ← pow_succ, ← mul_pow] at hm',

alreadydone · 2023-01-13T08:28:17Z

src/group_theory/monoid_localization.lean

+  haveI : smul_comm_class R M M :=
+    ⟨λ r m₁ m₂, by simp_rw [smul_eq_mul, mul_comm m₁, smul_mul_assoc]⟩,


Could be replaced by this:

Suggested change

haveI : smul_comm_class R M M :=

⟨λ r m₁ m₂, by simp_rw [smul_eq_mul, mul_comm m₁, smul_mul_assoc]⟩,

rw [mul_comm ↑t, mul_comm ↑t, mul_comm b, mul_comm b'] at ht ⊢,

A bit weird that we suddenly need commutativity here; is this indicating we should but haven't flipped the direction somewhere?

A bit weird that we suddenly need commutativity here; is this indicating we should but haven't flipped the direction somewhere?

Ah, it seems that actually the right fix is to replace is_scalar_tower R M M by smul_comm_class R M M. Do you want me to go ahead and do that? Note this PR is getting dangerously close to the porting tide.

Sorry what I suggested doesn't work as is: I should say the last three lines could be replaced by

rw [mul_comm ↑t, mul_comm ↑t, mul_comm b, mul_comm b'] at ht ⊢, simp only [smul_mul_assoc, ht],

However, I agree that it's better to change the hypothesis to smul_comm_class, and this golf works against that, so I'm happy with the current proof. It's up to you whether to make the change; if not, feel free to merge after fixing the conflict.

I think I'll just leave a TODO comment

src/field_theory/ratfunc.lean

src/ring_theory/localization/localization_localization.lean

…ation-comm

alreadydone · 2023-01-22T03:45:27Z

maintainer merge

github-actions · 2023-01-22T03:45:40Z

🚀 Pull request has been placed on the maintainer queue by alreadydone.

riccardobrasca · 2023-01-22T08:59:59Z

Thanks!

bors merge

…tiplication (#15584) In a future PR, this will allow `localization` and `module_localization` to be defeq. Mathematically this makes no difference. For now, only the primed `localization.r'` is defeq to `localized_module.r`. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>

bors · 2023-01-22T11:31:57Z

Pull request successfully merged into master.

Build succeeded:

refactor(group_theory/monoid_localization): flip the direction of mul…

199e331

…tiplication This will allow `localization` and `module_localization` to be defeq. Mathematically this makes no difference.

eric-wieser added the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 21, 2022

eric-wieser and others added 4 commits July 21, 2022 09:50

add commuted lemmas

944c914

fix

1dbc914

fix

23e1d18

fix

b0aafa7

jjaassoonn mentioned this pull request Jul 23, 2022

[Merged by Bors] - feat(algebra/module/localized_module): add characteristic predicate for localized_module #15507

Closed

jjaassoonn added 10 commits July 23, 2022 09:57

fix

795ee1f

fix

468eecf

fix

e8b8d91

fix

c851e49

fix

e390c66

fix

dfcc120

fix localization/integral.lean

b0bb1f0

fix

e1ed73f

fix ring_theory/local_properties

83defae

fix

90b0482

alreadydone reviewed Jul 25, 2022

View reviewed changes

src/group_theory/monoid_localization.lean Show resolved Hide resolved

Merge remote-tracking branch 'origin/master' into eric-wieser/localiz…

d4e679e

…ation-comm

eric-wieser requested a review from a team as a code owner December 11, 2022 16:48

eric-wieser added 9 commits December 11, 2022 18:37

fix

e303875

fix

9731245

fix

82739a7

flip equality direction too

965e3ae

fix

1501b1b

fix

ed136af

fix

3b183ef

fix

02437f3

fix

c8e9030

eric-wieser added the awaiting-review The author would like community review of the PR label Dec 12, 2022

eric-wieser requested a review from alreadydone December 12, 2022 10:58

alreadydone reviewed Dec 26, 2022

View reviewed changes

alreadydone added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 27, 2022

eric-wieser and others added 3 commits January 9, 2023 12:42

Apply suggestions from code review

aaeacfc

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

Update src/ring_theory/localization/at_prime.lean

10e07c6

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

golf

7bdadc8

eric-wieser commented Jan 9, 2023

View reviewed changes

fix docstring

a015bca

eric-wieser added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 12, 2023

Merge branch 'master' into eric-wieser/localization-comm

a58a384

alreadydone approved these changes Jan 13, 2023

View reviewed changes

golfs

80cfeb8

eric-wieser force-pushed the eric-wieser/localization-comm branch from 57b7a4a to 80cfeb8 Compare January 18, 2023 23:49

eric-wieser and others added 4 commits January 20, 2023 18:55

Merge remote-tracking branch 'origin/master' into eric-wieser/localiz…

62233a8

…ation-comm

@fix@

05c054c

todo comment

89789d7

unused_argument

80eb744

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jan 22, 2023

bors bot changed the title ~~refactor(group_theory/monoid_localization): flip the direction of multiplication~~ [Merged by Bors] - refactor(group_theory/monoid_localization): flip the direction of multiplication Jan 22, 2023

bors bot closed this Jan 22, 2023

bors bot deleted the eric-wieser/localization-comm branch January 22, 2023 11:32

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(group_theory/monoid_localization): flip the direction of multiplication #15584

[Merged by Bors] - refactor(group_theory/monoid_localization): flip the direction of multiplication #15584

eric-wieser commented Jul 21, 2022 •

edited

riccardobrasca commented Dec 24, 2022

alreadydone left a comment

eric-wieser Jan 9, 2023

jjaassoonn Jan 9, 2023

alreadydone Jan 13, 2023

alreadydone Jan 13, 2023

eric-wieser Jan 19, 2023

alreadydone Jan 19, 2023

eric-wieser Jan 20, 2023

alreadydone commented Jan 22, 2023

github-actions bot commented Jan 22, 2023

riccardobrasca commented Jan 22, 2023

bors bot commented Jan 22, 2023

	rw [mul_comm, mul_assoc, mul_comm _ ↑m', ← pow_succ, ← mul_pow] at hm',
	rw [← mul_left_comm, ← pow_succ, ← mul_pow] at hm',

		haveI : smul_comm_class R M M :=
		⟨λ r m₁ m₂, by simp_rw [smul_eq_mul, mul_comm m₁, smul_mul_assoc]⟩,

	haveI : smul_comm_class R M M :=
	⟨λ r m₁ m₂, by simp_rw [smul_eq_mul, mul_comm m₁, smul_mul_assoc]⟩,
	rw [mul_comm ↑t, mul_comm ↑t, mul_comm b, mul_comm b'] at ht ⊢,

[Merged by Bors] - refactor(group_theory/monoid_localization): flip the direction of multiplication #15584

[Merged by Bors] - refactor(group_theory/monoid_localization): flip the direction of multiplication #15584

Conversation

eric-wieser commented Jul 21, 2022 • edited

riccardobrasca commented Dec 24, 2022

alreadydone left a comment

Choose a reason for hiding this comment

eric-wieser Jan 9, 2023

Choose a reason for hiding this comment

jjaassoonn Jan 9, 2023

Choose a reason for hiding this comment

alreadydone Jan 13, 2023

Choose a reason for hiding this comment

alreadydone Jan 13, 2023

Choose a reason for hiding this comment

eric-wieser Jan 19, 2023

Choose a reason for hiding this comment

alreadydone Jan 19, 2023

Choose a reason for hiding this comment

eric-wieser Jan 20, 2023

Choose a reason for hiding this comment

alreadydone commented Jan 22, 2023

github-actions bot commented Jan 22, 2023

riccardobrasca commented Jan 22, 2023

bors bot commented Jan 22, 2023

eric-wieser commented Jul 21, 2022 •

edited