Zulip Chat Archive

Stream: maths

Topic: UFD


view this post on Zulip Kenny Lau (Sep 02 2018 at 20:36):

Johannes just added UFD!

view this post on Zulip Kenny Lau (Sep 02 2018 at 20:36):

@Kevin Buzzard

view this post on Zulip 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[x] (KK the field of fractions of RR) being "the same" as factoring in R[x]R[x], RR a UFD implies R[x]R[x] a UFD.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 02 2018 at 20:58):

Could you explain what looks different?

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 20:59):

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

view this post on Zulip Patrick Massot (Sep 02 2018 at 20:59):

Come on! The Wikipedia page you linked to even mention Galois connections!

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 20:59):

ha ha

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 20:59):

I would have just done the maths stuff

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 20:59):

not the weird CS stuff

view this post on Zulip 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.

view this post on Zulip 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?!?

view this post on Zulip Patrick Massot (Sep 02 2018 at 21:02):

Kevin, do you understand what this mean?

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 21:02):

they're multisets maybe?

view this post on Zulip 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 :(

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 21:25):

right :-)

view this post on Zulip 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 -- ?!

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 02 2018 at 21:34):

No, an arbitrary set. That's cool!

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 21:36):

That's cool!

That's CS nonsense :-)

view this post on Zulip Mario Carneiro (Sep 02 2018 at 21:36):

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

view this post on Zulip Mario Carneiro (Sep 02 2018 at 21:37):

Yes, all unbounded LCMs are zero

view this post on Zulip 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 Πppep\Pi_pp^{e_p} with epe_p allowed to be all non-zero and even all infinity (indeed the order of the profinite completion of the integers is Πpp\Pi_pp^\infty)

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 21:38):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 02 2018 at 21:39):

I think that's the same as what you suggest

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 21:39):

that would be for profinite orders

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 22:57):

.. maybe a Galois insertion or something...

view this post on Zulip 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