diagonalizable linear maps

Stream: Is there code for X?

[Lawrence Wu (llllvvuu)]

Should we have a definition like this? Or what would be the way to prove a theorem like "a linear map is diagonalizable iff its minpoly splits and is squarefree"?

def LinearMap.IsDiagonalizable {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M]
    (f : Module.End R M) : Prop :=
  ∃ (ι : Type v) (b : Module.Basis ι R M) (μ : ι → R), ∀ i : ι, f.HasEigenvector (μ i) (b i)

[Kevin Buzzard]

That looks like a good definition of diagonalizable to me

[Jireh Loreaux]

I think Diagonalization should be a structure.

[Eric Wieser]

Like this?

structure LinearMap.Diagonalization (ι : Type*} {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M]
    (f : Module.End R M) extends Module.Basis ι R M where
  μ : ι → R
  hasEigenVector_μ (i : ι) : f.HasEigenvector (μ i) (toBasis i)

[Lawrence Wu (llllvvuu)]

We can also have a sorted version on Fin (I don’t need it, but it’s what we have for LinearMap.IsSymmetric)

[Kevin Buzzard]

On Fin you can also have UpperTriangularization

[Kenny Lau]

we would need to think about whether we want to make μ computable

[Eric Wieser]

What do you mean by that?

[Kenny Lau]

structure LinearMap.Diagonalization (ι : Type*} {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M]
    (f : Module.End R M) extends Module.Basis ι R M where
  exists_hasEigenVector (i : ι) : ∃ μ, f.HasEigenvector μ (toBasis i)

[Eric Wieser]

I think the only reason to prefer that spelling is it saves us proving the ext theorem that it suffices for the basis part to agree

[Eric Wieser]

.. assuming that property is actually true in that level of generality;

[Kenny Lau]

they are both extensional (i think)

[Kenny Lau]

oh wait, it's a ring not a field

[Kenny Lau]

yeah i think they're still equivalent

[Kenny Lau]

if μ1 v = μ2 v then (μ1-μ2) v = 0 but basis -> linearly independent -> μ1-μ2=0

[Eric Wieser]

So let's write the version with a mu field so that you can write that theorem to prove it :)

[Kenny Lau]

I think my comment came from our awful definition of AlgebraicGeometry.Scheme.Cover which is very much not extensional because of the extra data f but which I was told that this is a nofix because it's being deprecated soon :tm:

[Kevin Buzzard]

Kenny Lau said:

if μ1 v = μ2 v then (μ1-μ2) v = 0 but basis -> linearly independent -> μ1-μ2=0

Can you change basis and change the eigenvalues for some non-reduced ring? e.g mod 8 the matrices diag(1,7) and diag(3,5) have the same char poly, but they don't seem to be conjugate in GL_2(Z/8).

[Kevin Buzzard]

(pari)

? [a,b;c,d]*[Mod(1,8),0;0,Mod(7,8)]-[Mod(3,8),0;0,Mod(5,8)]*[a,b;c,d]
%1 =
[Mod(6, 8)*a Mod(4, 8)*b]

[Mod(4, 8)*c Mod(2, 8)*d]

so a,b,c,d would all have to be even to make this the zero matrix, which would mean ad-bc can't be a unit.

[Kenny Lau]

oh, i haven't thought about that extensionality...

[Kenny Lau]

i was just thinking about "mu is extra data (given the basis of eigenvectors)", and it seems like you are additionally thinking about "mu is unique up to ordering"

[Kenny Lau]

@Aaron Liu do you think this is true?

[Aaron Liu]

what's going on

[Aaron Liu]

what's the problem

[Kenny Lau]

Aaron Liu said:

what's going on

let f:R^n -> R^n be a linear map, R is a ring,
let {v1, ..., vn} be a basis of eigenvectors,
let {w1, ..., wn} be another basis of eigenvectors,
then their eigenvalues are the same up to ordering

[Kenny Lau]

i think it's true

[Kenny Lau]

@Kevin Buzzard because like for simplicity pretend v1 .... vn all have distinct eigenvalues,
then write w1 = sum ai vi
then f(wi) = sum ai λi vi = sum ai λ1' vi
by invertibility stuff, (a1, ..., an) = (1) so we should be able to conclude λ1' = one of the λi

[Kenny Lau]

hmm ok i'm not convinced by my argument

[Aaron Liu]

n is finite?

[Kenny Lau]

all i can conclude is that ai (λ1' - λi) = 0 for all i,
and in the classical case: (you use the fact that it's a field to conclude that ai=0 or λ1'=λi, and by invertibility there must be a non-zero ai)

[Aaron Liu]

can I use a weird ring

[Kenny Lau]

of course

[Kenny Lau]

i think i want to use Z/6Z with (ai) = (2,3) and λ1' = 0 and (λi) = (3,2)

[Kenny Lau]

which means... consider diag(3,2) with coeffs in Z/6Z,
then (2,3) is an eigenvector with eigenvalue 0
and its complement... (3,2) has eigenvalue -1

[Kenny Lau]

oh god

[Aaron Liu]

is the ring has to be comm

[Kenny Lau]

so, mu is not unique up to ordering, but it's still derivable from the basis

[Kenny Lau]

well my ring is comm and it already fails

[Aaron Liu]

what's the counterexample

[Kenny Lau]

diag(3,2),
standard basis has eigenvalues (3, 2)
the cursed basis ((2,3), (3,2)) has eigenvalues (0, -1)

[Aaron Liu]

what is a diag(3,2)

[Kenny Lau]

$\begin{pmatrix}3&0\\0&2\end{pmatrix}$

[Aaron Liu]

oh makes sense

[Aaron Liu]

somewhat cursed basis has weird eigenvalues

[Kenny Lau]

i'm sure @Eric Wieser will be overjoyed to hear about this counterexample

[Kenny Lau]

actually we should formalise it in Counterexample/

[Kenny Lau]

(right after Diagonalization gets merged)

[Aaron Liu]

oh (Z/6Z)[X] doesn't have unique factorization

[Kenny Lau]

is that because 2*2 = -1*2

[Kenny Lau]

wait, then that means 2 is not irreducible

[Aaron Liu]

well look at X*(X+1) = (X+3)*(X+4)

[Kenny Lau]

oh, missed the [X]

[Kenny Lau]

well i think 3 = 3 * 3 is still a big problem even inside (Z/6Z)[X]

[Kenny Lau]

is X irreducible?

[Kenny Lau]

uh, X = (2X+3) * (3X+2)

[Kenny Lau]

Aaron Liu said:

oh (Z/6Z)[X] doesn't have unique factorization

I think you have a way bigger problem here... I don't think anything is irreducible, so how can you factorise anything into irreducibles

[Aaron Liu]

so you end up with this degree 2 polynomial having 4 roots

[Aaron Liu]

maybe it works better in integral domains

[Kevin Buzzard]

The concept of factorization is kind of dead in the water if you have zero divisors.

[Kevin Buzzard]

An exercise which totally stumped me for a while as an undergraduate was: "Figure out all the ideals of $\Z/6\Z$. Is it a PID?". The ideals are all principal, so obviously it was a PID, but then that would mean it was a UFD and it clearly wasn't because you can't have $2\times 3=0$ in a UFD. Took a while for the penny to drop that it wasn't a PID because although it was a PI, it wasn't a D.

[Edison Xie]

Kevin Buzzard said:

although it was a PI, it wasn't a D.

that was an end of term exam question for me as a year two student and I thought it was a PID at that time :joy:

[Lawrence Wu (llllvvuu)]

OK, I'm cooking it up: #29610 if there is API people think should be added let me know.

Should I try to cover simultaneous diagonalizability in the same definition or nah? Something like

structure LinearMap.Diagonalization.{u, v} (α ι : Type*) {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M]
    (f : α → Module.End R M) extends Module.Basis ι R M where
  μ : α → ι → R
  hasEigenVector_μ (a : α) (i : ι) : (f a).HasEigenvector (μ a i) (toBasis i)

Or maybe it would make some of the single diagonalizable map stuff too awkward?

[Lawrence Wu (llllvvuu)]

Seems to work so far:

import Mathlib

namespace LinearMap

open Module Matrix Polynomial

variable {α R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]

structure SimultaneousDiagonalization (ι : Type*) (f : α → End R M) extends Basis ι R M where
  μ : α → ι → R
  hasEigenVector_μ (a : α) (i : ι) : (f a).HasEigenvector (μ a i) (toBasis i)

abbrev Diagonalization (ι : Type*) (f : End R M) := SimultaneousDiagonalization ι fun _ : Unit ↦ f

def Diagonalization.mk {ι : Type*} {f : End R M} {b : Basis ι R M} {μ : ι → R}
    (h : ∀ i, f.HasEigenvector (μ i) (b i)) : f.Diagonalization ι :=
  { toBasis := b, μ := fun _ ↦ μ, hasEigenVector_μ := fun _ => h }

def Diagonalization.μ {ι : Type*} {f : End R M} (self : f.Diagonalization ι) :=
  SimultaneousDiagonalization.μ self ()

def Diagonalization.hasEigenVector_μ {ι : Type*} {f : End R M}
    (self : f.Diagonalization ι) (i : ι) : f.HasEigenvector (self.μ i) (self.toBasis i) :=
  SimultaneousDiagonalization.hasEigenVector_μ self () i

def SimultaneousDiagonalization.diagonalization {ι : Type*} {f : α → Module.End R M}
    (D : SimultaneousDiagonalization ι f) (a : α) : (f a).Diagonalization ι :=
  Diagonalization.mk (D.hasEigenVector_μ a)

@[ext]
theorem SimultaneousDiagonalization.ext {ι : Type*} {f : α → End R M}
    {D₁ D₂ : SimultaneousDiagonalization ι f} (h : D₁.toBasis = D₂.toBasis) : D₁ = D₂ := by
  suffices D₁.μ = D₂.μ by cases D₁; cases D₂; simp_all only
  ext a i
  suffices D₁.μ a i • D₁.toBasis i = D₂.μ a i • D₁.toBasis i by
    simpa using congr(D₁.toBasis.repr $this i)
  rw [← (D₁.hasEigenVector_μ a i).apply_eq_smul, h, ← (D₂.hasEigenVector_μ a i).apply_eq_smul]

example {ι} {f : Module.End R M} {D₁ D₂ : f.Diagonalization ι} (h : D₁.toBasis = D₂.toBasis) :
    D₁ = D₂ := by
  ext : 1
  exact h

lemma Diagonalization.toMatrix_eq_diagonal {ι : Type*} [Fintype ι] [DecidableEq ι]
    {f : End R M} (D : f.Diagonalization ι) : f.toMatrix D.toBasis D.toBasis = diagonal D.μ := by
  ext i j
  simp [toMatrix_apply, (D.hasEigenVector_μ j).apply_eq_smul]
  grind [Finsupp.single_apply, diagonal_apply]

-- note: Nontrivial R golfed in #29420
lemma Diagonalization.charpoly_eq {ι : Type*} [Fintype ι] [DecidableEq ι] [Nontrivial R] [Free R M]
    [Module.Finite R M] {f : End R M} (D : f.Diagonalization ι) :
    f.charpoly = ∏ i, (X - C (D.μ i)) := by
  rw [← f.charpoly_toMatrix D.toBasis, D.toMatrix_eq_diagonal, charpoly_diagonal]

end LinearMap

[Eric Wieser]

Is a simultaneous diagonalization just a diagonalization of the block diagonal map?

[Scott Carnahan]

It is diagonalization of block diagonal by “block scalar” (meaning block diagonal with identical blocks).

[Eric Wieser]

Ah, and I guess because the basis is bundled you can't just instantiate with Module.Basis.pi

[Lawrence Wu (llllvvuu)]

maybe it works better in integral domains

That's enough to fix the statement. The following is true:

theorem LinearMap.Diagonalization.μ_unique {ι ι' R M : Type*} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M]
    {f : Module.End R M} {D₁ : f.Diagonalization ι} {D₂ : f.Diagonalization ι'} :
    ∃ e : ι ≃ ι', D₁.μ = D₂.μ ∘ e := by
  sorry

I was too small-brained to immediately see why, so I asked Aristotle to prove it: https://gist.github.com/llllvvuu/b4fd97595ca34cfa1623355a6815254d

Seems like the reason is that if you take an eigenvector (mu, v) in its repr c in any diagonalization D, then we have ∀ j ∈ c.support → c j • D.μ j = c j • mu, and only in integral domains can we cancel c j and conclude that D includes a basis of every eigenspace.

(EDIT: just realized there's an easier route that goes through docs#Polynomial.roots_prod and #29526.)

[Lawrence Wu (llllvvuu)]

#29610 is ready for review (dependency on #29420 is minor)

[Kenny Lau]

@Lawrence Wu (llllvvuu) Consider the following counterexample: R=ℕ, M=ℕ, N=3*ℕ-{3}

[Kenny Lau]

actually there is no need for 3, consider N=ℕ-{1} instead

[Kenny Lau]

@Lawrence Wu (llllvvuu) out of curiosity, how much of the code is yours and how much is aristotle's?

[Lawrence Wu (llllvvuu)]

Kenny Lau said:

out of curiosity, how much of the code is yours and how much is aristotle's?

I chuck every theorem into Aristotle and then I golf it. I guess my golfing touches close to 100% line-of-code-wise but is a minority of the effort. The only ones I don't do are the ones where I can write the one liner in a few seconds (which is not all one-liners), and sometimes when I'm experimenting, e.g. exists_diagonalization_iff_directSum I was experimenting with the PID stuff.

[Kenny Lau]

thanks for the information!

[Kenny Lau]

Lawrence Wu (llllvvuu) said:

theorem

so i assume the initial definitions (and also subsequent defs) are 0% aristotle? and also, does aristotle have access to the mathlib theorems?

[Lawrence Wu (llllvvuu)]

so i assume the initial definitions (and also subsequent defs) are 0% aristotle? and also, does aristotle have access to the mathlib theorems?

It can make its own defs and API, but if I know the end goal is a mathlib PR then I will write the defs and API (signatures) myself. Or for example, in this case: https://gist.github.com/lawrence-harmonic/5f37baa0eecab2ccfca3cf3a7af3bbd5 Aristotle generated two helper lemmas but I changed the API to be more idiomatic for #29478 . In that example it can also be seen that yes, it does use, even abuse, mathlib definitions and theorems (this was an extreme case of an unoptimized proof that I golfed a lot, but it was helpful to have the key manipulations written there and the golfing is always pretty low-effort).

[Lawrence Wu (llllvvuu)]

small bikeshed, are the names here (SimultaneousDiagonalization/Diagonalization) good or should I do like CommonEigenbasis/Eigenbasis?

[Eric Wieser]

Eigenbasis sounds better to me

[Lawrence Wu (llllvvuu)]

/poll Name?
Diagonalization/SimultaneousDiagonalization
Eigenbasis/CommonEigenbasis
other

[Kenny Lau]

I would suggest Eigenbasis but also make sure that the docstring mentions "diagonalization" so that it can be discovered with leanexplore

[Kenny Lau]

I think we really have a problem with our naming scheme

[Jireh Loreaux]

In what sense?

[Kenny Lau]

there's no good way to refer to one thing by two names (or rather we have decided not to). e.g. the whole VectorSpace business we had, which makes Lean less beginner-friendly (when it already is very much not)

[Kenny Lau]

I feel like notation "VectorSpace" => Module might work

[Jireh Loreaux]

VectorSpace may yet make a comeback, hold on to your hats. :wink: (there's some work going on about making collections of classes usable in practice, to the point that having VectorSpace as a kind of abbreviation for [AddCommGroup V] [Field 𝕜] [Module 𝕜 V] would be not just doable, but probably even standard; this is not yet ironed out though.)

[Kenny Lau]

who is "we"?

[Jireh Loreaux]

I didn't say "we". But see lean4#8279.

[Kenny Lau]

I think the implementation of abbrev is not sufficient for the type of aliasing that I want in my head that I suggested with notation

[Kenny Lau]

obviously notation is morally the wrong thing to choose, but it works the best

[Kenny Lau]

(maybe that was the point of the issue that you linked to)

[Jireh Loreaux]

note that the existing class abbrev is even different from class Foo .... attribute [reducible, inline] Foo.

[Ryan Smith]

Kenny Lau said:

Lawrence Wu (llllvvuu) out of curiosity, how much of the code is yours and how much is aristotle's?

Is Aristotle publicly available for lean work? I saw something on their website about ios but that doesn't seem relevant. Gauss looks like it has a form to request access. Are there any other publicly announced and available assistants?