[Merged by Bors] - feat: introduce `IsRelPrime` and `DecompositionMonoid` and refactor by alreadydone · Pull Request #10327 · leanprover-community/mathlib4

alreadydone · 2024-02-07T09:52:31Z

Introduce typeclass DecompositionMonoid, which says every element in the monoid is primal, i.e., whenever an element divides a product b * c, it can be factored into a product such that the factors divides b and c respectively. A domain is called pre-Schreier if its multiplicative monoid is a decomposition monoid, and these are more general than GCD domains.
Show that any GCDMonoid is a DecompositionMonoid. In order for lemmas about DecompositionMonoids to automatically apply to UniqueFactorizationMonoids, we add instances from UniqueFactorizationMonoid α to Nonempty (NormalizedGCDMonoid α) to Nonempty (GCDMonoid α) to DecompositionMonoid α. (Zulip) See the bottom of message for an updated diagram of classes and instances.
Introduce binary predicate IsRelPrime which says that the only common divisors of the two elements are units. Replace previous occurrences in mathlib by this predicate.
Duplicate all lemmas about IsCoprime in Coprime/Basic (except three lemmas about smul) to IsRelPrime. Due to import constraints, they are spread into three files Algebra/Divisibility/Units (including key lemmas assuming DecompositionMonoid), GroupWithZero/Divisibility, and Coprime/Basic.
Show IsCoprime always imply IsRelPrime and is equivalent to it in Bezout rings. To reduce duplication, the definition of Bezout rings and the GCDMonoid instance are moved from RingTheory/Bezout to RingTheory/PrincipalIdealDomain, and some results in PrincipalIdealDomain are generalized to Bezout rings.
Remove the recently added file Squarefree/UniqueFactorizationMonoid and place the results appropriately within Squarefree/Basic. All results are generalized to DecompositionMonoid or weaker except the last one.

With this PR, all the following instances (indicated by arrows) now work; this PR fills the central part.

																		  EuclideanDomain (bundled)
                                                                              ↙          ↖
                                                                 IsPrincipalIdealRing ← Field (bundled)
                                                                            ↓             ↓
         NormalizationMonoid ←          NormalizedGCDMonoid → GCDMonoid  IsBezout ← ValuationRing ← IsDiscreteValuationRing
                   ↓                             ↓                 ↘       ↙
Nonempty NormalizationMonoid ← Nonempty NormalizedGCDMonoid →  Nonempty GCDMonoid → IsIntegrallyClosed
                                                 ↑                    ↓
                    WfDvdMonoid ← UniqueFactorizationMonoid → DecompositionMonoid (pre-Schreier)
                                                 ↑
                                       IsPrincipalIdealRing

…ommunity/mathlib4 into DecompositionMonoid

alreadydone · 2024-02-12T20:24:09Z

bors r+

…10327) + Introduce typeclass `DecompositionMonoid`, which says every element in the monoid is primal, i.e., whenever an element divides a product `b * c`, it can be factored into a product such that the factors divides `b` and `c` respectively. A domain is called pre-Schreier if its multiplicative monoid is a decomposition monoid, and these are more general than GCD domains. + Show that any `GCDMonoid` is a `DecompositionMonoid`. In order for lemmas about `DecompositionMonoid`s to automatically apply to `UniqueFactorizationMonoid`s, we add instances from `UniqueFactorizationMonoid α` to `Nonempty (NormalizedGCDMonoid α)` to `Nonempty (GCDMonoid α)` to `DecompositionMonoid α`. ([Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/non-normalizable.20gcd_monoid/near/316895209)) See the bottom of message for an updated diagram of classes and instances. + Introduce binary predicate `IsRelPrime` which says that the only common divisors of the two elements are units. Replace previous occurrences in mathlib by this predicate. + Duplicate all lemmas about `IsCoprime` in Coprime/Basic (except three lemmas about smul) to `IsRelPrime`. Due to import constraints, they are spread into three files Algebra/Divisibility/Units (including key lemmas assuming DecompositionMonoid), GroupWithZero/Divisibility, and Coprime/Basic. + Show `IsCoprime` always imply `IsRelPrime` and is equivalent to it in Bezout rings. To reduce duplication, the definition of Bezout rings and the GCDMonoid instance are moved from RingTheory/Bezout to RingTheory/PrincipalIdealDomain, and some results in PrincipalIdealDomain are generalized to Bezout rings. + Remove the recently added file Squarefree/UniqueFactorizationMonoid and place the results appropriately within Squarefree/Basic. All results are generalized to DecompositionMonoid or weaker except the last one. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Coprime.20if.20product.20is.20squarefree/near/419334520) With this PR, all the following instances (indicated by arrows) now work; this PR fills the central part. ``` EuclideanDomain (bundled) ↙ ↖ IsPrincipalIdealRing ← Field (bundled) ↓ ↓ NormalizationMonoid ← NormalizedGCDMonoid → GCDMonoid IsBezout ← ValuationRing ← DiscreteValuationRing ↓ ↓ ↘ ↙ Nonempty NormalizationMonoid ← Nonempty NormalizedGCDMonoid → Nonempty GCDMonoid → IsIntegrallyClosed ↑ ↓ WfDvdMonoid ← UniqueFactorizationMonoid → DecompositionMonoid ↑ IsPrincipalIdealRing ``` Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org>

mathlib-bors · 2024-02-12T22:06:43Z

Pull request successfully merged into master.

Build succeeded:

…10327) + Introduce typeclass `DecompositionMonoid`, which says every element in the monoid is primal, i.e., whenever an element divides a product `b * c`, it can be factored into a product such that the factors divides `b` and `c` respectively. A domain is called pre-Schreier if its multiplicative monoid is a decomposition monoid, and these are more general than GCD domains. + Show that any `GCDMonoid` is a `DecompositionMonoid`. In order for lemmas about `DecompositionMonoid`s to automatically apply to `UniqueFactorizationMonoid`s, we add instances from `UniqueFactorizationMonoid α` to `Nonempty (NormalizedGCDMonoid α)` to `Nonempty (GCDMonoid α)` to `DecompositionMonoid α`. ([Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/non-normalizable.20gcd_monoid/near/316895209)) See the bottom of message for an updated diagram of classes and instances. + Introduce binary predicate `IsRelPrime` which says that the only common divisors of the two elements are units. Replace previous occurrences in mathlib by this predicate. + Duplicate all lemmas about `IsCoprime` in Coprime/Basic (except three lemmas about smul) to `IsRelPrime`. Due to import constraints, they are spread into three files Algebra/Divisibility/Units (including key lemmas assuming DecompositionMonoid), GroupWithZero/Divisibility, and Coprime/Basic. + Show `IsCoprime` always imply `IsRelPrime` and is equivalent to it in Bezout rings. To reduce duplication, the definition of Bezout rings and the GCDMonoid instance are moved from RingTheory/Bezout to RingTheory/PrincipalIdealDomain, and some results in PrincipalIdealDomain are generalized to Bezout rings. + Remove the recently added file Squarefree/UniqueFactorizationMonoid and place the results appropriately within Squarefree/Basic. All results are generalized to DecompositionMonoid or weaker except the last one. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Coprime.20if.20product.20is.20squarefree/near/419334520) With this PR, all the following instances (indicated by arrows) now work; this PR fills the central part. ``` EuclideanDomain (bundled) ↙ ↖ IsPrincipalIdealRing ← Field (bundled) ↓ ↓ NormalizationMonoid ← NormalizedGCDMonoid → GCDMonoid IsBezout ← ValuationRing ← DiscreteValuationRing ↓ ↓ ↘ ↙ Nonempty NormalizationMonoid ← Nonempty NormalizedGCDMonoid → Nonempty GCDMonoid → IsIntegrallyClosed ↑ ↓ WfDvdMonoid ← UniqueFactorizationMonoid → DecompositionMonoid ↑ IsPrincipalIdealRing ``` Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org>

See #10327 for the new copyright header

ocfnash and others added 13 commits February 4, 2024 15:19

feat: add lemma exists_squarefree_dvd_pow_of_ne_zero

42e0176

initial

8775afd

more IsRelPrime replacement

85730d2

copy IsCoprime lemmas to IsRelPrime

547c288

misc lemmas

55015f5

streamline instances with Nonempty

83fde93

generalize Squarefree.isRadical

fc3ca80

IsRadical.of_dvd

82a90cf

fix

a7ed74c

golf

03aedf5

move IsBezout.gcd to PID

73ee2f8

remove Squarefree/UFM and finish(?)

3984b1e

ufm_of_decomposition_of_wfDvdMonoid

567ed6c

alreadydone added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Feb 7, 2024

alreadydone requested review from jcommelin and ocfnash February 7, 2024 09:52

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 Feb 7, 2024

Merge remote-tracking branch 'origin/master' into DecompositionMonoid

fb35f5f

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

Update Mathlib.lean

e3d54ad

alreadydone added WIP Work in progress and removed awaiting-review labels Feb 7, 2024

alreadydone added 6 commits February 7, 2024 11:45

fixes

536fca6

Merge branch 'DecompositionMonoid' of https://github.com/leanprover-c…

1691ca7

…ommunity/mathlib4 into DecompositionMonoid

fix

0e597ed

fix

64bf1d5

fix

69052f6

generalize/deprecate irreducible_iff_prime

3b29187

alreadydone added 2 commits February 12, 2024 13:31

Merge branch 'DecompositionMonoid' of https://github.com/leanprover-c…

91a7b5f

…ommunity/mathlib4 into DecompositionMonoid

forgot to remove temp def

7c05e2e

alreadydone removed the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Feb 12, 2024

mathlib-bors bot changed the title ~~feat: introduce IsRelPrime and DecompositionMonoid and refactor~~ [Merged by Bors] - feat: introduce IsRelPrime and DecompositionMonoid and refactor Feb 12, 2024

mathlib-bors bot closed this Feb 12, 2024

mathlib-bors bot deleted the DecompositionMonoid branch February 12, 2024 22:06

alreadydone mentioned this pull request Feb 28, 2024

[Merged by Bors] - feat: sum and product of commuting semisimple endomorphisms #10808

Closed

YaelDillies added a commit that referenced this pull request Jan 14, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

c2f8a51

See #10327 for the new copyright header

YaelDillies mentioned this pull request Jan 14, 2025

[Merged by Bors] - chore(Submonoid/Membership): don't import MonoidWithZero #20748

Closed

2 tasks

YaelDillies added a commit that referenced this pull request Jan 14, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

65b3103

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 15, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

41731ef

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 15, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

95c0687

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 15, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

2bf7213

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 15, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

931f733

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 15, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

669d9f6

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 15, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

5690fc5

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 15, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

91db9e5

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 15, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

06046ac

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 17, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

f6a4834

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 19, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

655b07c

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 20, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

d78854b

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 21, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

20fa0e5

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 22, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

e2a7062

See #10327 for the new copyright header

YaelDillies added a commit that referenced this pull request Jan 25, 2025

chore(Submonoid/Membership): don't import MonoidWithZero

34df748

See #10327 for the new copyright header

mathlib-bors bot pushed a commit that referenced this pull request Jan 31, 2025

chore(Submonoid/Membership): don't import MonoidWithZero (#20748)

c7a5e3b

See #10327 for the new copyright header

jt496 pushed a commit that referenced this pull request Feb 3, 2025

chore(Submonoid/Membership): don't import MonoidWithZero (#20748)

f97940e

See #10327 for the new copyright header

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: introduce `IsRelPrime` and `DecompositionMonoid` and refactor#10327

[Merged by Bors] - feat: introduce `IsRelPrime` and `DecompositionMonoid` and refactor#10327
alreadydone wants to merge 39 commits intomasterfrom
DecompositionMonoid

alreadydone commented Feb 7, 2024 •

edited

Loading

Uh oh!

alreadydone commented Feb 12, 2024

Uh oh!

mathlib-bors bot commented Feb 12, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

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

Uh oh!

Uh oh!

alreadydone commented Feb 12, 2024

Uh oh!

mathlib-bors bot commented Feb 12, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

alreadydone commented Feb 7, 2024 •

edited

Loading