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

Stream: maths

[Anne Baanen]

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]

Are they both defined in the same generality?

[Anne Baanen]

(docs#is_integral, docs#integral_closure)

[Anne Baanen]

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

[Anne Baanen]

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.

[Johan Commelin]

We should ask Lean (-;

[Eric Wieser]

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

• docs#function.eval
• docs#add_monoid_hom.apply
• docs#monoid_hom.apply
• docs#ring_hom.apply
• docs#linear_map.proj
• docs#alg_hom.apply

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

[Patrick Massot]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

I meant the product in the order I used.

[Patrick Massot]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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]

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

[Johan Commelin]

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

[Patrick Massot]

I was the one doing the mistake at that time

[Patrick Massot]

What a brilliant team.

[Patrick Massot]

Great minds think alike

[Yaël Dillies]

Two idiots one thought, as we say in German.

[Jasmin Blanchette]

You mean: Great minds think alike. ;)

[Yaël Dillies]

Great minds think alike!

[Johan Commelin]

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

[Mario Carneiro]

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