# Zulip Chat Archive

## Stream: maths

### Topic: Minimal polynomials

#### Aaron Anderson (Aug 31 2020 at 00:52):

I'm trying to remove the assumptions of commutativity required to define minimal polynomials, so that we can use them in linear algebra, over at branch#minimal_polynomial_noncomm

#### Aaron Anderson (Aug 31 2020 at 00:52):

Everything appears to be working without too much effort, except for the theorem docs#integral_closure_idem

#### Aaron Anderson (Aug 31 2020 at 00:55):

Can anyone help me troubleshoot what's gone wrong? I've changed the instance assumptions of `is_integral`

to let one `semiring`

be noncommutative, but I don't know what that's breaking

#### Adam Topaz (Aug 31 2020 at 01:10):

What's the integral closure of a noncommutative ring?

#### Aaron Anderson (Aug 31 2020 at 01:11):

Integral closure still assumes commutativity.

#### Aaron Anderson (Aug 31 2020 at 01:12):

I've only changed the assumption on the basic definition `is_integral`

, which amounts to being the root of a monic polynomial, and three lemmas about `is_integral`

that don't deal with integral closures per se.

#### Adam Topaz (Aug 31 2020 at 01:14):

Oh I see.

#### Adam Topaz (Aug 31 2020 at 01:17):

I'm not on a computer, but my guess is that it's an issue with `is_integral_trans`

#### Aaron Anderson (Aug 31 2020 at 01:21):

Taking it apart, this almost works:

```
theorem integral_closure_idem {R : Type*} {A : Type*} [comm_ring R] [comm_ring A] [algebra R A] :
integral_closure (integral_closure R A : set A) A = ⊥ :=
eq_bot_iff.2 $ λ x hx, algebra.mem_bot.2
⟨⟨x, by { apply is_integral_trans _ _ hx, exact (integral_closure R A).algebra,
swap, apply integral_closure.is_integral, sorry }⟩, rfl⟩
```

but I'd need to synthesize the `is_scalar_tower`

instance.

#### Aaron Anderson (Aug 31 2020 at 01:21):

Of course, I'd really rather not butcher this proof over this bug.

#### Aaron Anderson (Aug 31 2020 at 01:22):

(My branch is building, but that's because I've commented out that theorem)

#### Aaron Anderson (Aug 31 2020 at 05:14):

Ok, I've got a workaround, but I'd still appreciate insight as to why I need to declare this one instance manually, so I can fix it:

```
theorem integral_closure_idem {R : Type*} {A : Type*} [comm_ring R] [comm_ring A] [algebra R A] :
integral_closure (integral_closure R A : set A) A = ⊥ :=
eq_bot_iff.2 $ λ x hx, algebra.mem_bot.2
⟨⟨x, @is_integral_trans _ _ _ _ _ _ _ _ (integral_closure R A).algebra _ integral_closure.is_integral x hx⟩, rfl⟩
```

#### Kenny Lau (Aug 31 2020 at 10:00):

It looks like it is caused by the diamond `subalgebra -> subring -> ring`

and `subalgebra -> comm_ring -> ring`

#### Aaron Anderson (Sep 25 2020 at 23:58):

@Johan Commelin , I could add minimal polynomials of endomorphisms or matrices to the `yaml`

s, but there's no one `decl`

, as at @Anne Baanen's advice (which did simplify things), I've been working directly with expressions of the form `minimal_polynomial f.is_integral`

. Should I define `min_poly`

somewhere, so we can link to it?

#### Johan Commelin (Sep 26 2020 at 05:27):

@Patrick Massot what do you think? Should we just link to `minimal_polynomial`

for the minpoly of a matrix?

#### Anne Baanen (Sep 26 2020 at 10:44):

If I had to choose one, then it would be `matrix.is_integral`

, because it contains the matrix/linear algebra specific work.

Last updated: May 12 2021 at 08:14 UTC