feat(data/pnat): factor finsupps

[awainverse]

adds a new definition of factorization for pnats, using finsupps
proves facts about order isomorphisms of lattices

---

[awainverse]

I have added everything to one new file, although it should probably be split up. I've left comments on the sections that I think should be moved. Probably the section on lattice operations under order_embeddings and order_isos should be moved to order.order_iso, and the section on lattice instances on finsupps in particular should be put either in data.finsupp or a new file called data.finsupp.order or data.finsupp.lattice.

[jcommelin]

Some trivial comments. More to come.

[semorrison]

Could you write a short account, either in a comment here or ideally as a module doc-string, about what improvement this makes over existing machinery in mathlib? I have to admit I'm not certain what the purpose of this is yet.

[awainverse]

I've added some of the definitions/results that I think work better for finsupps than for multisets to the module docstring. I see some bad formatting from writing this when I had spent about half as much time with lean as I have now, so I'll try to clean that up after I can download fresh oleans from the server.

[awainverse]

Another more speculative advantage of finsupps for factorization is that you could use enat-valued finsupps to provide the same definition of unique factorization for general monoids and monoid_with_zero, but I'm not doing that in this PR, and I'm not sure how useful that really is.

[semorrison]

Sorry, @robertylewis, I'm not sure I can usefully review this. I'm imagining the intended application of this work is to make it easier to develop the theory of multiplicative functions in number theory, but I'm no expert in that direction so can't judge how well this serves that purpose.

@kbuzzard or @Vierkantor, maybe you could take a look?

[robertylewis]

Oh, no problem, I had just assigned you because you were the last to comment.

[Vierkantor]

I have not tried out the code in too much detail, but here are my impressions about the general approach:

• finsupp is a strict generalization of multiset. A priori, such a generalization can be useful (my suggestion would be to use exponents in ℤ to represent the factors of positive rational numbers).
• Setting the value of a finsupp at one point does seem to be easier than changing the multiplicity of a multiset element, and that operation is useful for number theory.
• If we generalize from multiset to finsupp, I don't see the purpose of keeping around the multiset-based lemmas. Especially since data.pnat.factors doesn't seem to be imported by anything in mathlib. I know re-proving the multiset-based lemmas is not fun, but it should be a clearer demonstration of the power (or awkwardness?) of the finsupp-based approach.
• I have more experience with unique_factorization_domain, which also uses a multiset of factors. In fact, there seems to be a lot of duplication between the two, so it might be worth defining a factor_finsupp for a general semiring/monoid_with_zero(?), then prove that these exist for both ℕ and unique factorization domains.
• finsupp has some API issues, but it's better to fix the issues than avoid using finsupp.

So my preliminary conclusion is that using a finsupp to count the prime factors of a number is probably a good idea, but I'd like to see it happen for more algebraic structures than just natural numbers so we can decrease the amount of duplication, rather than increase it.

[awainverse]

@Vierkantor, I like the sound of everything you've said.
I've started a Zulip thread https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Refactoring.20UFDs.20to.20Monoids to discuss a possible generalization.

[robertylewis]

What's the status here? I get the sense from the conversation that this isn't "request review" right now. @awainverse @Vierkantor ?

[semorrison]

Perhaps it makes sense to close this while other work is going on?