minpoly for mat same minpoly for lin

Stream: new members

[MohanadAhmed]

Hello

How would one prove that the minimal polynomial of a matrix and the corresponding linear map are the same? Unfolding the definitions leads to some scary definitions. In mathlib the statement seems to be there for charpoly at docs#linear_algebra.charpoly.to_matrix. The proof at proof is .... well .... well beyond my mathlib understanding capabilities. :sweat_smile:

What I tried is doing unfolds till I reached the goals shown in the image below. If somehow I can say the yellow parts and the green parts are the same then it should work right? But I am guessing that is probably not the best approach.

image.png

import linear_algebra.matrix.spectrum
import linear_algebra.eigenspace
import linear_algebra.charpoly.basic
import linear_algebra.matrix.charpoly.coeff
import linear_algebra.charpoly.to_matrix
import linear_algebra.matrix.charpoly.minpoly
import linear_algebra.matrix.to_linear_equiv

open matrix polynomial
open linear_map module.End
open_locale matrix big_operators

variables {n: Type*}[fintype n][decidable_eq n] --[nonempty n]
variables {R: Type*}[field R][is_alg_closed R]

lemma mat_minpoly_is_linmap_minpoly (A: matrix n n R) :
  minpoly R A = minpoly R (to_lin' A) :=
begin
 -- unfold minpoly, unfold to_lin', unfold to_matrix', dsimp,
  sorry,
end

lemma root_minpoly_is_root_minpoly (A: matrix n n R) (μ: R):
  (minpoly R A).is_root μ ↔ (minpoly R (to_lin' A)).is_root μ :=
begin
  sorry,
end

[Eric Wieser]

The green parts will follow with some effort from docs#map_is_integral I think

[Eric Wieser]

Though you'll need to first rewriteto_lin' to docs#matrix.to_lin_alg_equiv'

[Eric Wieser]

The yellow parts will follow from polynomial.aeval_alg_hom

[Riccardo Brasca]

In general unfolding definitions leads to scary things. Have you tried to use the API as in the normal mathematical proof?

[Riccardo Brasca]

If you find that certains lemmas are missing we can add them

[Riccardo Brasca]

I mean, the standard math proof is that one divides the other, that is irreducible and both are monic, so OK

[Riccardo Brasca]

The divisibility comes from something being an algebra iso and property of evaluation. I am pretty sure everything is there

[MohanadAhmed]

Hello @Riccardo Brasca . Thanks for your suggestions.
So I took a look at the lemmas associated with minpoly and applied some of them. I now need to prove that the minpoly of the matrix evaluated at the linear map is zero. I don't know if this is a reduction of the problem or not? Any suggestions or thoughts for that one:

I to a look at the proof of docs#minpoly.aeval located here proof. I think we come round to the same problem that was ealier i.e. polynomials evaluated with the other type. So matrix polynomial evaluated with linear_map or vice versa.

⇑(aeval (⇑to_lin' A))
    (degree_lt_wf.min (λ (p : polynomial R), p.monic ∧ eval₂ (algebra_map R (matrix n n R)) A p = 0) hx) =
  0

import linear_algebra.matrix.spectrum
import linear_algebra.eigenspace
import linear_algebra.charpoly.basic
import linear_algebra.matrix.charpoly.coeff
import linear_algebra.charpoly.to_matrix
import linear_algebra.matrix.charpoly.minpoly
import linear_algebra.matrix.to_linear_equiv
import linear_algebra.matrix.basis

open matrix polynomial
open linear_map module.End
open_locale matrix big_operators

variables {n: Type*}[fintype n][decidable_eq n] --[nonempty n]
variables {R: Type*}[field R][is_alg_closed R]
variables {Z: matrix n n R}
variables {p: polynomial R}

lemma mat_minpoly_is_linmap_minpoly [nonempty n][is_domain (matrix n n R)] (A: matrix n n R) :
  minpoly R A = minpoly R (to_lin' A) :=
begin
  apply minpoly.eq_of_irreducible_of_monic,
  apply minpoly.irreducible,
  exact is_integral,
  rotate,
  exact minpoly.monic is_integral,
  -- Here we need to prove : ⇑(aeval (⇑to_lin' A)) (minpoly R A) = 0.
  delta minpoly,
  split_ifs with hx,
-- The goal now becomes
/- ⇑(aeval (⇑to_lin' A))
    (degree_lt_wf.min (λ (p : polynomial R), p.monic ∧ eval₂ (algebra_map R (matrix n n R)) A p = 0) hx) =
  0 -/
end

[Eric Wieser]

polynomial.aeval_alg_hom should help here

[Eric Wieser]

Also, [is_domain (matrix n n R)] is a _very_ strong assumption, that forces either n < 2 or subsingleton R

[Eric Wieser]

Here's a proof:

lemma mat_minpoly_is_linmap_minpoly [nonempty n] (A : matrix n n R) :
  minpoly R (to_lin' A) = minpoly R A :=
begin
  let e : matrix n n R ≃ₐ[R] _ := to_lin_alg_equiv',
  change minpoly R (e A) = minpoly R A,
  rw [minpoly, minpoly],
  simp_rw [←polynomial.aeval_def, aeval_alg_equiv, alg_hom.comp_apply, alg_equiv.coe_alg_hom,
    add_equiv_class.map_eq_zero_iff],
  symmetry,
  apply dif_ctx_congr (is_integral_alg_equiv e).symm _ (λ _, rfl),
  intro h,
  congr,
end

[Eric Wieser]

Riccardo Brasca said:

If you find that certains lemmas are missing we can add them

#19030

[Eric Wieser]

With that PR, the proof is just minpoly_alg_equiv to_lin_alg_equiv' A or similar

[Eric Wieser]

#19036 adds the requested result (and three other analogous ones)

[Eric Wieser]

@MohanadAhmed, maybe these new lemmas now help with your eigenvalue work. simp should close the goal now.

[MohanadAhmed]

Yes they will help I was working around them by going through the has_eigenvalue definition.

So root of charpoly is equivalent to has_eigenvalue is equivalent to root of minpoly of the endomorphism to_lin: A

Now I think I can cut some of the middle man work

[MohanadAhmed]

https://github.com/MohanadAhmed/lean-matrix-cookbook/blob/master/src/matrix_cookbook/mat_eigs_lib.lean