# Zulip Chat Archive

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

(docs#is_integral, docs#integral_closure)

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

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

We should ask Lean (-;

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

:

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