Zulip Chat Archive

Stream: maths

Topic: Duplication `is_integral R x` / `x ∈ integral_closure R x`


view this post on Zulip Anne Baanen (May 06 2021 at 10:44):

I am mildly annoyed that there are two (defeq) ways to spell "x : S is the root of a monic polynomial over R": is_integral R x and x ∈ integral_closure R S. Writing is_integral is closer to mathematical practice, but using integral_closure you get a lot of results for free: since integral_closure is a subalgebra, you can apply subalgebra.pow_mem, subalgebra.multiset_prod_mem, ...

Any thoughts on whether and how we might improve this situation?

view this post on Zulip Johan Commelin (May 06 2021 at 10:59):

Are they both defined in the same generality?

view this post on Zulip Anne Baanen (May 06 2021 at 11:01):

(docs#is_integral, docs#integral_closure)

view this post on Zulip Anne Baanen (May 06 2021 at 11:01):

Ah no, A is a comm_ring in integral_closure but just a ring in is_integral

view this post on Zulip Anne Baanen (May 06 2021 at 11:02):

I don't remember whether commutativity of A is really needed to turn the integral closure into a subalgebra, or that this is just convenient for mathlib's usage.

view this post on Zulip Johan Commelin (May 06 2021 at 11:03):

We should ask Lean (-;

view this post on Zulip Eric Wieser (May 06 2021 at 11:37):

This problem exists everywhere we have bundled objects, right? For instance, here are some of the ways to say "apply a function at i", (λ f, f i):

I think the best thing to do is make it clear what the underlying unbundled version is in the documentation

view this post on Zulip Patrick Massot (May 06 2021 at 11:50):

Anne Baanen said:

I don't remember whether commutativity of A is really needed to turn the integral closure into a subalgebra, or that this is just convenient for mathlib's usage.

It is essential. Take R = int, A is 2x2 matrices with rational coefficients. Both (0010)\begin{pmatrix}0 & 0\\1 & 0\end{pmatrix} and (01/200)\begin{pmatrix}0 & 1/2\\0 & 0\end{pmatrix} are integral but there product isn't.

view this post on Zulip Johan Commelin (May 06 2021 at 11:52):

Their sum isn't, I guess. But the product is just the same as the second matrix, right?

view this post on Zulip Kevin Buzzard (May 06 2021 at 11:54):

Their product depends on which way you're producting them :-) Certainly the square of their sum isn't integral, which suffices.

view this post on Zulip Patrick Massot (May 06 2021 at 11:55):

I meant the product in the order I used.

view this post on Zulip Patrick Massot (May 06 2021 at 11:56):

I haven't checked with Lean, but I hope (0010)(01/200)=(0001/2)\begin{pmatrix}0 & 0\\1 & 0\end{pmatrix}\begin{pmatrix}0 & 1/2\\0 & 0\end{pmatrix} = \begin{pmatrix}0 & 0\\0 & 1/2\end{pmatrix}

view this post on Zulip Johan Commelin (May 06 2021 at 11:56):

I guess I'm no longer able to compute matrix multiplications in my head :face_palm:

view this post on Zulip Kevin Buzzard (May 06 2021 at 11:57):

The product equation might even be true over nat and Z/2Z\Z/2\Z!

view this post on Zulip Patrick Massot (May 06 2021 at 11:59):

I'm pretty sure we already had this discussion in December. I found this example in my notes from when I was teaching this earlier this year.

view this post on Zulip Kevin Buzzard (May 06 2021 at 12:00):

I think it might have been in private messages -- I do remember discussing this example though.

view this post on Zulip Johan Commelin (May 06 2021 at 12:02):

(I don't remember making the same mistake with the multiplication... :laughing:)

view this post on Zulip Patrick Massot (May 06 2021 at 12:02):

I was the one doing the mistake at that time

view this post on Zulip Patrick Massot (May 06 2021 at 12:02):

What a brilliant team.

view this post on Zulip Patrick Massot (May 06 2021 at 12:03):

Great minds think alike

view this post on Zulip Yaël Dillies (May 06 2021 at 13:39):

Two idiots one thought, as we say in German.

view this post on Zulip Jasmin Blanchette (May 06 2021 at 13:47):

You mean: Great minds think alike. ;)

view this post on Zulip Yaël Dillies (May 06 2021 at 13:49):

Great minds think alike!

view this post on Zulip Johan Commelin (May 06 2021 at 13:55):

I've also heard "Fools never differ" as a reply to "Great minds think alike" :grinning: :see_no_evil:

view this post on Zulip Mario Carneiro (May 07 2021 at 00:50):

I think that's actually the continuation of the original quote. Everyone just cuts that last part off


Last updated: Jun 17 2021 at 16:20 UTC