Definition of circulant matrices

Stream: maths

[Wrenna Robson]

I'm just looking at the definition we have of circulants. https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix/circulant.html

The definition I am more familiar with has the circulant matrix generated by cycling the rows, not - as here - the columns.

While it doesn't strictly matter - a row-generated circulant is also a column-generated circulant (v : n → α and λ (i : n), v (-i)) respectively)- it does require a slightly tiresome amount of translation, and means that there are some lemmas that are natural and true but not present - for instance, a vec_mul version of matrix.circulant_mul.

What do people think the best way to allow for both the row-form and column-form would be? And does anyone know why it was defined in terms of columns to begin with - is this standard in some other context?

[Wrenna Robson]

Sorry, I actually see wikipedia does do it by column! So probably that is the answer. But one can certainly also do it via row (see page 31 in https://bikesuite.org/files/v4.2/BIKE_Spec.2021.09.29.1.pdf).

[Wrenna Robson]

One might also want an is_circulant predicate, and certainly it is true that the subring of circulant matrices over a ring R indexed by fin n are isomorphic to polynomials in R[X]/(X^n - 1) (which, per my other recent question, are in turn isomorphic to vectors of the form fin n -> R with the multiplication that corresponds to the convolution operation).

[Wrenna Robson]

https://github.com/leanprover-community/mathlib/pull/9011 - looks like this was the only substantive commit to this file. @Johan Commelin @Eric Wieser, sorry to bother you, but it looks like the original author of this file isn't on Zulip and you were the reviewers: do you have any opinions about changes or extensions to this?

[Wrenna Robson]

I don't ask arbitrarily - the theory of quasi-cyclic codes is intimately connected to circulant properties.

[Eric Wieser]

The PR author is @Alex Zhang

[Wrenna Robson]

Ah - thank you. I was looking for the name at the top.

[Alex Zhang]

@Wrenna Robson Hi! I am not actively working on PRs currently, but I still keep an eye here. I may be back later and write more things later.

[Wrenna Robson]

Hey; love the circulant work! If you have a mo I would appreciate a look at my above questions.

[Alex Zhang]

@Wrenna Robson Yes, I don't see there is any substantial difference between the row definition and the column definition. So I think either way is fine. is_circulant may be helpful if you need such a thing very often in your work, but this is also a very simple thing. More interesting things may be to write more algebraic connections (I may have already written some, but I don't remember now..) as the current file is quite basic.

[Wrenna Robson]

Yes, it's purely to aid in the construction of the circulants.