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

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 yamls, 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