[Merged by Bors] - feat(RingTheory/Radical): Radical of an element in a unique factorization normalization monoid by seewoo5 · Pull Request #14873 · leanprover-community/mathlib4

seewoo5 · 2024-07-18T16:36:56Z

For a unique factorization normalization monoid, define a radical of an element as a product of normalized prime factors (without duplication).

This is part of our project to port Mason-Stothers Theorem in mathlib @jcpaik. You can find more theorems that will be added in future PRs here.

github-actions · 2024-07-18T16:37:37Z

PR summary 0963a13d95

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Radical`	1012

Declarations diff

+ primeFactors
+ primeFactors_pow
+ radical
+ radical_dvd_self
+ radical_eq_of_associated
+ radical_mul_unit
+ radical_of_prime
+ radical_one_eq
+ radical_pow
+ radical_pow_of_prime
+ radical_unit_eq_one
+ radical_unit_mul
+ radical_zero_eq

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.

jcommelin

Thanks for your PR!

Mathlib/RingTheory/Radical.lean

jcommelin · 2024-07-19T07:50:50Z

Mathlib/RingTheory/Radical.lean

+theorem radical_zero_eq_one : radical (0 : α) = 1 := by
+  rw [radical, primeFactors, normalizedFactors_zero, Multiset.toFinset_zero, Finset.prod_empty]
+
+theorem radical_one_eq_one : radical (1 : α) = 1 := by


Suggested change

theorem radical_one_eq_one : radical (1 : α) = 1 := by

@[simp]

theorem radical_one : radical (1 : α) = 1 := by

Should I also change radical_unit_eq_one to radical_unit_eq? I wonder what is the rule behind the naming (if the simp reduction is 'trivial', drop the right hand side?).

Another minor question is: do we want radical_(zero|one)_eq or radical_(zero|one)?

seewoo5 · 2024-07-28T22:28:26Z

@jcommelin Could you check the updates? Thanks!

Mathlib/RingTheory/Radical.lean

erdOne · 2024-07-30T17:27:15Z

Mathlib/RingTheory/Radical.lean

+    rw [primeFactors, Multiset.toFinset_val]
+    apply Multiset.dedup_le
+
+theorem radical_prime {a : α} (ha : Prime a) : radical a = normalize a := by


Suggested change

theorem radical_prime {a : α} (ha : Prime a) : radical a = normalize a := by

theorem radical_of_prime {a : α} (ha : Prime a) : radical a = normalize a := by

This holds for every square-free element right? How hard is it to generalise this? same below.

I believe so, but not sure how hard it is. For commutative rings, coprime induction with additional theorems in #15331 might work (assuming that we have multiplicativity theorem for the normalization map).

Now that I think of it more, I think it follows easily from squarefree_iff_nodup_normalizedFactors.

Should I prove it in this PR, or make another one later? FYI these are mainly for porting the formalization of Mason-Stothers theorem and we don't need the generalization.

Mathlib/RingTheory/Radical.lean

seewoo5 · 2024-08-13T07:03:54Z

@jcommelin @erdOne Let me know if any updates are needed!

Mathlib/RingTheory/Radical.lean

jcommelin

Sorry for the late response. I was away on holidays.

bors merge

…tion normalization monoid (#14873) For a unique factorization normalization monoid, define a radical of an element as a product of normalized prime factors (without duplication). Co-authored-by: Jineon Baek <jcpaik@jcpaik-desktop.local> Co-authored-by: Johan Commelin <johan@commelin.net>

YaelDillies · 2024-08-14T13:38:02Z

Mathlib/RingTheory/Radical.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2024 Jineon Back and Seewoo Lee. All rights reserved.


Suggested change

Copyright (c) 2024 Jineon Back and Seewoo Lee. All rights reserved.

Copyright (c) 2024 Jineon Baek, Seewoo Lee. All rights reserved.

YaelDillies · 2024-08-14T13:39:18Z

Mathlib/RingTheory/Radical.lean

+Radical of an element `a` in a unique factorization monoid is the product of
+the prime factors of `a`.
+-/
+def radical (a : M) : M :=


Don't you think this is too generic of a name to be put in the root namespace?

@YaelDillies I agree, do you have any suggestions? I was thinking something like element_radical. Maybe I should also change the name of the file Radical.lean accordingly?

The defs you're using are in the UniqueFactorizationDomain namespace. m not a huge fan of it (why not just UFD or RingTheory?) but it would be an obvious statu quo choice

I may not understand completely but moving everything to the RingTheory/UniqueFactorizationDomain.lean would be okay?

No, I'm talking about the namespace, not the file!

mathlib-bors · 2024-08-14T13:56:02Z

Pull request successfully merged into master.

Build succeeded:

jcommelin · 2024-08-14T14:00:22Z

@seewoo5 Could you please create a follow-up PR implementing the comments by @YaelDillies ?

…tion normalization monoid (#14873) For a unique factorization normalization monoid, define a radical of an element as a product of normalized prime factors (without duplication). Co-authored-by: Jineon Baek <jcpaik@jcpaik-desktop.local> Co-authored-by: Johan Commelin <johan@commelin.net>

@YaelDillies

…15826) Restrict scope of radical as suggested in [this comment](#14873 (comment)) by @YaelDillies.

…tion normalization monoid (#14873) For a unique factorization normalization monoid, define a radical of an element as a product of normalized prime factors (without duplication). Co-authored-by: Jineon Baek <jcpaik@jcpaik-desktop.local> Co-authored-by: Johan Commelin <johan@commelin.net>

@YaelDillies

…15826) Restrict scope of radical as suggested in [this comment](#14873 (comment)) by @YaelDillies.

…tion normalization monoid (#14873) For a unique factorization normalization monoid, define a radical of an element as a product of normalized prime factors (without duplication). Co-authored-by: Jineon Baek <jcpaik@jcpaik-desktop.local> Co-authored-by: Johan Commelin <johan@commelin.net>

@YaelDillies

…15826) Restrict scope of radical as suggested in [this comment](#14873 (comment)) by @YaelDillies.

…tion normalization monoid (#14873) For a unique factorization normalization monoid, define a radical of an element as a product of normalized prime factors (without duplication). Co-authored-by: Jineon Baek <jcpaik@jcpaik-desktop.local> Co-authored-by: Johan Commelin <johan@commelin.net>

@YaelDillies

…15826) Restrict scope of radical as suggested in [this comment](#14873 (comment)) by @YaelDillies.

seewoo5 added 3 commits July 18, 2024 09:28

initial commit

e270cb8

remove unnecessary import

b172681

lint

b542624

seewoo5 added the t-algebra Algebra (groups, rings, fields, etc) label Jul 18, 2024

seewoo5 self-assigned this Jul 18, 2024

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 18, 2024

mathlib.lean

0a9d1af

seewoo5 changed the title ~~feat(RingTheory/Radical): Radical of an element in unique factorization normalization monoid~~ feat(RingTheory/Radical): Radical of an element in a unique factorization normalization monoid Jul 18, 2024

jcommelin reviewed Jul 19, 2024

View reviewed changes

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 19, 2024

Jineon Baek added 3 commits July 22, 2024 09:51

edit comments

fbb690d

Name changes + edit comments

188206f

Add simp tag

d148c69

jcpaik removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 22, 2024

jcpaik requested a review from jcommelin July 22, 2024 01:01

jcpaik self-assigned this Jul 22, 2024

seewoo5 mentioned this pull request Jul 30, 2024

[Merged by Bors] - feat(RingTheory/Radical): Theorems for coprime elements + alpha #15331

Closed

3 tasks

erdOne reviewed Jul 30, 2024

View reviewed changes

seewoo5 added 4 commits July 30, 2024 10:50

address comments

0df94d7

rename alpha -> M

20840c1

minor

c20c796

remove k

c1da6cd

This was referenced Aug 5, 2024

Porting Radical.lean seewoo5/lean-poly-abc#48

Closed

[Merged by Bors] - feat: Mason-Stothers theorem (polynomial ABC) #15706

Closed

jcommelin reviewed Aug 14, 2024

View reviewed changes

Mathlib/RingTheory/Radical.lean Show resolved Hide resolved

Update Mathlib/RingTheory/Radical.lean

0963a13

jcommelin reviewed Aug 14, 2024

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Aug 14, 2024

YaelDillies reviewed Aug 14, 2024

View reviewed changes

mathlib-bors bot changed the title ~~feat(RingTheory/Radical): Radical of an element in a unique factorization normalization monoid~~ [Merged by Bors] - feat(RingTheory/Radical): Radical of an element in a unique factorization normalization monoid Aug 14, 2024

mathlib-bors bot closed this Aug 14, 2024

mathlib-bors bot deleted the feature/element-radical branch August 14, 2024 13:56

seewoo5 mentioned this pull request Aug 15, 2024

[Merged by Bors] - refactor: Restrict scope of radical to UniqueFactorizationDomain #15826

Closed

mathlib-bors bot pushed a commit that referenced this pull request Aug 16, 2024

refactor: Restrict scope of radical to UniqueFactorizationDomain (#…

b899e71

…15826) Restrict scope of radical as suggested in [this comment](#14873 (comment)) by @YaelDillies.

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024

refactor: Restrict scope of radical to UniqueFactorizationDomain (#…

179f8cf

…15826) Restrict scope of radical as suggested in [this comment](#14873 (comment)) by @YaelDillies.

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024

refactor: Restrict scope of radical to UniqueFactorizationDomain (#…

c739119

…15826) Restrict scope of radical as suggested in [this comment](#14873 (comment)) by @YaelDillies.

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024

refactor: Restrict scope of radical to UniqueFactorizationDomain (#…

bf76034

…15826) Restrict scope of radical as suggested in [this comment](#14873 (comment)) by @YaelDillies.

	theorem radical_one_eq_one : radical (1 : α) = 1 := by
	@[simp]
	theorem radical_one : radical (1 : α) = 1 := by

	theorem radical_prime {a : α} (ha : Prime a) : radical a = normalize a := by
	theorem radical_of_prime {a : α} (ha : Prime a) : radical a = normalize a := by

		@@ -0,0 +1,104 @@
		/-
		Copyright (c) 2024 Jineon Back and Seewoo Lee. All rights reserved.

	Copyright (c) 2024 Jineon Back and Seewoo Lee. All rights reserved.
	Copyright (c) 2024 Jineon Baek, Seewoo Lee. All rights reserved.

Conversation

seewoo5 commented Jul 18, 2024 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 0963a13d95

Import changes for modified files

Declarations diff

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

seewoo5 commented Jul 28, 2024

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

seewoo5 commented Aug 13, 2024

Uh oh!

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Aug 14, 2024

Uh oh!

jcommelin commented Aug 14, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

seewoo5 commented Jul 18, 2024 •

edited by YaelDillies

Loading

github-actions bot commented Jul 18, 2024 •

edited

Loading