Why does mathlib have matrices?

Stream: mathlib4

[Violeta Hernández]

This is probably off-topic but I'm quite surprised we even have matrices in Mathlib. I'm of the personal opinion that a basis-free approach to linear algebra ends up being more elegant and often simpler.

[Aaron Liu]

some things are basic invariant but still really hard to define without matrices

[Violeta Hernández]

Aaron Liu said:

some things are basic invariant but still really hard to define without matrices

Examples?

[Aaron Liu]

like I guess the determinant or the trace

[Aaron Liu]

maybe "really hard" was an exaggeration

[Yury G. Kudryashov]

Here are at least 3 reasons to have matrices.

• Sometimes, it is easier to define something for matrices and prove that it doesn't depend on a choice of coordinates.
• For some theorems, the basis is important. We can try to formulate them for a pair of (linear operator, basis), but this is worse than talking about matrices.
• We want to support undergrad curriculum.

[Violeta Hernández]

Aaron Liu said:

like I guess the determinant or the trace

Determinant is the scale factor of the n-th exterior power, trace is the contraction map on tensors

[Violeta Hernández]

Fair enough, it's not like matrices are categorically unuseful in math. Though I'd argue we could be quite more liberal with their use if we so wanted.

[Kevin Buzzard]

Aaron Liu said:

maybe "really hard" was an exaggeration

I'm not so sure it's an exaggeration. I don't know of any way of defining the trace of a linear map from a finite-dimensional vector space to itself without picking a basis and taking the trace of the corresponding matrix (my confused thoughts about it in 2021 are here).

I have just spent the week picking bases for vector spaces for FLT and using matrices, because sometimes the way to prove things about constructions for finite-dimensional vector spaces is to prove things about matrices first. Example: I don't know of any proof that a linear isomorphism from a finite-dimensional real vector space to itself scales Lebesgue measure by its determinant which doesn't involve picking a basis and then doing a pretty gruelling calculation with matrices, as we do here in docs#Real.map_matrix_volume_pi_eq_smul_volume_pi in mathlib . If I knew a conceptual proof of this then I'd be able to answer my own recent mathoverflow question.

All this is off-topic for this thread (edit: not any more because I moved it to a more appropriate thread) but there is definitely a point to matrices. They are a model for linear maps and sometimes to prove theorems or make definitions, you need a model; conceptually I am not sure why but in practice this seems to be definitely true.

[Yoh Tanimoto]

How much is it allowed to use the existence of a basis? If it is allowed to use the dimensions of subspaces, how about defining trace as the sum of generalized eigenvalues times multilicity?

[Sébastien Gouëzel]

Kevin Buzzard said:

Aaron Liu said:

maybe "really hard" was an exaggeration

I'm not so sure it's an exaggeration. I don't know of any way of defining the trace of a linear map from a finite-dimensional vector space to itself without picking a basis and taking the trace of the corresponding matrix (my confused thoughts about it in 2021 are here).

Endomorphisms of $E$ are isomorphic to $E \otimes E^*$ (where $v \otimes \xi$ is the rank-one map mapping $x$ to $\xi(x) v$). There is a canonical linear mapping from $E \otimes E^*$ to the scalar field, sending $v \otimes \xi$ to $\xi(v)$ (obviously well defined by the universal property of the tensor product). Let's call it the trace. To me, it doesn't depend on a basis (and it also shows why the trace of finite-rank endomorphisms is also well defined in infinite dimension).

[Sébastien Gouëzel]

(I see that you mention in your post that you still need to pick a basis to show that the map from $E \otimes E^*$ is onto, but I'm not sure I agree with that: the image are the finite rank maps, and in finite dimension all maps are automatically finite rank, right? Of course at some point you need to use that the dimension is finite, but I'd say what is relevant is not that you have a basis, only a finite generating family)

[Timothy Chow]

I don't want to get too far off topic, but I'll just say that I have a hard time imagining formalizing most of numerical linear algebra without matrices.

[Shreyas Srinivas]

And spectral graph theory

[Shreyas Srinivas]

Of which we have a bunch of basic definitions in mathlib

[Violeta Hernández]

Kevin Buzzard said:

Aaron Liu said:

maybe "really hard" was an exaggeration

Example: I don't know of any proof that a linear isomorphism from a finite-dimensional real vector space to itself scales Lebesgue measure by its determinant which doesn't involve picking a basis and then doing a pretty gruelling calculation with matrices, as we do here in docs#Real.map_matrix_volume_pi_eq_smul_volume_pi in mathlib .

Lebesgue measure on R^n is the unique locally finite translation invariant Borel measure up to a scaling factor. In particular, for linear map T : R^n -> R^n, one has λ(T(E)) = f(T) λ(E) for every Borel E, for some constant f(T) ≥ 0. Clearly f is multiplicative.

Choose an inner product on R^n. Since orthogonal maps preserve the unit sphere, they must have f(T) = 1. For maps with an orthogonal basis of eigenvectors, one has f(T) = |product of eigenvalues|. Finally, SVD tells you that these two properties uniquely define f(T) = |det(T)|.

You certainly do have to define a basis for this argument, but you don't need to use the specific language of matrices.

[Kevin Buzzard]

But I claim that you do, because you need to prove that all linear maps can be expressed as a product of linear maps for which you understand the scaling factor, and that is proved using matrices.

[Violeta Hernández]

Fair enough. I guess the Lebesgue measure is not a priori an entity in linear algebra since you only know how it works on rectangles with a very specific orientation. So it makes sense matrices with their builtin bases end up a useful tool for working with it.

[Kevin Buzzard]

Lebesgue measure is much more algebraic than that because it's Haar measure (at least on Borel subsets, which are enough), so all you need is the topology -- you don't need a basis for this.

[Rida Hamadani]

In Seymour's project, we use explicit matrices representations extensively in the proof, even though the result itself is not about matrices. I think the whole work could have been done without matrices but it is not clear to me that it would have resulted in a better proof, representing regular matroids as totally unimodular matrices helps when taking their sums.

[Rida Hamadani]

But also the study of matrices itself is an area that needs a venue to be formalized in, complexity of matrix multiplication, existence of hadamard matrices, and so on: How would we go about formalizing new results in these areas if we don't have a functioning language of matrices in mathlib?

[Kevin Buzzard]

Sébastien Gouëzel said:

(I see that you mention in your post that you still need to pick a basis to show that the map from $E \otimes E^*$ is onto, but I'm not sure I agree with that: the image are the finite rank maps, and in finite dimension all maps are automatically finite rank, right? Of course at some point you need to use that the dimension is finite, but I'd say what is relevant is not that you have a basis, only a finite generating family)

So it seems to me that:

1) You can define what it means for a vector space to be finite-dimensional without choosing a basis (just say it's finitely-generated)

2) If E is finite-dimensional then the map $E\otimes E^*\to End(E)$ is a computable function, but the proof that it's a bijection is a dimension-count and it might be hard to do this without picking a basis;

3) the inverse of this computable function is probably non-computable in general, so

4) if you attempt to define trace this way without picking a basis then (a) it will be noncomputable and (b) you'll still have to convince me that you can prove that the map $E\otimes E^*\to End(E)$ is a bijection without picking a basis. Note that I won't give you the dimension of the space; I'll only tell you that it's finitely-generated as a module.

Maybe it's possible to prove that it's a bijection without picking a basis though, or maybe you don't care because you will allow yourself to pick a basis in a proof.

So perhaps a summary is that trace of a linear map is noncomputable unless you pick a basis?

[Stepan Nesterov]

Kevin Buzzard said:

2) If E is finite-dimensional then the map $E\otimes E^*\to End(E)$ is a computable function, but the proof that it's a bijection is a dimension-count and it might be hard to do this without picking a basis (I agree surjectivity is fine though);

Isn't this function injective without assuming finite-dimensionality?

[Timothy Chow]

Kevin Buzzard said:

So perhaps a summary is that trace of a linear map is noncomputable unless you pick a basis?

I wonder if some of these observations can be made formal. Perhaps a starting point would be the paper Hilbert spaces without the Countable Axiom of Choice, which explores what can be said about Hilbert spaces without the axiom of choice. Without choice, a Hilbert space may lack a basis, which gives a precise meaning to "not picking a basis." Also in the absence of choice, some of the funny things that can happen with Dedekind-finiteness may give some insight into what can and cannot be proved in the finite-dimensional case.

[Martin Dvořák]

Rida Hamadani said:

In Seymour's project, we use explicit matrices representations extensively in the proof, even though the result itself is not about matrices. I think the whole work could have been done without matrices but it is not clear to me that it would have resulted in a better proof, representing regular matroids as totally unimodular matrices helps when taking their sums.

Actually, is does the concept of total unimodularity exist on linear maps beyond matrices?

[Martin Dvořák]

Violeta Hernández said:

Determinant is the scale factor of the n-th exterior power, trace is the contraction map on tensors

Sounds like some very fancy math. Unfortunately, I don't have any idea what it means.

Without understanding the topic (maybe I am entirely wrong, please, let me know), it seems to me that you are mentioning two theorems. Maybe you can state them in Lean and add them with proof_wanted to Mathlib? Or perhaps also prove them yourself?

I think the goal should be connecting the concepts of determinant and trace of matrices to those more abstract concepts rather than removing them because they can be expressed in terms of those more abstract concepts. Again, I am commenting on something that I don't understand, so I might be completely wrong.

[Violeta Hernández]

Do we have exterior powers (or the exterior algebra to begin with) in Mathlib?

[Eric Wieser]

docs#ExteriorAlgebra

[Eric Wieser]

ExteriorPower is I believe in some open PRs (as a subtype)

[Violeta Hernández]

I'm specifically talking about the exterior power of a linear map

[Violeta Hernández]

If T : V → V with dim(V) = n then ∧ⁿ(T) = det(T)

[Trebor Huang]

How far could we get by defining "finite dimensional" as "dualizable" in the monoidal closed category sense? Then trace works but idk about determinants. The benefit is it kind of generalizes to modules and vector bundles.

[Violeta Hernández]

(For anyone just opening this thread, I'm now quite convinced that matrices do belong in Mathlib, even if my preferred approach to linear algebra is to avoid them)

[Boris Alexeev]

I guess a related question is: suppose all the desirable facts about trace, dimensionality, scaling of Lebesgue measure, etc were easily provable without matrices.

Would mathlib have matrices then?

[Violeta Hernández]

If that were the case I'd suggest moving them to Batteries. And over there we could do all the fun computational stuff like implementing Karatsuba or sparse matrices. But I suspect that would be an unpopular opinion.

[Stepan Nesterov]

I doubt that somebody would argue that the mathlib correct way to define https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/RootSystem/CartanMatrix.html#RootPairing.Base.cartanMatrixIn is as an endomorphism of the space of formal linear combinations on a set in bijection with a set of simple roots of a root system

[Thomas Browning]

Just for fun, here's something about linear maps in mathlib that really needs matrices, I think: f ∘ g = id ↔ g ∘ f = id for linear endomorphisms of a finite free module over a commutative semiring (this is docs#LinearMap.comp_eq_id_comm + docs#Matrix.instIsStablyFiniteRingOfCommSemiring).

[Thomas Browning]

(at least, the proof is 200 lines of horrid mucking around with explicit matrix entries)

[Aaron Liu]

That one works for any noetherian ring I think

[Aaron Liu]

not just the matrix ring

[Violeta Hernández]

Every Noetherian ring is Dedekind finite?

[Aaron Liu]

Maybe I'm remembering wrong?

[Aaron Liu]

oh for semirings the proof I know doesn't work

[Aaron Liu]

so idk about semirings

[Violeta Hernández]

Yeah, in the field case this result is nice since you can just use injective ↔ surjective on endomorphisms. If you tell me the semiring case can't be done any nicer than explicit matrix calculations I'll sadly concede that they're not at all unavoidable.

[Alex Meiburg]

I would add: there's a good chunk of important math in the literature regarding sparse matrices, tridiagonal matrices, and matrix norms that are not basis independent. These could be formalized using linear operators where everything is basis-dependent, but then really I think just using matrices is much more reasonable.

[Riccardo Brasca]

Matrices are very much needed for Lie algebras (or it would very difficult to avoid them).

[Timothy Chow]

Boris Alexeev said:

I guess a related question is: suppose all the desirable facts about trace, dimensionality, scaling of Lebesgue measure, etc were easily provable without matrices.

Would mathlib have matrices then?

I think it should. Rida Hamadani put it well: matrices are not just "what you get from a linear transformation when you pick a basis." They are objects of study in their own right. It seems that mathlib currently has a bias toward (for lack of a better word) "abstract" rather than "numerical" mathematics, but if the goal of mathlib is to formalize "all of math" then numerical mathematics is also part of math.

Slightly off topic, but Nick Trefethen's Applied Mathematician's Apology is an excellent read.

[Etienne Marion]

I don’t think mathlib’s goal is to formalize all of the math.

[Timothy Chow]

Etienne Marion said:

I don’t think mathlib’s goal is to formalize all of the math.

What do you think the goal of mathlib is? This is a real question.

[Violeta Hernández]

I think Mathlib's goal is to formalize the most useful and well-known mathmatics. And whatever outliers remain can be placed in the other projects of the Lean ecosystem.

[Kevin Buzzard]

There was a recent paper published in the Annals of Mathematics about behaviour of eigenvalues of a matrix which had random entries of either +1 or -1 in each slot. Not sure you could do this with linear maps:-)

[David Loeffler]

I'm coming late to this thread here, but I can't help asking the counter-question: why do some people here regard it as desirable to actively avoid the use of matrices? I feel there's a little bit of mathematical virtue-signalling going on here: "real mathematicians don't use matrices", and anything that requires explicit matrix calculations is an "outlier" (a classic "no true Scotsman" fallacy).

I can understand the psychology behind this, since I went through the same phase myself. Like most mathematicians I initially learned linear algebra with explicit matrices and vectors (in school). When I encountered the basis-free, linear-transformations approach (in my first year at university) it initially seemed very strange and difficult to me, and I had to work quite hard to really master it. Once I'd fully learned this new approach, I naturally wanted to convince myself that the sacrifice I had made was worthwhile, by embracing the view that anything involving explicit matrices and vectors was clumsy, inelegant, intrinsically inferior.

But that phase didn't last: as I matured as a mathematician, I came to the conclusion that the explicit matrix-based approach and the abstract vector-space approach are both just tools, and you use whichever tool suits your problem better – you don't hear carpenters arguing over whether screwdrivers are better than hammers.

(I went through several such cycles in my mathematical training – another one involved category theory. There are also examples of the entire mathematical community collectively going through a similar cycle over a much longer time-scale, e.g. the see-saw between explicit vs. abstract methods in commutative algebra.)

[Jireh Loreaux]

My advisor basically spent his career working with matrices. Of special interest to him were commutators of compact operators (on a Hilbert space). In the 70's, Joel Anderson exhibited that a rank-one projection is a commutator of compact operators. I would be rather astounded if anyone could give a proof of that without matrices. The construction consists of a pair of block tri-diagonal matrices, and the sizes of the blocks grow arithmetically.

[Timothy Chow]

At the risk of beating a dead horse, let me list a few examples to underline the point that a matrix is not just "what you get from a linear transformation by picking a basis" but a concept without which it would be difficult to even state many fundamental results.

1. The theory of matrices with nonnegative (or positive) entries (the Perron–Frobenius theorem, Sinkhorn's theorem, total positivity, etc.) Entire books have been written on this subject.
2. Random matrix theory. In many applications, such as compressed sensing, the actual entries are important and it's not just "random linear transformation theory."
3. As already mentioned earlier in this thread, the computational complexity of matrix algorithms is an active area of research. Just one example: AlphaEvolve's recent discovery of an algorithm to multiply two 4x4 complex-valued matrices using only 48 multiplications, the first improvement since 1969.
4. A matrix can arise from a combinatorial object such as a graph or a polytope or a finite Markov chain. As someone else already said, it would be difficult to state, let alone prove, Kirchhoff's matrix-tree theorem and other results in spectral graph theory without matrices.
5. Pfaffians and permanents. These can be defined graph-theoretically but it would be extremely awkward to prove much about them if one were not allowed to use matrices.

It would be easy to extend this list. I'm fond of the non-messing-up theorem for rectangular arrays, though one could argue that this is not really a central topic in mathematics. Ditto for the Hadamard conjecture that was mentioned earlier.

[Ruben Van de Velde]

I wouldn't want to remove matrices from mathlib, but I did find it an interesting exercise upthread to see how far we could get without them

[Timothy Chow]

In general, I do think it is valuable to ask whether a theorem that makes no mention of X can be proved without X. (That's quite different from asking whether mathematics as a whole can do without X.) Regardless of whether the answer is yes, no, or somewhere in between, we often learn something valuable in the process. Examples:

• Can an elementary statement about prime numbers (e.g., the prime number theorem) always be proved by elementary means?
• Can Burnside's $p^aq^b$ theorem be proved without character theory?
• Can a theorem about Lie groups (or finite groups) be proved "directly" as opposed to by checking each case in the classification individually?
• Does a combinatorial theorem always admit a combinatorial proof? This one is particularly relevant to the matrix discussion because in many cases, one is seeking a proof (of a basis-independent result) that picks a basis! That is, one seeks to "explain" a result obtained via dimension counting by constructing a basis indexed by combinatorial objects that yield additional insight into the structure.

Sometimes, these kinds of questions can lead to new axioms (e.g., asking which theorems about linear independence can be formulated and proved without vector spaces could lead to the axioms for matroids) or reverse-mathematical insights (e.g., asking whether arithmetical theorems of ZFC can always be proved in ZF could lead to Shoenfield's absoluteness theorem). That's why I asked above if there might be a way to be more formal about what "picking a basis" really means.

But even if there's no way to completely formalize such a question, pursuing it can certainly be insightful. Of course, if one is trying to attack an unproven conjecture, it makes sense to use all tools available, since any proof is better than no proof. That doesn't mean that there aren't sometimes advantages to proofs that intentionally avoid X.

[Stepan Nesterov]

Is “can a theorem in mathlib be proved without importing a certain very large file” ever a formal question that maintainers ask for performance reasons?

[Damiano Testa]

Import sizes are certainly considered when evaluating PRs. The summary also has some statistics about the import changes of PRs.

[Violeta Hernández]

I've learned a lot from this thread. I think my personal preference against matrices hasn't really changed much, and I think matrix-free approaches can yield a lot of clarity into definitions like the trace or the determinant which are somewhat unmotivated otherwise. But now I see that this isn't the end of the story.

[Martin Dvořák]

Since I am the person whose 3 out of 4 Ph.D.-thesis projects are essentially about matrices, I cannot help but add one more remark.

I won't bother me if you consider me an inferior person for the reason that I work with matrices. It will bother me, however, if you make working with matrices in Lean harder (regardless of the motivation).

[Violeta Hernández]

I don't consider anyone here inferior for their tastes in mathematics.

[Timothy Chow]

On MathOverflow, I asked about the precise meaning of "picking a basis". It was not really a discussion about Lean, so I won't elaborate here, other than to highlight that Todd Trimble proposed a way to define the trace without picking a basis