## Stream: maths

### Topic: UFD

@Kevin Buzzard

#### Kevin Buzzard (Sep 02 2018 at 20:56):

Crazy stuff. Looks very different (and much better) than anything I would have written. Here are some random things one could do: PID -> UFD, a Noetherian ring is a UFD iff all height 1 primes are principal, a regular local ring is a UFD, Gauss' lemma about factoring in $K[x]$ ($K$ the field of fractions of $R$) being "the same" as factoring in $R[x]$, $R$ a UFD implies $R[x]$ a UFD.

#### Kevin Buzzard (Sep 02 2018 at 20:58):

Seeing all this lattice stuff reminds me that as far as we know we still don't have the [fourth isomorphism theorem] (https://en.wikipedia.org/wiki/Correspondence_theorem_(group_theory)) for any of groups, abelian groups, additive groups, additive abelian groups, R-modules or rings.

#### Patrick Massot (Sep 02 2018 at 20:58):

Could you explain what looks different?

#### Kevin Buzzard (Sep 02 2018 at 20:59):

I wouldn't have used the word "lattice" at all :-)

ha ha

#### Kevin Buzzard (Sep 02 2018 at 20:59):

I would have just done the maths stuff

#### Kevin Buzzard (Sep 02 2018 at 20:59):

not the weird CS stuff

#### Patrick Massot (Sep 02 2018 at 21:00):

It makes me feel I've been living in the matrix all those years, without knowing my life was secretly ruled by Galois connections.

#### Patrick Massot (Sep 02 2018 at 21:01):

lemma factor_set.sup_add_inf_eq_add : ∀(a b : factor_set α), a ⊔ b + a ⊓ b = a + b WTF?!?

#### Patrick Massot (Sep 02 2018 at 21:02):

Kevin, do you understand what this mean?

#### Kevin Buzzard (Sep 02 2018 at 21:02):

they're multisets maybe?

#### Patrick Massot (Sep 02 2018 at 21:04):

I'll find out tomorrow. I need to sleep: kids go back to school tomorrow, so I go back to getting up early :(

#### Kevin Buzzard (Sep 02 2018 at 21:06):

You make a good point though -- this was definitely something which sprung out at me when I was looking throuhg it. I guess to get an overview of the PR one could look at the definitions. We have associated which presumably is the predicate which is true on a b if a = u b for u a unit. We have the standard definition of UFD, then factor_set, factors' and factors and then all that GCD domain stuff which I think is a CS thing

#### Kevin Buzzard (Sep 02 2018 at 21:07):

Hey -- if I use leanpkg upgrade to pull that update of mathlib, a dependency for the perfectoid project, into the perfectoid project, and then I type leanpkg build withing _target/deps/mathlib, will it take 10 seconds or 20 minutes to compile? Note that I already did this once, earlier today, and this is just one new file which nothing else depends on.

#### Bryan Gin-ge Chen (Sep 02 2018 at 21:11):

Depends on which commit you're at specifically, but I'd bet on a long build because the commit right before that one touched algebra.ring and data.multiset

#### Kevin Buzzard (Sep 02 2018 at 21:15):

@Patrick Massot my kids are back on Wed and sanity will once again prevail in our house. As for the a ⊔ b + a ⊓ b = a + b thing, I think what's going on is that factorset alpha is defined to be  with_top (multiset { a : associates α // irreducible a }) , so that is either a finite set of irreducible (up to units) or an artificial "top", which presumably corresponds to the factors of zero. + is union of multisets, so {3,3,5}+{3,7}={3,3,3,5,7}, and the meet and join are just infs and sups with multisets. The with_top is so that we can factor zero and still have a divides b iff factors of a are a subset of factors of b.

#### Mario Carneiro (Sep 02 2018 at 21:23):

I would have just done the maths stuff, not the weird CS stuff

You have such a funny idea of what CS is. I think you just think everything that isn't the math you do is CS

right :-)

#### Kevin Buzzard (Sep 02 2018 at 21:26):

I mean, you guys must have learnt it somewhere, and it's definitely not in a maths degree, so what is left? gcd domain -- ?!

#### Kevin Buzzard (Sep 02 2018 at 21:27):

My eldest son is going to university next month to study computer science and philosophy, and there was a maths book which was recommended reading for his course so I got it out of our library for him to take a look at, and it really made me laugh -- "how to store a real number in 32 bits" etc :-)

#### Johannes Hölzl (Sep 02 2018 at 21:32):

So I don't know much about UFDs itself, but the formalization of factors as multiset of associated elements felt very natural. Adding a top element was an easy thing, next step would be to show that the multisets form a conditionally complete lattice with bottom, then we get that factor_set is a complete lattice and we get GCD (infimum) and LCM (supremum) of arbitrary sets. a ⊔ b + a ⊓ b = a + b is the fact that gcd a b * lcm a b = a * b expressed as (extended) multiset of factors.

#### Kevin Buzzard (Sep 02 2018 at 21:33):

you surely can't take an LCM of an arbitrary set -- you mean an arbitrary finite set?

#### Mario Carneiro (Sep 02 2018 at 21:34):

No, an arbitrary set. That's cool!

#### Kevin Buzzard (Sep 02 2018 at 21:36):

just to be clear then -- is the LCM of all the primes which are 1 mod 4 equal to zero?

#### Kevin Buzzard (Sep 02 2018 at 21:36):

That's cool!

That's CS nonsense :-)

#### Mario Carneiro (Sep 02 2018 at 21:36):

It is a bit funny that with this interpretation 3 | 2^infty

#### Mario Carneiro (Sep 02 2018 at 21:37):

Yes, all unbounded LCMs are zero

#### Kevin Buzzard (Sep 02 2018 at 21:38):

I have actually seen some version of this which is not what Johannes has used, and it's the order of a profinite group. A general order is $\Pi_pp^{e_p}$ with $e_p$ allowed to be all non-zero and even all infinity (indeed the order of the profinite completion of the integers is $\Pi_pp^\infty$)

#### Kevin Buzzard (Sep 02 2018 at 21:38):

and with interpretation sanity prevails again and 3 does not divide $2^\infty$

#### Mario Carneiro (Sep 02 2018 at 21:39):

I guess the more mathematically natural approach just completes the multisets as functions Prime -> with_top nat

#### Mario Carneiro (Sep 02 2018 at 21:39):

I think that's the same as what you suggest

#### Kevin Buzzard (Sep 02 2018 at 21:39):

that would be for profinite orders

#### Kevin Buzzard (Sep 02 2018 at 21:40):

the far more mathematically natural way to do this UFD thing would just be to ignore zero rather than shoehorn it in

#### Kevin Buzzard (Sep 02 2018 at 22:57):

I suppose another way which would look more natural to a mathematician would be to embed the multisets into the partially ordered set of principal ideals. Then one can see what the natural lattice structure is -- you can embed the principal ideals into the lattice of all ideals. Here you see the "correct" GCD of X and Y in the polynomial ring K[X,Y] in two variables -- rather than the empty multiset it's the non principal ideal generated by X and Y. The notion of GCD in a UFD does not seem so useful to me -- you can't solve lX + mY = GCD in general, for example. Still I can imagine you guys finding some sort of strange use for it...

#### Kevin Buzzard (Sep 02 2018 at 22:57):

.. maybe a Galois insertion or something...

#### Johan Commelin (Sep 03 2018 at 04:15):

Right, I think what Kevin suggests would be very useful. Take gcd's as ideals, and you open up another realm of interesting theorems to be formalized...

Last updated: May 12 2021 at 08:14 UTC