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 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: Dec 20 2023 at 11:08 UTC