Refactoring UFDs to Monoids

Stream: maths

[Aaron Anderson]

@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]

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]

or something involving enats

[Aaron Anderson]

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]

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]

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]

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

[Kevin Buzzard]

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]

just make a subtype

[Kenny Lau]

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

[Aaron Anderson]

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]

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]

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]

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

[Adam Topaz]

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

[Mario Carneiro]

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

[Adam Topaz]

That should be ok.

[Kevin Buzzard]

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]

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]

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

[Adam Topaz]

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]

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

[Kevin Buzzard]

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]

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

[Adam Topaz]

This is something about things ordered by divisibility.

[Adam Topaz]

So yeah, something should be doable with monoids / monoids_with_zeros

[Aaron Anderson]

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]

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

[Adam Topaz]

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

[Reid Barton]

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]

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]

(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]

@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]

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

[Aaron Anderson]

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

[Aaron Anderson]

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]

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]

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

[Aaron Anderson]

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]

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

[Kevin Buzzard]

calc uses lemmas tagged [trans]

[Aaron Anderson]

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

[Aaron Anderson]

and works fine when I explicitly use apply instead of tactics

[Kevin Buzzard]

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

[Aaron Anderson]

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]

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]

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]

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

[Kevin Buzzard]

oh yeah, I can reproduce

[Aaron Anderson]

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

works just fine

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

#3702

[Aaron Anderson]

#3714

[Aaron Anderson]

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]

@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]

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]

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

[Anne Baanen]

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]

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]

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]

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

[Aaron Anderson]

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]

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]

Oh, it looks like this is missing from mathlib:

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

[Adam Topaz]

scratch that, it's mul_action.regular M.

[Aaron Anderson]

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]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Mario Carneiro]

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

[Adam Topaz]

Can this be solved with notation only?

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

[Mario Carneiro]

no, overloaded notation is not very good in lean 3

[Adam Topaz]

I guess that's a terrible idea.

[Mario Carneiro]

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

[Adam Topaz]

I see.

[Mario Carneiro]

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

[Mario Carneiro]

\|\_m or something

[Adam Topaz]

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

[Adam Topaz]

That's not too awful.

[Aaron Anderson]

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

[Aaron Anderson]

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]

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]

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

[Aaron Anderson]

I have a tentative definition of gcd_monoid at mathlib:gcd_monoid

[Aaron Anderson]

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]

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]

several normalization classes:

[Aaron Anderson]

• 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]

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]

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]

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]

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]

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]

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]

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]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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]

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]

#3779 monoidifies some stuff

[Aaron Anderson]

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]

@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]

I'm making some progress at mathlib:ufm.

[Aaron Anderson]

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]

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]

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]

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]

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]

They might not be constructively the same, or something?

[Aaron Anderson]

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]

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

[Kevin Buzzard]

The definition goes via the commutative semiring of ideals

[Aaron Anderson]

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

[Aaron Anderson]

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]

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]

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]

and then you should be good

[Aaron Anderson]

once I work everything out here

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

We don't need computability for this stuff

[Aaron Anderson]

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

[Aaron Anderson]

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]

#4156