Cayley-Hamilton

Stream: maths

[Aaron Anderson]

I think the "determinantal" proof of Cayley Hamilton, as presented in this pdf (https://people.reed.edu/~jerry/332/28ch.pdf) would be pretty amenable to Lean, except for the fact that polynomials cannot be evaluated (with the standard tools at least) into non-commutative values. I understand why this could make life easier for multivariate polynomials, but adjoining just one element to a commutative ring, say, gives another commutative ring. Can anyone recommend any fixes?

[Scott Morrison]

It doesn't seem that polynomial.eval₂ assumes the target ring is commutative.

[Aaron Anderson]

Thanks! Unfortunately polynomial.eval₂_ring_hom does assume the target ring is commutative, which might still set me back a little.

[Scott Morrison]

You do need to know that your map f : R \to S lands in the centre of S.

[Scott Morrison]

i.e. you could eval into any R-algebra, more generally than along a ring_hom to a commutative ring.

[Scott Morrison]

This should be fixed!

[Scott Morrison]

It would be a pretty major overhaul of polynomial.lean, however.

[Scott Morrison]

I know @Yury G. Kudryashov has been planning various refactors there, but I'm not sure where he's up to.

[Aaron Anderson]

Well, now that I'm deconfused about polynomial.eval₂, I should be able to prove that the image of my polynomial evaluation is a commutative subring of matrices, which should be enough to use determinants.

[Yury G. Kudryashov]

Sorry, I'll return to the polynomials refactor tomorrow.

[Yury G. Kudryashov]

After my refactor aeval will work for matrices.

[Yury G. Kudryashov]

(or any other algebra)

[Yury G. Kudryashov]

Currently it assumes that the target ring is commutative.

[Yury G. Kudryashov]

[1/n]: #3003

[Johan Commelin]

@Yury G. Kudryashov Thank you so much for doing this!

[Aaron Anderson]

I have written what I'm pretty sure is most of a proof of Cayley-Hamilton.

[Aaron Anderson]

It's in this repository, with another project. https://github.com/jalex-stark/friendship-theorem/tree/master/src

[Aaron Anderson]

The only sorrys left have to do with polynomial.eval2, and should be fixed by either hard work, better understanding of how to infer instances, or waiting for the refactor to make polynomials evaluation less commutativity-dependent.

[Yury G. Kudryashov]

I'm sorry for slowing you down. I have a several refactors on the queue. I'll try to switch back to polynomials in about an hour. UPD: unless I'll go to bed earlier.

[Scott Morrison]

What is going on with

def choose_index : n := arbitrary n

def vec_to_one_row (vec : n → R): matrix n n R :=
λ (i : n), ite (i = choose_index) vec 0

This stuff seems weird.

[Aaron Anderson]

I wanted to apply a matrix of matrices to a vector of vectors, but matrix.mul_vec and such seem to require that the entries of the matrix and vector belong to the same ring

[Aaron Anderson]

So I came up with a way to replace the vector of vectors with a matrix of matrices

[Aaron Anderson]

Kind of weird, I agree, but easier in the short-term than developing the “right” generalization of matrix multiplication to ring actions or something

[Scott Morrison]

I think it's going to require a bit of restructuring before others could use this proof.

[Scott Morrison]

@Yury G. Kudryashov, I just experimented a bit with generalising parts of polynomial.lean to semiring, rather than comm_semiring.

[Scott Morrison]

How much would it get in the way of your refactoring plans if I PR'd that?

[Scott Morrison]

I can try again later if it's going to be annoying.

[Yury G. Kudryashov]

What parts?

[Scott Morrison]

https://github.com/leanprover-community/mathlib/pull/3043

[Scott Morrison]

So everything before eval2 first appears, except that everything about C still assumes a comm_semiring.

[Mario Carneiro]

Hm, that's an interesting point @Aaron Anderson . Matrices are supposed to be the finite based version of linear maps between vector spaces, so there should be a way to turn a matrix into a linear map

[Yury G. Kudryashov]

My next refactor will deal with eval₂, eval, and aeval.

[Scott Morrison]

So what I was just doing is perhaps orthogonal?

[Yury G. Kudryashov]

Yes.

[Scott Morrison]

(It wasn't intended as a real PR; just the quickest way to show you now.)

[Scott Morrison]

Ok. I will not do anything that touches eval*!

[Mario Carneiro]

Given a basis on V and a vector in V, you can produce a list of coefficients in R, which you can use mul_vec on to get another list of coefficients in R. Given a basis on W you can evaluate the list to get a vector in W

[Mario Carneiro]

So it seems like nothing new is needed in matrices, mul_vec is sufficient. It just needs to be coupled with constructions for converting from R^n to and from a vector space

[Aaron Anderson]

I’ll try to clean it up soon. Ultimately these vectors of vectors and matrices of matrices really come from tensor products, so maybe the best way to express this proof is by fleshing out the theory of tensors-as-matrices a bit

[Scott Morrison]

Another fun thing to prove might be

matrix n n (polynomial R) ≃+* polynomial (matrix n n R)

(this requires #3043 before it even makes sense)

[Scott Morrison]

if you have that, there is what looks like a lovely proof of Cayley-Hamilton at http://drorbn.net/AcademicPensieve/2015-12/CayleyHamilton.pdf

[Kenny Lau]

there must be a way to generalize this statement

[Johan Commelin]

Its an R-alghom

[Kenny Lau]

this is saying that two functors commute

[Kenny Lau]

looks like a homomorphism condition to me

[Kevin Buzzard]

They only commute up to natural isomorphism

[Scott Morrison]

what is the universal property for matrix n n? Can we prove this (natural) isomorphism by comparing the universal properties of the LHS and RHS?

[Jalex Stark]

universal property in the category of R-algebras? I want to say something like "it admits an embedding of every n-dimensional R-algebra" but that's not quite it

[Scott Morrison]

like polynomial R is the initial object in the category of "rings S equipped with a map from R and a chosen element"

[Scott Morrison]

what is matrix n n R?

[Kevin Buzzard]

End_R(R^n)

[Kevin Buzzard]

up to natural isomorphism

[Scott Morrison]

but just saying that doesn't give you matrix n n (polynomial R) ≃+* polynomial (matrix n n R) for free

[Scott Morrison]

https://mathoverflow.net/a/142445

[Scott Morrison]

doesn't actually seem very useful

[Johan Commelin]

Yeah... it's a universal coproperty :rofl:

[Jalex Stark]

does anyone have a math proof of this isomorphism? it's not clear to me
edit: ah, the isomorphism concretely is "collect like powers of the indeterminate"

[Patrick Massot]

It's a bit sad to struggle with Cayley-Hamilton for matrices when this theorem has not much to do with matrices, and we'll need to do multilinear algebra properly at some point. But I guess it still progress to work towards having it anyway (and I certainly don't have time for multilinear algebra).

[Scott Morrison]

The proof, at least as a ≃+ is just a bunch of currying, swapping, uncurrying, and using src#finsupp.equiv_fun_on_fintype

[David Wärn]

polynomial and matrix n n are both 'semigroup algebras', over the monoid of natural numbers and the semigroup fin n x fin n, viewed as indexing the standard basis of matrix n n, respectively

[David Wärn]

I guess the latter is not quite a semigroup actually...

[Kevin Buzzard]

$\begin{pmatrix} a_0+a_1X+a_2X^2+\cdots&b_0+b_1X+b_2X^2+\cdots\\ c_0+c_1X+c_2X^2+\cdots&d_0+d_1X+d_2X^2+\cdots \end{pmatrix}$

"equals"

$\begin{pmatrix}a_0&b_0\\c_0&d_0\end{pmatrix}+\begin{pmatrix}a_1&b_1\\c_1&d_1\end{pmatrix}X+\begin{pmatrix}a_2&b_2\\c_2&d_2\end{pmatrix}X^2+\cdots$

[Kevin Buzzard]

A mathematican can say they're equal because they're equal in some fluid over-set

[Kevin Buzzard]

Might well work for multivariate polynomials too. Might have to be careful with infinite matrices

[David Wärn]

Maybe the correct thing to say is that polynomial A for an R-algebra A is $A \otimes \mathbb Z[X]$, and matrix n n A is $A \otimes M_n(\mathbb Z)$? Then it's associativity and commutativity of tensor product?

[Kevin Buzzard]

R=$\mathbb{Z}$

[Kevin Buzzard]

and this proof generalises to mv_polynomial

[David Wärn]

Are you saying we may assume R is $\mathbb Z$ or that this only makes sense for $\mathbb Z$?

[Kevin Buzzard]

I was just remarking that you said R-algebra but R is mentioned precisely once in your comment; you either tensor with R[X] or change R to Z and you're fine

[David Wärn]

Right, I think I meant "is" as in "isomorphic as R-algebras", but that also works

[Kevin Buzzard]

I was just remarking that you said R-algebra but R is mentioned precisely once in your comment; you either tensor with R[X] or change R to Z and you're fine

[Scott Morrison]

We don't have tensor products of R-algebras yet?

[Johan Commelin]

nope, we don't afaik

[Scott Morrison]

#3050

[Scott Morrison]

I have a very sorryful proof of Cayley-Hamilton, following the argument at http://drorbn.net/AcademicPensieve/2015-12/CayleyHamilton.pdf.

[Scott Morrison]

It is still a mess and needs some refactoring.

[Scott Morrison]

It also needs some sorrys filled in. I am confident all the remaining ones are "easy" (no design or API changes need, just bashing around with polynomials and/or matrices).

[Scott Morrison]

If anyone wants to jump in and hack on it, go for it: git checkout origin/cayley_hamilton

[Scott Morrison]

I will start cleaning up the structure later

[Patrick Massot]

Scott Morrison said:

If anyone wants to jump in and hack on it, go for it: git checkout origin/cayley_hamilton

Scott means leanproject get mathlib:cayley_hamiltonso that you get oleans too.

[Johan Commelin]

Unfortunately Azure isn't done yet

[Johan Commelin]

@Scott Morrison I'm seeing def baz, shouldn't that be def bar or def dror? :stuck_out_tongue_wink: [/jk]

[Johan Commelin]

Also, I would prefere M or A for matrices, over m.

[Scott Morrison]

All the names are up for grabs. :-)

[Scott Morrison]

Mostly the proof is/will be only the usual de Bruijn factor relative to the informal proof, but the statement "polynomials of matrices are matrices of polynomials" takes a ridiculously long time to set up properly (because we need both a good characterisation of the function, and that's it's an algebra equivalence). Having finished with the route I took (discussed earlier in this thread), I'm not sure it was the easiest one. :-)

[Johan Commelin]

But the resulting proof is quite nice. And the statement baz is very useful anyways. So we will profit in the future, I'm quite sure.

[Patrick Massot]

Johan Commelin said:

Unfortunately Azure isn't done yet

It's done now (unless someone pushed a new commit in the mean time).

[Johan Commelin]

I just did (-;

[Johan Commelin]

I pushed a proof of q

[Johan Commelin]

@Scott Morrison how did I let you get away with defining scalar in mathlib, but not scalar_apply?

[Johan Commelin]

@Jalex Stark I pushed another bit (just a heads up)

[Jalex Stark]

thanks; i merged and pushed another bit

[Johan Commelin]

@Jalex Stark Did you know about git pull --rebase?
Not very important, but it avoids the merges (unless there are conflicts) by replaying your work on top of whatever you pull.

[Jalex Stark]

(in this case there were conflicts; two lemmas that we both proved, yours seemed better so I accepted them)

[Jalex Stark]

i'm not sure i understand what you mean by avoiding merging. if there aren't conflicts, git pull will handle the merge by itself?

[Patrick Massot]

This is orthogonal.

[Patrick Massot]

git pull --rebase will also handle conflicts, with your help if needed.

[Johan Commelin]

Yes, I didn't phrase it correctly

[Johan Commelin]

It will replay automatically (unless there are conflicts) is what I should have written.

[Johan Commelin]

git pull will merge, but you can "rewrite history" by taking your local changes, storing them in the file cabinat (so to speak), doing a git pull and then taking your local changes and replaying them on top of whatever was pulled.

[Johan Commelin]

As I said, it's not very important.

[Johan Commelin]

Because once it is merged into mathlib the entire git history is squashed into 1 commit anyways

[Jalex Stark]

ah i see, git pull rebase will pretend that I pulled before making my changes

[Jalex Stark]

it kind of performs a reidemeister move on the commit tree

[Johan Commelin]

Once your git history is a non-trivial knot... didn't you do something wrong?? :grinning_face_with_smiling_eyes:

[Jalex Stark]

working with double sums feels too hard

[Johan Commelin]

I pushed a proof of sum_over_range'

[Scott Morrison]

thanks for all the work while I was eating dinner :-)

[Johan Commelin]

I pushed some more stuff

[Scott Morrison]

Turns out coeff_mul_zero has a rather shorter proof. :-)

[Jalex Stark]

simp [coeff_mul]?

[Johan Commelin]

After a digression involving simp and lunch, I'm back (-;

[Jalex Stark]

do we already have an induction principle like this?

import tactic

noncomputable theory
open_locale big_operators
open_locale classical


lemma sum_add_induction {α M : Type} [add_comm_monoid M] {p : M → Prop}
  (f : α → M) (s : finset α) (p_add : ∀ a b, p a → p b → p (a + b)) (p_zero : p 0) (p_s : ∀ x ∈ s, p $ f x) :
p $ ∑ x in s, f x :=
begin
  induction s using finset.induction with x hx s hs, simpa,
  rw finset.sum_insert, swap, assumption,
  apply p_add, apply p_s, simp,
  apply hs, intros a ha, apply p_s, simp [ha],
end

[Johan Commelin]

I don't recognise it

[Johan Commelin]

Should we have a definition for matrices like
(λ i' j', if i' = i ∧ j' = j then x else 0)?

[Jalex Stark]

in maths this is sometimes called an "elementary matrix"?

[Jalex Stark]

i think we could use some simp lemmas for these in the current work

[Scott Morrison]

Yes.

[Johan Commelin]

Wiki says that elementary matrices are those that differ from the identity matrix by a single row/col operation

[Jalex Stark]

in quantum computing we just call them \ketbra i j

[Jalex Stark]

is that notion from wikipedia a useful one?

[Johan Commelin]

Maybe we should just have \delta

[Johan Commelin]

I think it's fine to just claim the name elementary_matrix for this concept. we can cook up a new name for the wiki thing, if we need it.

[Jalex Stark]

should this go in data.matrix.basic?

[Johan Commelin]

I think so

[Johan Commelin]

Of course it needs 25 compatibility lemmas with 1 and 0, and diagonal and scalar, etc...

[Scott Morrison]

Working with coefficients and degrees of polynomials is so painful!

[Johan Commelin]

And trace elementary and det (elementary i j) etc

[Johan Commelin]

@Scott Morrison On which sorrys are you currently working?

[Scott Morrison]

I pushed a few, but I think I'm going to stop for a while

[Scott Morrison]

So they're all yours :-)

[Scott Morrison]

we're pretty close

[Jalex Stark]

I have this so far, I think I should put it in a separate PR?

variables {α β : Type*} [semiring α] [semiring β]
variables {m n : Type u} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n]

@[reducible]
def elementary_matrix (i : n) (j : m) : matrix n m α :=
(λ i' j', if i' = i ∧ j' = j then 1 else 0)

lemma matrix_eq_sum_elementary (x : matrix n m α) :
x = ∑ (i : n) (j : m), (x i j) • elementary_matrix i j :=
begin
  ext,
    rw finset.sum_apply,
    rw finset.sum_apply,
    rw ← finset.sum_subset, swap 4, exact {i},
    { norm_num, },
    { simp },
    intros, norm_num at a, norm_num,
    convert finset.sum_const_zero,
    ext, norm_num, rw if_neg, tauto
end

[Scott Morrison]

I'd advise against using @[reducible] unless you have a good reason.

[Scott Morrison]

appropriate @[simp] lemmas are nearly always better

[Scott Morrison]

My suggestion would be to put it into the cayley_hamilton branch, and check that it is usable there

[Scott Morrison]

That branch is going to turn into many PRs, not just one.

[Scott Morrison]

so we can slice this off again once we see it's working

[Johan Commelin]

@Scott Morrison I think that algebras like algebra R (polynomial A) are currently not really "supported" by mathlib...

[Scott Morrison]

What do you mean?

[Johan Commelin]

Well, it's part of a diagram...

[Johan Commelin]

R → A → polynomial A, and this thing is (provably) the composition. (Maybe even definitionally.)

[Johan Commelin]

But we'll need a bunch of lemmas for that.

[Jalex Stark]

but those lemmas are the lemmas about tensor products, no?

[Johan Commelin]

Of course we can add the lemmas in the special cases. But I'm still trying to figure out if we can get a general machine to make this as easy as it should be.

[Scott Morrison]

I guess I'm not sure still what you're concerned about

[Scott Morrison]

I mean, it's just some R-algebra, that we happen to have built out of a different R-algebra.

[Johan Commelin]

Ooh, wait.. this is for noncommutative A, so we don't even have algebra A (polynomial A).
Let me shut up.

[Johan Commelin]

In fact, this works:

lemma turkle_map_apply (r : R) :
  algebra_map R (polynomial A) r = C (algebra_map R A r) :=
rfl

[Scott Morrison]

(I really should rename all my metasyntactic variables before making branches public...)

[Scott Morrison]

I've no idea where I picked up turkle from. It seems to be entirely unattested amongst lists of metasyntactic variables I can find. Nevertheless my chickens are called foobar, quux, and turkle.

[Scott Morrison]

(On even-numbered days they are all called bruce.)

[Johan Commelin]

I have fixed another sorry

[Johan Commelin]

Scott Morrison said:

(I really should rename all my metasyntactic variables before making branches public...)

What we really need is a linter that automatically flags if a name is wrong, and suggests to replace it with a proper one...
I fear that we need AGI before that happens.

[Rob Lewis]

What we really need is a linter that automatically flags if a name is wrong, and suggests to replace it with a proper one...

https://arxiv.org/abs/2004.07761

[Scott Morrison]

I wonder if we should change the definition of to_fun in polynomial_algebra.lean, to use eval2.

[Scott Morrison]

At the time I first wrote it, eval2 didn't work in this generality. I think it should now, and perhaps there's better API support?

[Scott Morrison]

Not sure.

[Johan Commelin]

@Scott Morrison Not sure if it matters...

[Johan Commelin]

We probably need equation lemmas either way

[Johan Commelin]

I've pushed another couple sorry-fixes

[Kevin Buzzard]

Hey it's really important that the constructor for the elementary matrix takes the value of the nonzero matrix entry as an input. That way you can reduce a lot of problems about R-linearity to questions about the underlying abelian group. This was an important trick I learnt when working with @Shing Tak Lam on derivations

[Scott Morrison]

(This is the same argument that we should talk much more about monomial n a in polynomial.lean, and less about C a * X^n.)

[Scott Morrison]

@Jalex Stark, I'll leave it to you to make this change?

[Scott Morrison]

@Jalex Stark, one of your commits has the line rw ← sum_product',, but there's no declaration with that name that I can find.

[Scott Morrison]

Did you forget to add a file?

[Jalex Stark]

oops sorry, I just got online and have a few things to address but should get to it soon. That's supposed to be a new decl in big_operators. (which i probably need to rewrite because i did a lot of stashing and switching between branches in one local copy of mathlib yesterday)

[Jalex Stark]

oh, it is in fact there in the current branch. the decl is made by to_additive on prod_product' in big_operators (okay, I changed sum_product' to finset.sum_product' and it works now)

[Jalex Stark]

i'm working on changing elementary_matrix now

[Scott Morrison]

I think things are going to be a lot easier if I refactor eval2 so it takes a bundled ring_hom rather than needing a is_semiring_hom typeclass

[Scott Morrison]

however I'm not super confident that will go well... not sure how many other places will need changes

[Scott Morrison]

I may experiment with it on a different branch for a bit

[Jalex Stark]

I think at some point I wrote an instance is_semiring_hom f for f being the to_fun of a bundled algebra_hom, and this felt dirty

[Scott Morrison]

yes, it's past time we killed is_semiring_hom.

[Scott Morrison]

@Jalex Stark, your work on elementary_matrix has broken the proof of matrix_polynomial_equiv_polynomial_matrix_coeff_apply.

[Scott Morrison]

Do you know what's going on, or should I start on that?

[Scott Morrison]

(Otherwise, we're down to a single sorry on cayley_hamilton, which looks like easy algebra.)

[Jalex Stark]

yeah, I don't know why i pushed before i reached an error-free state, I am still working locally to propagate elementary_matrix throughout

[Jalex Stark]

it does seem to be simplifying stuff

[Scott Morrison]

okay! I will leave that bit of the file then, and try and do my algebra homework

[Jalex Stark]

I have something like

M x.fst x.snd * ⇑(algebra_map R A) (elementary_matrix x.fst x.snd 1 i j))

but want something like

M x.fst x.snd • (elementary_matrix x.fst x.snd 1) $ i j

I think I am missing something simple

[Johan Commelin]

algebra.smul_def?

[Jalex Stark]

thanks!

[Scott Morrison]

Ok, cayley_hamilton now builds except for this thing with elementary_matrix!

[Scott Morrison]

there is a _lot_ of cleanup still to do

[Jalex Stark]

for the elementary_matrix stuff i just have two more proofs to fix in polynomial_algebra

[Scott Morrison]

awesome! and I found a quick work-around so

[Scott Morrison]

We have cayley_hamilton! (No sorries.)

[Jalex Stark]

maybe your work-around is best for what's remaining, the "right" way would be to show that elementary_matrix i j is an add_monoid_hom

[Scott Morrison]

oh ...

[Scott Morrison]

except, @Jalex Stark, I didn't notice you adding the [inhabited n] instances, which I don't think we want

[Jalex Stark]

hm.

[Scott Morrison]

and which changes the statement of Cayley-Hamilton subtly...

[Scott Morrison]

we have to prove it for empty matrices, too :-)

[Scott Morrison]

actually... err... is it even true?

[Jalex Stark]

matrix unit unit is unit. So is the empty matrix 0 or 1?

[Scott Morrison]

what is the characteristic polynomial of the empty matrix? surely 1?

[Scott Morrison]

if you want it to be the product of the eigenvalues, it is 1

[Jalex Stark]

the characteristic matrix is the empty matrix

[Scott Morrison]

but the "usual formula" gives zero

[Scott Morrison]

huh :-)

[Jalex Stark]

right, and this is fine because the empty matrix brings the zero ring into the picture

[Jalex Stark]

so we're complaining that we can't factor the identity map on our ring through the zero ring

[Scott Morrison]

phew:

#eval matrix.det (λ (x y : punit), (0 : ℤ))

says 0 :-)

[Scott Morrison]

Lean has spoken.

[Scott Morrison]

So indeed, we need to get rid of that inhabited hypothesis.

[Scott Morrison]

sadly matrix.induction_on needs a h_zero argument, just to cover this case

[Scott Morrison]

maybe I'll split it into two versions, one with an inhabited argument using your trick

[Scott Morrison]

but we won't use that one here

[Scott Morrison]

Okay, cayley_hamilton works again, this time including the trivial case

[Jalex Stark]

maybe I'm just too tired to be doing this right now, but I want to rewrite

⇑matrix_polynomial_equiv_polynomial_matrix (elementary_matrix i j p + elementary_matrix i j q)
= ⇑matrix_polynomial_equiv_polynomial_matrix (elementary_matrix i j p) + ⇑matrix_polynomial_equiv_polynomial_matrix (elementary_matrix i j q)

I tried rw ring_hom.map_add and that didn't work (and then lean crashed and I'm waiting to rebuild mathlib, since i don't have oleans yet)

[Scott Morrison]

try alg_hom.map_add

[Jalex Stark]

:thumbs_up: I will try that in a few minutes

[Mario Carneiro]

Jalex Stark said:

matrix unit unit is unit. So is the empty matrix 0 or 1?

Isn't it both?

[Jalex Stark]

yes, the question was what should happen to it when we bring it into polynomial land

[Jalex Stark]

so by "is" i didn't mean = I meant equal after applying some map out of matrix unit unit

[Jalex Stark]

if the map wanted to be a ring hom then it would have to land at 0, but thankfully that's not the case and scott figured out that it wants to land at 1
(edit: I guess I misunderstood something along the way)

[Scott Morrison]

@Mario Carneiro the question was really what the determinant of the empty matrix is

[Scott Morrison]

and it is indeed meant to be zero, which is good for Cayley-Hamilton, and bad for "determinant is the product of the eigenvalues"

[Jalex Stark]

Scott Morrison said:

try alg_hom.map_add

didn't work. I'll try haveing the statement i want intstead of rwing to it

[Jalex Stark]

ah i'm spewing nonsense

[Mario Carneiro]

I think the determinant of the empty matrix should not be defined

[Mario Carneiro]

which means that it should be 0 in lean

[Kenny Lau]

the determinant of the empty matrix is 1

[Kenny Lau]

S_0 has exactly one element, and the empty product is 1

[Mario Carneiro]

Ah, I messed up the math on one of the definitions. https://math.stackexchange.com/questions/2130175/does-the-unique-map-on-the-zero-space-have-determinant-1 gives a number of independent reasons for the determinant to be defined and equal to 1

[Mario Carneiro]

Oh I misread Scott's #eval too, he measured the determinant of the 1x1 zero matrix

[Scott Morrison]

oops!

[Scott Morrison]

#3214 #3215 #3216 and #3217 are all mini-PRs coming out of cayley_hamilton.

[Scott Morrison]

The rest may have to wait until #3193 and #3213 have merged.

[Scott Morrison]

Although @Jalex Stark, do you want to make the elementary_matrix stuff a separate PR? It could get started now.

[Scott Morrison]

I think you want @[simp] on scalar_apply_eq and scalar_apply_ne, and corresponding @[simp] lemmas for elementary_matrix.

[Reid Barton]

I haven't read this carefully, but I just want to say (a) the determinant of the empy matrix is 1, (b) elementary matrix doesn't mean a matrix with a single nonzero entry.

[Scott Morrison]

Yes! (a) was eventually agreed, after I caused some confusion.

[Scott Morrison]

I also agree with (b), and I think we haven't renamed yet for lack of the right name.

[Scott Morrison]

What should these matrices be called?

[Scott Morrison]

maybe just basis_matrix?

[Reid Barton]

I was going to suggest something like std_basis_matrix, yeah

[Reid Barton]

partly in reference to the confusingly named std_basis (does it still exist)?

[Kevin Buzzard]

#eval matrix.det (λ (x y : punit), (0 : ℤ))

Wait, that's the det of the 1x1 matrix (0). I think CH is false for the 0 by 0 matrix

[Kevin Buzzard]

Sorry, late to the party. So we are agreed that CH fails for 0x0 matrices?

[Jalex Stark]

any polynomial of the empty matrix is the empty matrix is zero, so CH is true for 0x0 matrices

[Jalex Stark]

i like std_basis_matrix

[Johan Commelin]

@Scott Morrison I'm happy with the polynomial refactor. I left one tiny comment. If you agree, I'll hit it with the merge hammer.

[Scott Morrison]

I generalised that lemma, and put the PR on the queue.

[Johan Commelin]

Great!

[Scott Morrison]

It occurs to me that we are still missing map_smul there. I tried proving that, but it will be easier post #3213.

[Scott Morrison]

@Jalex Stark, I'm just slicing things up into PRs now. Do you want to do the honours on https://github.com/leanprover-community/mathlib/pull/new/std_basis_matrix

[Jalex Stark]

Go ahead without me, sorry. Working on mathlib PRs is quite addictive and I need to leave space in my head for my day job right now