Notation for Matrix (Fin m) (Fin n) R

Stream: mathlib4

[Eric Wieser]

Eric Wieser said:

I mean something like (col v : R^m×1)

Yaël Dillies said:

I was thinking something like M_[m, n][R]

#12178 explores this further

[Jon Eugster]

Exactly, I would like to add notation for M : Matrix (Fin n) (Fin m) R as I believe the two (Fin _) clutter the infoview, especially when students start doing exercises about something concrete like 3x3-Matrices.
Do people have an opinion what's the cleanest notation for such concrete matrices? (please add other suggestions):

[Jon Eugster]

/poll What would be a preferred notation for Matrix (Fin n) (Fin m) R
Mat[m, n][R]
R¹ˣ³ (does not work for variables n : Nat; Potential problem with Mᵀᵀ)
both Mat[m, n][R] and R¹ˣ³ (preferring the latter if possible)
R^[m, n] (maybe fragile with HPow? But seems alright)
R^n×m (does not work at all, currently)

[Jon Eugster]

(generally, anything with × (\times) seems very fragile or broken)

[Notification Bot]

4 messages were moved here from #mathlib4 > Why does Matrix.row use Unit instead of Fin 1? by Eric Wieser.

[Eric Wieser]

ℝ⁽ⁿ⁾ˣ² works fine

[Eric Wieser]

Though I claim that as soon as m and n are variables, Matrix (Fin m) (Fin n) is usually an antipattern anyway

[Jon Eugster]

Eric Wieser said:

Though I claim that as soon as m and n are variables, Matrix (Fin m) (Fin n) is usually an antipattern anyway

I think you are right regarding contributions to mathlib. However, in teaching I often thought I'd like to say let m n : Nat and look at (m,n)-Matrices" which feels more natural/mathematical than "let m,n be two Fintypes.". And Matrix (Fin m) (Fin n) does appear in Mathlib 62 times (GroupTheory/RingTheory/NumberTheory/LinearAlgebra), so it seems not completely unreasonable that people use it. (Can add a comment to the docstring though suggesting using Fintype!)

[Jon Eugster]

/poll What would be a preferred notation for Matrix (Fin n) (Fin m) R
Mat[m, n][R]
ℝ⁽ⁿ⁾ˣ²
both Mat[m, n][R] and R¹ˣ³ (preferring the latter if possible)
R^[m, n]
R^n×m (does not work at all, currently)

[Jon Eugster]

(apparently I can't delete/modify a poll :neutral: )

[Eric Wieser]

You get in trouble quite quickly with Fin m if you want to use block matrices or kronecker matrices or ...

[Antoine Chambert-Loir]

Jon Eugster said:

Exactly, I would like to add notation for M : Matrix (Fin n) (Fin m) R as I believe the two (Fin _) clutter the infoview, especially when students start doing exercises about something concrete like 3x3-Matrices.
Do people have an opinion what's the cleanest notation for such concrete matrices? (please add other suggestions):

My opinion is matrices should be indexed by general (possibly finite) types, there's most of the time no need that they be of the form ‘Fin n‘ for some natural number n. In fact this is even often a nuisance.

[Kevin Buzzard]

Give Type an OfNat instance

[Kevin Buzzard]

(ZMod)

[Yaël Dillies]

Antoine Chambert-Loir said:

My opinion is matrices should be indexed by general (possibly finite) types, there's most of the time no need that they be of the form ‘Fin n‘ for some natural number n. In fact this is even often a nuisance.

What about Mat[ι, κ][R] being notation for Matrix ι κ R and Mat[m, n][R] being notation for Mat[Fin m, Fin n][R]?

[Yaël Dillies]

This could be made to work because the notation could look at whether the expected type is Type _ or Nat

[Eric Wieser]

But the notation isn't any shorter!

Mat[ι, κ][R]
Matrix ι κ R

[Eric Wieser]

Kevin Buzzard said:

Give Type an OfNat instance

This works:

instance : CoeSort Nat Type where
  coe := Fin

#check Matrix (2 :) (2 :) ℕ -- Matrix (Fin 2) (Fin 2) ℕ : Type

[Mitchell Lee]

I think we are underestimating the cognitive burden caused by adding an extra definition or piece of notation. In my opinion, it easily eclipses the benefit of not having to type Fin a couple times.

[Jireh Loreaux]

@Jon Eugster it makes it a bit difficult to explain what's going on in, e.g., the row swaps in Gaussian elimination if the indices don't come from a type, since a row swap is precisely a reindexing of the rows of a matrix, but for this they need to be numbered (not just have a cardinality).

[Jon Eugster]

@Jireh Loreaux I get that, I'm also not arguing for (Fin m) instead of [Fintype m] for statements in mathlib.

Instead, my assumption is that the notation !![2, 2; 4, 5] : Matrix (Fin 2) (Fin 2) R should be a well-integrated part into mathlib, but so far I have the experience that it's not as smooth as I'd like it to be. And as part of working with this notation I thought it would also be nice if the type was displayed as simple as Mat[2,2][R] so that one doesn't even need to parse these additional Fin floating around.

But maybe it's just a wrong assumption that this is how one should use the API for calculations with simple, concrete matrices as you would find them in an undergrad exercise sheet (or in some science application) .

[Eric Wieser]

Writing a simproc for !![a, b] * !![c; d] is on my todo list; I had one in Lean 3, but it never got merged.

[Jireh Loreaux]

Jon, I think for numerals only that syntax could be nice. However, I think it would be confusing to allow Mat[m,n] to mean Matrix (Fin m) (Fin n) where m n : Nat. That's because throughout Mathlib, people will see Matrix m n, and, not realizing the distinction, think that this is the same thing as Mat[m,n], when it really isn't. But if we restrict it to work only for numerals, I think that's less of an issue and suits your use case better.