Minimal polynomials

Stream: maths

[Aaron Anderson]

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]

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

[Aaron Anderson]

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]

What's the integral closure of a noncommutative ring?

[Aaron Anderson]

Integral closure still assumes commutativity.

[Aaron Anderson]

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]

Oh I see.

[Adam Topaz]

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

[Aaron Anderson]

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]

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

[Aaron Anderson]

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

[Aaron Anderson]

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]

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

[Aaron Anderson]

@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]

@Patrick Massot what do you think? Should we just link to minimal_polynomial for the minpoly of a matrix?

[Anne Baanen]

If I had to choose one, then it would be matrix.is_integral, because it contains the matrix/linear algebra specific work.