Linear Algebra/Matrices: Elementary row operations, element

Stream: maths

[Alex Brodbelt]

Hi!

I checked the list of undergraduate mathematics missing in mathlib and these seems to not be in mathlib yet. I would like to start contributing to mathlib and was wondering how to start? :sweat_smile: (I'm not really sure where to ask)

Would implementing gaussian elimination or defining elementary matrices and proving that they are invertible be a good start? (I checked to the best of my ability to see if they are in mathlib and they aren't there ...I think)

[Patrick Massot]

There are some things in https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Transvection.html

[Alex Brodbelt]

Patrick Massot said:

There are some things in https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Transvection.html

For instance is defining a property like IsRowEchelonForm, IsDiagonal, IsTriangularizable, and so forth of interest? These aren't defined per se... but I imagine there mioght be a reason for this(?)

I've seen that there are theorems similar to gaussian elimination, but state it as the existence of elementary matrices that multiply to such and such, instead of as an algorithm. I imagine this distinction does not matter to mathlib?

Otherwise, I was looking at the Permutation matrices folder and I think it would be fun to formalise the following result on the characteristic polynomial of the permutation matrices

write the permutation g as a product of disjoint cycles c_r

$$g = c_1 c_2 \ldots c_k$$

where

$$c_r = (e_{1_r} e_{2_r} \ldots e_{m_r})$$

then

$$p_{\rho(g)}(x) = \prod_{r}^{k} (x^{m_r} - 1)$$

[Patrick Massot]

Alex Brodbelt said:

Patrick Massot said:

There are some things in https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Transvection.html

For instance is defining a property like IsRowEchelonForm, IsDiagonal, IsTriangularizable, and so forth of interest? These aren't defined per se... but I imagine there might be a reason for this(?)

I think the reason is that Mathlib is very much biased towards abstract stuff. So matrices are far behind linear maps. But I think those definitions would be welcome.

[Johan Commelin]

Note that docs#Matrix.diagonal and docs#Matrix.scalar exist.

[Johan Commelin]

Of course that's not exactly the same as an IsDiagonal or IsScalar predicate.

[Patrick Massot]

Alex Brodbelt said:

I've seen that there are theorems similar to gaussian elimination, but state it as the existence of elementary matrices that multiply to such and such, instead of as an algorithm. I imagine this distinction does not matter to mathlib?

This is a subtle question. It depends what you call an algorithm. You could implement a function computing Gaussian elimination assuming the coefficients are in a computable field, and then prove this function does its job. I think it would already be nice. But it would sit in some slightly uncomfortable intermediate land between having an abstract result like the one we already have and an efficient verified implementation. The later would be a lot more work and very dependent on what you want to do with this efficient implementation.

[Eric Wieser]

We also already have an unverified implementation that is maybe efficient, inside linarith

[Alex Brodbelt]

Eric Wieser said:

We also already have an unverified implementation that is maybe efficient, inside linarith

interesting! I figure this is not quite a good first challenge to start with though :lol: - I'd be curious to try though

[Peter Nelson]

Patrick Massot said:

Alex Brodbelt said:

Patrick Massot said:

There are some things in https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Transvection.html

For instance is defining a property like IsRowEchelonForm, IsDiagonal, IsTriangularizable, and so forth of interest? These aren't defined per se... but I imagine there might be a reason for this(?)

I think the reason is that Mathlib is very much biased towards abstract stuff. So matrices are far behind linear maps. But I think those definitions would be welcome.

I'm happy to see this comment, because I had been wondering about this. I have a good amount of matrix stuff in my repo regarding row space, column space, rank, and linear independence for indexed sets of vectors such as the rows/columns of a matrix. See this file, for instance. It gets as far as proving that the rank of a transposed matrix is equal to the rank, and unlike the mathlib version works over arbitrary fields and infinite row/column sets.

But I've been hesitant to start PRing that kind of stuff because it is all too 'plebeian' - my perception is that it goes against the grain of the way mathlib does things.

I think there are many parts of mathematics that need to view matrices as concrete objects rather than special cases of linear operators (eg coding theory, optimization, matroids, algebraic graph theory), and if you are in those areas, what is available in mathlib is awkward. Specifically, if the indexing sets for rows and columns of a matrix are semantically relevant, modding out by change of co-ordinates needs to be handled with care.

Would anyone that is au fait with mathlib linear algebra be able to take a quick look at that linked file and tell me if making PRs from that sort of stuff is worth the effort?

[Alex Brodbelt]

Patrick Massot said:

Alex Brodbelt said:

Patrick Massot said:

There are some things in https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Transvection.html

For instance is defining a property like IsRowEchelonForm, IsDiagonal, IsTriangularizable, and so forth of interest? These aren't defined per se... but I imagine there might be a reason for this(?)

I think the reason is that Mathlib is very much biased towards abstract stuff. So matrices are far behind linear maps. But I think those definitions would be welcome.

It's quite silly predicate... but this is not in mathlib, so could be nice to have? Makescertain theorem lemmas and theorems more readable

def IsDiagonal [Zero α] (M : Matrix n n α) : Prop :=
  ∃ d : n → α, M = diagonal d

[Kevin Buzzard]

Probably i \ne j -> M i j = 0 is easier to work with? Not sure, maybe it doesn't matter much (one will be the definition, another a theorem).

[Alex Brodbelt]

Kevin Buzzard said:

Probably i \ne j -> M i j = 0 is easier to work with? Not sure, maybe it doesn't matter much (one will be the definition, another a theorem).

I'm not sure how to golf the reverse implication... but here is my attempt

theorem IsDiagonal_iff [Zero α] { M : Matrix n n α} : IsDiagonal M ↔ ∀ i j : n, i ≠ j → M i j = 0 :=
  ⟨
    fun ⟨d, MeqD⟩ i j inej => by rw [MeqD, diagonal_apply_ne d inej],
    fun h => by let d := fun (i : n) => M i i; exact ⟨d, by ext i j; by_cases hij: i = j; rw [hij, diagonal_apply_eq]; rw [diagonal_apply_ne d hij]; apply h i j hij⟩
  ⟩

[Eric Wieser]

Certainly mathlib should have M ∈ Set.range diagonal ↔ ∀ i j : n, i ≠ j → M i j = 0 :=

[Eric Wieser]

I'm not sure we need an IsDiagonal predicate, because there is a whole family of IsFoo definitions which we can skip by using ∈ Set.range foo

[Eric Wieser]

(for instance we have no IsNat or IsRat etc, and use Set.range Nat.cast and Set.range Rat.cast instead)

[Alex Brodbelt]

Eric Wieser said:

I'm not sure we need an IsDiagonal predicate, because there is a whole family of IsFoo definitions which we can skip by using ∈ Set.range foo

Ah I see... fun to do nonetheless, how is decision of when to make a predicate made?

[Kevin Buzzard]

Every definition comes with a cost. It wraps up code into a new declaration which won't be unfolded by default, and so either all your proofs have unfold my_declaration in ( or you do it the correct way and write lots of API lemmas making your definition useful. So you have to have a correspondingly good argument for the existence of your definition in order to justify this work.

[Edward van de Meent]

i'm curious, how does making a macro/abbreviation fit into this?

[Kevin Buzzard]

Those are "problematic" for a different reason; lean can see through them (one model for what abbreviation foo := bar means is "humans are weak and don't understand bar, so whenever it shows up in the infoview print it as foo, and let them talk about foo, but really it's not actually there, it's just bar"), but I've heard an argument saying that they decrease readability: experts who know exactly what bar means understand it immediately, and might not know what foo is.

[Damiano Testa]

For what is worth, I introduced the abbrevs PosMulMono and friends, thinking that they were an improvement and managed to convince Floris, even though his reaction was "I'd rather not". Now, I regret them being there! :smile:

[Kevin Buzzard]

They were helpful for me recently because I wanted to do a calculation in WithBot (Multiplicative Int) but half the lemmas didn't fire, but because of that packaging it was easy to work out exactly what I needed to do to make them fire. See #13090 . It was only after that PR that I actually discovered that they were abbrevs!

[Damiano Testa]

Ok, I'm glad that they are helpful then!