Glue vector to a matrix

Stream: mathlib4

[Martin Dvořák]

What is the idiomatic way to glue a vector v to a matrix A please?
Originally I used

Matrix.fromRows A (Matrix.row Unit v)

but it turned out to be hard to work with.

I hope there is something like ​Matrix.of (Matrix.vecCons v A) but in one definition.
Did I overlook it?

[Eric Wieser]

Can you give a mwe of the function you want to exist? Are you using Fin-indexed or Type-indexed matrices?

[Martin Dvořák]

I'm not sure. I'd prefer Type-indexed matrices, but I will use what Mathlib has better support for.

[Martin Dvořák]

For example, is there a more idiomatic way to write the following?

import Mathlib

example (m n : ℕ) (β : Type) (A : Matrix (Fin m) (Fin n) β) (v : Fin n → β) :
    Matrix (Fin m.succ) (Fin n) β :=
  Matrix.of (Matrix.vecCons v A)

[Eric Wieser]

I think that's the preferred spelling for Fin m.succ, and the one above is the preferred spelling for Sum m Unit

[Eric Wieser]

I suppose you could ask for an Option m-valued version

[Eric Wieser]

Which of those three choices is appropriate depends on what you want to do with the matrix

[Martin Dvořák]

I guess I shouldn't have literally Matrix.of (Matrix.vecCons v A) in my theorem statement, right?

[Eric Wieser]

Or Matrix.fromRows A (Matrix.row Unit v)

[Martin Dvořák]

I want to work with determinants, but I also want to use the resulting matrix in other block matrices.

[Martin Dvořák]

I guess the Fin m.succ version will be best for me because I can do the Laplacian expansion of the determinant then.

[Martin Dvořák]

docs#Matrix.det_succ_row

[Martin Dvořák]

And perhaps it is best to first have the extra row and then the original matrix because:
docs#Matrix.det_succ_row_zero

[Martin Dvořák]

My question is what can I use in place of Matrix.of (Matrix.vecCons v A) so that it preserves the intention but has nicer API.

[Eric Wieser]

I think the answer in mathlib is "use docs#Matrix.updateColumn instead"

[Eric Wieser]

Eg, see how we define the cramer matrix by replacing a column/row with zeros and 1s, instead of removing it entirely

[Eric Wieser]

So I think this is an #xy problem, where you're asking how to do some pen-and-paper maths in a generic way (type indices) with a nice API, and the answer is possibly "don't do it the pen and paper way"

[Eric Wieser]

Presumably the glueing is an intermediate construction in a larger proof, and not part of your final statement?

[Martin Dvořák]

Yes and no.
Most of the time, it is indeed just an intermediate construction in a larger proof.
However, there will be a place where something like that will appear in the final theorem, because we will be proving things about a binary matroid defined via this matrix:
https://github.com/Ivan-Sergeyev/seymour/blob/0c8aa3de8a0cf14112e7154a8e853415e63642b5/Seymour/EasyDirection.lean#L118

[Martin Dvořák]

Eric Wieser said:

I suppose you could ask for an Option m-valued version

Indexing rows by Option would be nice, but would then Laplacian expansion of a determinant even make sense in such a setting?