Commit 2024-02-12 20:59 b569e065
View on Github →feat: introduce IsRelPrime
and DecompositionMonoid
and refactor (#10327)
- Introduce typeclass
DecompositionMonoid
, which says every element in the monoid is primal, i.e., whenever an element divides a productb * c
, it can be factored into a product such that the factors dividesb
andc
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 aDecompositionMonoid
. In order for lemmas aboutDecompositionMonoid
s to automatically apply toUniqueFactorizationMonoid
s, we add instances fromUniqueFactorizationMonoid α
toNonempty (NormalizedGCDMonoid α)
toNonempty (GCDMonoid α)
toDecompositionMonoid α
. (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) toIsRelPrime
. 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 implyIsRelPrime
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 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