UFD

Stream: maths

[Kenny Lau]

Johannes just added UFD!

[Kenny Lau]

@Kevin Buzzard

[Kevin Buzzard]

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]

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]

Could you explain what looks different?

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

ha ha

[Kevin Buzzard]

I would have just done the maths stuff

[Kevin Buzzard]

not the weird CS stuff

[Patrick Massot]

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]

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

[Patrick Massot]

Kevin, do you understand what this mean?

[Kevin Buzzard]

they're multisets maybe?

[Patrick Massot]

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]

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]

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]

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]

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

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

[Kevin Buzzard]

right :-)

[Kevin Buzzard]

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]

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]

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]

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

[Mario Carneiro]

No, an arbitrary set. That's cool!

[Kevin Buzzard]

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

[Kevin Buzzard]

That's cool!

That's CS nonsense :-)

[Mario Carneiro]

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

[Mario Carneiro]

Yes, all unbounded LCMs are zero

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

I think that's the same as what you suggest

[Kevin Buzzard]

that would be for profinite orders

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

.. maybe a Galois insertion or something...

[Johan Commelin]

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...