## Stream: maths

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

#### 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?

#### Johan Commelin (May 06 2021 at 10:59):

Are they both defined in the same generality?

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

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

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

#### 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 $\begin{pmatrix}0 & 0\\1 & 0\end{pmatrix}$ and $\begin{pmatrix}0 & 1/2\\0 & 0\end{pmatrix}$ are integral but there product isn't.

#### 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?

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

#### Patrick Massot (May 06 2021 at 11:55):

I meant the product in the order I used.

#### Patrick Massot (May 06 2021 at 11:56):

I haven't checked with Lean, but I hope $\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}$

#### Johan Commelin (May 06 2021 at 11:56):

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

#### Kevin Buzzard (May 06 2021 at 11:57):

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

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

#### Kevin Buzzard (May 06 2021 at 12:00):

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

#### Johan Commelin (May 06 2021 at 12:02):

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

#### Patrick Massot (May 06 2021 at 12:02):

I was the one doing the mistake at that time

#### Patrick Massot (May 06 2021 at 12:02):

What a brilliant team.

#### Patrick Massot (May 06 2021 at 12:03):

Great minds think alike

#### Yaël Dillies (May 06 2021 at 13:39):

Two idiots one thought, as we say in German.

#### Jasmin Blanchette (May 06 2021 at 13:47):

You mean: Great minds think alike. ;)

#### Yaël Dillies (May 06 2021 at 13:49):

Great minds think alike!

#### 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:

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