## Stream: maths

### Topic: Refactoring UFDs to Monoids

#### Aaron Anderson (Aug 05 2020 at 00:40):

@Anne Baanen has reviewed my PR on factorization of pnats with finsupps (#3291), and suggested that the finsupp generalization should be made more broadly. I think this means it's time to try @Kevin Buzzard's suggestion that UFDs be refactored to revolve around a predicate on monoids, rather than rings.

#### Aaron Anderson (Aug 05 2020 at 00:50):

One decision that'll have to be made is how to deal with the fact that a monoid may or may not have a 0 element. I'm in favor either of this kind of definition: Mario Carneiro said:

"all elements that are not zero-like have a unique factorization"

#### Aaron Anderson (Aug 05 2020 at 00:58):

or something involving enats

#### Aaron Anderson (Aug 05 2020 at 04:42):

I've started tinkering with casework based on def zerolike (x : α) : Prop := ∀ y, x * y = x, starting with normalization monoids. It works, but it's a bit of a hassle.

#### Aaron Anderson (Aug 05 2020 at 04:43):

Does anybody have any ideas as to what classes and instances would make casework on whether we're dealing with a monoid-with-zero tractable?

#### Aaron Anderson (Aug 05 2020 at 05:51):

Perhaps a better first step is changing the divisibility relation to work for all comm_monoids instead of just comm_semirings. I've started working on that at mathlib:divisibility_monoid. Does anybody have any objection to this?

#### Kevin Buzzard (Aug 05 2020 at 07:31):

The reason i think this is the way to go is that the nonzero ideals of a Dedekind domain have unique factorisation

#### Kevin Buzzard (Aug 05 2020 at 07:32):

Given a monoid with zero and a 1, and a proof that 0 isn't 1, is there a way to extract the nonzero elements as a monoid?

#### Kenny Lau (Aug 05 2020 at 07:39):

just make a subtype

#### Kenny Lau (Aug 05 2020 at 07:40):

{x // x \ne 0} or something like that

#### Aaron Anderson (Aug 05 2020 at 15:57):

I could definitely put a monoid instance on that subtype of a monoid_with_zero, but I should check first to see whether it's natural to use the submonoid API

#### Aaron Anderson (Aug 05 2020 at 16:20):

Hmm, using subtypes could again run into problems. If I just define, say, gcd on monoids without zero, and then define gcd on monoids with zero by using my definition of gcd on the subtype, then gcd's got the wrong type, and really the gcd function should be able to work with 0 just fine

#### Adam Topaz (Aug 05 2020 at 16:29):

I think the correct thing to do is to define the left adjoint of the forgetful functor from monoids with zero to monoids (formally adjoin a zero). Do all the constructions for monoid_with_zero, and then it will apply to a monoid by first applying this left adjoint.

#### Adam Topaz (Aug 05 2020 at 16:32):

(I think the construction of adjoining a zero to a monoid already exists.)

#### Adam Topaz (Aug 05 2020 at 16:56):

Also, in general you cannot put a monoid structure on {x // x \ne 0} because the original monoid might have zero divisors.

#### Mario Carneiro (Aug 05 2020 at 16:56):

what about the set of all non-zero-divisors?

#### Adam Topaz (Aug 05 2020 at 16:58):

That should be ok.

#### Kevin Buzzard (Aug 05 2020 at 17:03):

All divisibility theory stuff should perhaps be done under the running assumption that there are no zero divisors. All of this ED, PID, UFD stuff assumes integral domain, and the ideals in a Dedekind domain have no zero divisors (but have a zero). The slick definition of UFD is a monoid M0 with zero, with no zero-divisors, such that the monoid M you get by removing the zero, when quotiented out by the units, is a free monoid.

#### Aaron Anderson (Aug 05 2020 at 17:06):

Perhaps the thing to do is to create two definitions of everything, and then prove that the with-zero versions are equivalent to the zeroless versions as applied to the submonoid obtained by deleting 0 (or all 0-divisors, depending on assumptions) and transporting lemmas that way?

#### Kevin Buzzard (Aug 05 2020 at 17:17):

I don't know of any situation where mathematicians talk about unique factorisation but don't have a zero

#### Adam Topaz (Aug 05 2020 at 17:17):

Kevin Buzzard said:

All divisibility theory stuff should perhaps be done under the running assumption that there are no zero divisors. All of this ED, PID, UFD stuff assumes integral domain, and the ideals in a Dedekind domain have no zero divisors (but have a zero). The slick definition of UFD is a monoid M0 with zero, with no zero-divisors, such that the monoid M you get by removing the zero, when quotiented out by the units, is a free monoid.

Dont remove the zero, and it's even more slick -- it's a free commutative monoid_with_zero :) (after multiplicatively modding out by units)

#### Kevin Buzzard (Aug 05 2020 at 17:17):

One could argue that pnat was one, but pnat is rarely used

#### Kevin Buzzard (Aug 05 2020 at 17:19):

It has bugged me for literally decades that one of the definitions of a Dedekind domain is that it's an ID where each nonzero ideal factors uniquely into prime ideals. Often people forget to say nonzero

#### Aaron Anderson (Aug 05 2020 at 17:20):

I suspect that at least gcd_domain should be at least partially property of general monoids

#### Adam Topaz (Aug 05 2020 at 17:21):

This is something about things ordered by divisibility.

#### Adam Topaz (Aug 05 2020 at 17:21):

So yeah, something should be doable with monoids / monoids_with_zeros

#### Aaron Anderson (Aug 05 2020 at 17:22):

And a factorization is, at least partially, a function from a monoid to an add_monoid which is a homomorphism except at 0 if it exists

#### Aaron Anderson (Aug 05 2020 at 17:22):

And this particular 0 casework pops up other places, like logarithms

#### Adam Topaz (Aug 05 2020 at 17:22):

everything divides zero -- it's \top in some sense.

#### Reid Barton (Aug 05 2020 at 17:22):

Adam's observation also works for Dedekind domains too then, right? It's a ring whose prime ideals (pointed by 0 = the zero ideal, hence in particular must be an integral domain) generate the ideals freely as a monoid with zero

#### Aaron Anderson (Aug 05 2020 at 17:23):

So I don’t want to hang up the refactorization of these concepts to monoids on zero, but I think it’s still worth thinking of a good solution to that casework

#### Aaron Anderson (Aug 05 2020 at 17:24):

(And also I would rather be able to still use the stuff I wrote with pnats, but I don’t want to make everything else an awful mess in the process)

#### Adam Topaz (Aug 05 2020 at 17:26):

@Reid Barton I guess in this case it's the free comm_monoid_with_zero on a pointed set (where the point becomes 0).

#### Kevin Buzzard (Aug 05 2020 at 18:20):

Yes, in the Dedekind domain example, and also in nat, there are no units other than 1.

#### Aaron Anderson (Aug 05 2020 at 18:21):

I've found some trouble on mathlib:divisibility_monoid...

#### Aaron Anderson (Aug 05 2020 at 18:23):

I didn't think I changed anything other than what instance is required for comm_semiring_has_dvd, but now some places in the library, when we refer to a | b where a b : nat, it thinks we want to be checking divisibility of comm_monoid nat instances instead of nats

#### Aaron Anderson (Aug 05 2020 at 18:25):

I don't know why it'd do that if it wasn't already assuming that we were trying ask if one comm_semiring nat divides another...

#### Aaron Anderson (Aug 05 2020 at 18:30):

And it's only a problem with calc-mode proofs involving pnats.

#### Aaron Anderson (Aug 05 2020 at 18:32):

How do I see exactly what lemmas calc is using? It's definitely using some form of transitivity, etc. without explicitly mentioning them

#### Kevin Buzzard (Aug 05 2020 at 18:55):

This reminds me of the nat.pow v monoid.pow issue

#### Kevin Buzzard (Aug 05 2020 at 18:57):

calc uses lemmas tagged [trans]

#### Aaron Anderson (Aug 05 2020 at 19:02):

Hmm, the only lemma tagged [trans] that I would think it would use, dvd_trans, is just copy-pasted

#### Aaron Anderson (Aug 05 2020 at 19:02):

and works fine when I explicitly use apply instead of tactics

#### Kevin Buzzard (Aug 05 2020 at 19:03):

There will be some nat.dvd_trans and monoid.dvd_trans maybe?

#### Aaron Anderson (Aug 05 2020 at 19:06):

It appears that nat.dvd_trans is not tagged with [trans], but dvd_trans (the comm_semiring one that I switched to work with comm_monoid) is

#### Kevin Buzzard (Aug 05 2020 at 19:11):

import data.nat.basic

def ZZZ (a b c : ℕ) (hab : a ∣ b) (hbc : b ∣ c) :
a ∣ c :=
calc a ∣ b : hab
...    ∣ c : hbc

#print ZZZ -- dvd_trans


Yes, it's picking up the semiring one.

#### Aaron Anderson (Aug 05 2020 at 19:24):

Yeah, and when I copy-paste that, I get a red squiggle under the ..., with

type mismatch at application
dvd_trans
term
c
has type
ℕ
but is expected to have type
comm_monoid ℕ


#### Aaron Anderson (Aug 05 2020 at 19:25):

which is weird, because dvd_trans seems to still work outside of calc

#### Kevin Buzzard (Aug 05 2020 at 19:26):

oh yeah, I can reproduce

#### Aaron Anderson (Aug 05 2020 at 19:26):

def YYZ (a b c : ℕ) (hab : a ∣ b) (hbc : b ∣ c) :
a ∣ c :=
dvd_trans hab hbc


works just fine

#### Aaron Anderson (Aug 05 2020 at 19:40):

oh wow, it was the order of the implied variables in divisibility.lean

#### Aaron Anderson (Aug 05 2020 at 19:41):

the [comm_monoid] instance has to come before {a b c}

#3702

#3714

#### Aaron Anderson (Aug 07 2020 at 17:26):

In that PR, I try to make the divisibility relation work for any (noncommutative) monoid, as I realized that every instance of divisibility in mathlib boils down to exists c, a * c = b, which we might properly call right-divisibility, and associated already makes the choice to use right-associated as the definition in the noncommutative case.

#### Aaron Anderson (Aug 07 2020 at 17:29):

@Anne Baanen pointed out that that could be controversial, instead of defining left- and right-divisibility separately. Does anyone object to using right-divisibility?

#### Adam Topaz (Aug 07 2020 at 17:33):

I think making right divisibility the default is compatible with the fact that the default multiplicative action is an action on the left. It's saying that b is in the image of the (left) multiplicative action of a.

#### Adam Topaz (Aug 07 2020 at 17:36):

In fact, one could define divisibility in any situation where there is a mul_action.

#### Anne Baanen (Aug 07 2020 at 17:39):

Moreover, I would like to point out: even if we later want to introduce has_left_dvd, this PR would be helpful in the preparations because it identifies the parts that we would need to change.

#### Anne Baanen (Aug 07 2020 at 17:40):

So I'm pretty much in favour of the PR, but I would like to make sure we don't make non-canonical choices lightly.

#### Adam Topaz (Aug 07 2020 at 17:50):

I'm not suggesting this should be changed right now, but what are your thoughts about doing something like this at some point in the future?

class has_dvd (α β : Type*) :=
(dvd : α → β → Prop)

instance (M : Type) [monoid M] (α : Type*) [mul_action M α] : has_dvd M α :=
⟨ λ m a, ∃ b, m • b = a ⟩


#### Adam Topaz (Aug 07 2020 at 17:51):

This would let you speak about divisible modules, and things like this.

#### Aaron Anderson (Aug 07 2020 at 17:53):

I would appreciate the smooth syntax for divisible groups, but I’m not sure the definitional equalities between the two instances would be easy to pull off.

#### Adam Topaz (Aug 07 2020 at 17:54):

This works:

import algebra

class has_dvd' (α β : Type*) :=
(dvd : α → β → Prop)

instance foo (M : Type*) [monoid M] (α : Type*) [mul_action M α] : has_dvd' M α :=
⟨ λ m a, ∃ b, m • b = a ⟩

example (M) [comm_ring M] : has_dvd' M M := by apply_instance


#### Adam Topaz (Aug 07 2020 at 17:57):

Oh, it looks like this is missing from mathlib:

instance (M) [monoid M] : mul_action M M := sorry


#### Adam Topaz (Aug 07 2020 at 17:58):

scratch that, it's mul_action.regular M.

#### Aaron Anderson (Aug 07 2020 at 18:00):

I guess it would have to be a different typeclass to accomodate distinct types, so there’s no danger of overriding the existing instances

#### Aaron Anderson (Aug 07 2020 at 18:00):

The other thing you’d have to decide is if you want the mul_action to be inferred or explicit

#### Aaron Anderson (Aug 07 2020 at 18:01):

And whether if it’s inferred, you make a shortcut for the same | notation

#### Aaron Anderson (Aug 07 2020 at 18:03):

I guess you could even edit has_dvd in core, but that’s so vastly above my level

#### Mario Carneiro (Aug 07 2020 at 18:03):

this sounds like it will make the typeclass problem for divisibilty a lot more complicated

#### Adam Topaz (Aug 07 2020 at 18:06):

Can this be solved with notation only?

notation a ∣ b := ∃ c, a • c = b
notation a ∣ b := ∃ c, a * c = b


#### Mario Carneiro (Aug 07 2020 at 18:07):

no, overloaded notation is not very good in lean 3

#### Adam Topaz (Aug 07 2020 at 18:07):

I guess that's a terrible idea.

#### Mario Carneiro (Aug 07 2020 at 18:07):

unless it can be distinguished by type (and these never will be) it always just flags an ambiguity error

I see.

#### Mario Carneiro (Aug 07 2020 at 18:08):

I would just suggest using a sigil of some kind on the symbol

#### Mario Carneiro (Aug 07 2020 at 18:08):

\|\_m or something

#### Adam Topaz (Aug 07 2020 at 18:09):

notation a ∣ₘ b := ∃ c, a • c = b


#### Adam Topaz (Aug 07 2020 at 18:09):

That's not too awful.

#### Aaron Anderson (Aug 11 2020 at 17:03):

What strong opinions do people have about normalization and gcd domains?

#### Aaron Anderson (Aug 11 2020 at 17:06):

I'd like to have one structure called gcd monoid that applies to all monoids (with adequate cancellation at least), which is sort of a lattice structure with different names for the operations. However, normalization monoids have a definition which depends on 0 in the ways discussed earlier.

#### Kevin Buzzard (Aug 11 2020 at 17:09):

These were things which the computable people liked and I could never see the point of. Our definition of UFD is not a Prop, which isn't the mathematical definition. Do mathematicians really any of this stuff? Why can't you just work in the quotient of the nonzero elements by the units?

#### Aaron Anderson (Aug 11 2020 at 21:54):

Ok, we should definitely have a notion of gcd monoid/domain at least general enough to apply to euclidean domains...

#### Aaron Anderson (Aug 12 2020 at 00:06):

I have a tentative definition of gcd_monoid at mathlib:gcd_monoid

#### Aaron Anderson (Aug 13 2020 at 17:33):

Perhaps I'm overcomplicating things, but I think this is the best way to provide a common interface for all instances of gcd:

#### Aaron Anderson (Aug 13 2020 at 17:34):

gcd_monoid : a mixin on comm_monoid that provides gcd and lcm, only guaranteed to be unique up to associated, or maybe even mutual divisibility (whatever you can guarantee for Euclidean domains)

#### Aaron Anderson (Aug 13 2020 at 17:34):

several normalization classes:

#### Aaron Anderson (Aug 13 2020 at 17:36):

• normalization_monoid : a mixin on comm_monoid that provides normalize as a monoid_hom
• norm_unit_monoid_with_zero : basically the current definition of normalization_domain, implies an instance of normalization_monoid
• normalized_monoid or unique_unit_monoid : applies to nats and pnats, implies an instance of normalization_monoid

#### Aaron Anderson (Aug 13 2020 at 17:39):

and then
normalization_gcd_monoid : extends gcd_monoid and normalization_monoid, is basically equivalent to gcd_domain right now, except it can apply to nats, pnats, and associates, this is where coprime is defined to match nat.coprime from core

#### Aaron Anderson (Aug 13 2020 at 17:51):

One obnoxious thing is that for all of these, a useful monoid-theoretic property to assume is that associated is the same thing as mutual divisibility, but the proof of that is slightly different depending on whether you have a comm_cancel_monoid (not yet defined) or a comm_cancel_monoid_with_zero

#### Kevin Buzzard (Aug 13 2020 at 23:07):

Mutual divisibility is the same as associated for an integral domain and anyone trying to do any kind of factoring in a non integral domain is in for a tough time

#### Kevin Buzzard (Aug 13 2020 at 23:08):

I think we should have a mathematician's UFD which is a predicate on IDs rather than one which chooses representatives for factors. This is what comes up in commutative algebra

#### Aaron Anderson (Aug 13 2020 at 23:18):

So, there's no problem with doing it in a comm_cancel_monoid_with_zero, and that should let us do factorization of associates or ideals of a Dedekind Domain, etc.

#### Aaron Anderson (Aug 13 2020 at 23:19):

I'm just still here months later trying to find a way to not have to duplicate the gcd API between nats and pnats

#### Aaron Anderson (Aug 13 2020 at 23:19):

and it seems like the only solution is to have a class of commutative monoids where all elements can either be cancelled or are self-absorbing on both sides...

#### Aaron Anderson (Aug 14 2020 at 00:02):

I've spewed out some work on mathlib:gcd_monoid at src/algebra/gcd_monoid

#### Aaron Anderson (Aug 14 2020 at 00:02):

I'm pretty sure it contains both good and bad ideas...

#### Aaron Anderson (Aug 14 2020 at 00:04):

I have also, however, exceeded instance depth, which means I should probably get help from somebody who knows more than me...

#### Aaron Anderson (Aug 14 2020 at 17:27):

Ok, I think I know how to reorder my priorities on this.

• Refactor normalization and gcd to be mixins on comm_cancel_monoid_with_zero, which is basically an Integral Domain which has forgotten addition and subtraction. This neglects Euclidean domains and pnats for now.
• Turn to UFD. Find non-constructive, purely multiplicative criterion for defining is_UFD. Currently thinking atomic := every non-zero element can be written as a product of irreducibles and units, but not necessarily in some global or constructive way, together with (irreducible iff prime).
• Combine that definition with a normalization_monoid instance to get a constructive unique factorization, where all the irreducibles in the product are normalized (e.g. positive, e.g. monic)

#### Aaron Anderson (Aug 14 2020 at 18:14):

Another step in there might be monoidifying multiplicity, as once you have a set/type of representatives of associate classes, multiplicity should give you the factorization, for the low price of proving multiplicity is finite

#### Aaron Anderson (Aug 14 2020 at 21:19):

#3779 monoidifies some stuff

#### Aaron Anderson (Aug 14 2020 at 21:20):

It makes it possible to define a gcd_monoid instance on nats, and start merging the nat gcd API, but I don't start doing that in that PR

#### Aaron Anderson (Aug 14 2020 at 21:32):

@Kevin Buzzard, do you have opinions on the Prop definition of is_UFD? Another potential idea is irreducible iff prime and descending chain condition for divisibility

#### Aaron Anderson (Aug 23 2020 at 03:18):

I'm making some progress at mathlib:ufm.

#### Aaron Anderson (Aug 23 2020 at 03:22):

I've defined a class called DCC_dvd for monoids in which the relation (λ a b : α, a ≠ 0 ∧ ∃ x, ¬is_unit x ∧ b = a * x) is well-founded. I chose that definition because we've already proven that Noetherian rings satisfy that condition, but it's equivalent to < on associates being well-founded, and it's usually called ACCP in the literature because it's equivalent to the ACC for principal ideals. All of these equivalences are trivial on paper, and seem not too bad in Lean, but aren't yet all trivial. (Would just need one lemma about relation-preserving surjections).

#### Aaron Anderson (Aug 23 2020 at 03:25):

I've defined unique_factorization_monoid to be that together with irreducible_iff_prime, and have renamed unique_factorization_domain to prime_factorization, because that's really the data of that definition. We also have an analogous structure already called unique_irreducible_factorization, that contains that data, and all of these are equivalent as properties of the ring, although not definitionally.

#### Aaron Anderson (Aug 23 2020 at 03:44):

I am going to prove that unique_factorization_monoid is equivalent to "every nonzero element is a product of primes" is equivalent to "every nonzero element is a product of irreducibles uniquely up to units", but should I keep the structures of prime_factorization and unique_irreducible_factorization if those proofs work without them?

#### Aaron Anderson (Aug 23 2020 at 03:49):

Of course, I'll still provide a canonical prime/irreducible factorization for a normalization_monoid, but that seems like about the only condition on which a canonical one actually exists, and works for all of our important examples.

#### Aaron Anderson (Aug 23 2020 at 04:13):

I'm certainly skeptical that we need both prime_factorization and unique_irreducible_factorization, because any time they both exist, they're provably equivalent

#### Kevin Buzzard (Aug 23 2020 at 06:50):

They might not be constructively the same, or something?

#### Aaron Anderson (Aug 23 2020 at 15:55):

Well, any time either kind of factorization exists, you can prove both that such factorizations are unique up to units, and that irreducible is equivalent to prime

#### Kevin Buzzard (Aug 23 2020 at 17:56):

Can you give a definition of a Dedekind domain as an integral domain whose nonzero ideals satisfy unique factorisation?

#### Kevin Buzzard (Aug 23 2020 at 17:57):

The definition goes via the commutative semiring of ideals

#### Aaron Anderson (Aug 23 2020 at 20:04):

Do we actually have that commutative semiring instance on the type of ideals?

#### Aaron Anderson (Aug 23 2020 at 20:05):

I think we'd need a comm_cancel_monoid_with_zero instance on the type of ideals. I'm not sure if the cancel part is true for all comm_rings, but should be true for every integral_domain, I guess, and at least it's definitely true for ideals of a Dedekind domain

#### Aaron Anderson (Aug 23 2020 at 20:07):

Then you need to show what "prime" and possibly "irreducible" mean in that monoid, but "prime" just means prime ideal, at least for enough rings

#### Aaron Anderson (Aug 23 2020 at 20:07):

and then you need to show either that irreducible_iff_prime, in the monoid of ideals, or that each nonzero ideal is a product, in some way, of primes

#### Aaron Anderson (Aug 23 2020 at 20:07):

and then you should be good

#### Aaron Anderson (Aug 23 2020 at 20:08):

once I work everything out here

#### Kevin Buzzard (Aug 23 2020 at 21:37):

That's great. A lot has already been proven about the semring of ideals I believe.

#### Kevin Buzzard (Aug 23 2020 at 21:39):

Aaron Anderson said:

Kevin Buzzard, do you have opinions on the Prop definition of is_UFD? Another potential idea is irreducible iff prime and descending chain condition for divisibility

Just to reply to this (very late I'm sorry, we've been seeing relatives) -- I don't have a clue about this sort of question. I don't believe that definitional equality is so important at this level -- either that or I don't understand its importance. Any Prop which is classically equivalent to being a UFD for rings and which applies to the ideals of a Dedekind domain will be fine.

#### Aaron Anderson (Aug 23 2020 at 21:55):

Ok, I'm proving 3 props are equivalent definitions, and then all data will come after that. If someone has a different preference as to which prop should be the original definition, it shouldn't be so hard to juggle everything around.

#### Aaron Anderson (Aug 24 2020 at 23:07):

Pushed more work. I should be done with showing the equivalence of the different prop definitions, and now I'm going to start constructing an actual prime factorization under the assumption of normalization_monoid

#### Aaron Anderson (Aug 24 2020 at 23:09):

Unfortunately my definition will not be computable because I'm using choice, but it should be possible to refactor it to be defined in terms of multiplicity, which I believe is computable.

#### Kevin Buzzard (Aug 25 2020 at 06:53):

We don't need computability for this stuff

#### Aaron Anderson (Aug 25 2020 at 06:55):

I just pushed a bunch more stuff connecting my work to the rest of the library

#### Aaron Anderson (Aug 25 2020 at 06:56):

for now I’ve deleted the old associates.factor_set business, some of which I want to reimplement, but it seems we can now do pretty much everything we wanted to do before I started, but with more generality, and it’s a predicate

#### Aaron Anderson (Sep 15 2020 at 01:51):

#4156

Last updated: May 09 2021 at 10:11 UTC