feat(data/matrix/basic): add defs index_assoc and linear_equiv_index_assoc

[faenuccio]

Added two lemmas showing that matrix ((m × n) × o) ((m₁ × n₁) × o₁) R and matrix (m × n × o) (m₁ × n₁ × o₁) R are equivalent; the second lemma shows that they are linearly equivalent if the coefficients are a module over a base semiring.

---

[eric-wieser]

Both of these are trivial applications of existing functions, and it's not clear to me that these cases are any more special than any of the other trivial special cases.

[faenuccio]

Both of these are trivial applications of existing functions, and it's not clear to me that these cases are any more special than any of the other trivial special cases.

You mean to simply use that ((m x n) x p) and (m x n x p) are equivalent?

[pechersky]

Both of these are trivial applications of existing functions, and it's not clear to me that these cases are any more special than any of the other trivial special cases.

Can we just put these specializations of reindex into data.matrix.reindex?

[eric-wieser]

My thoughts are that these definitions aren't going to help you if you want to show any of

• matrix ((m × n) × o) (m₁ × n₁ × o₁) R ≃ matrix (m × n × o) ((m₁ × n₁) × o₁) R
• matrix ((m × n) × o) m₁ R ≃ matrix (m × n × o) m₁ R

We already have a general tool for solving this type of problem and it's matrix.reindex. If the case in this PR comes up particularly often for you, then we should probably either:

• add a comment in the docstring of kronecker_product or wherever this actually ends up being useful.
• add a comment in the docstring of matrix.reindex pointing out the existance of equiv.prod_assoc.

What's the use-case of these definitions?

[eric-wieser]

Can we just put these specializations of reindex into data.matrix.reindex?

That's a reasonable compromise too.

[faenuccio]

Can we just put these specializations of reindex into data.matrix.reindex?

That's a reasonable compromise too.

They come up somewhat often especially in statement of theorems. For their intelligibility It is therefore handy, I believe, that there is a name for the function instead of an application of other ones. I am of course happy to have it land in data.matrix.reindex if you so advise. If you want to delete it, I will modify my code for Kronecker products.

[eric-wieser]

Is the kronecker product code something you plan to PR? If so, perhaps it makes sense to put this PR on hold until we have the kronecker API to evaluate it by

[faenuccio]

Is the kronecker product code something you plan to PR? If so, perhaps it makes sense to put this PR on hold until we have the kronecker API to evaluate it by

Yes, it is actually ready but it uses these two lemmas. I though that I first needed to have them approved, then merge mathlib and then PR that file. I am happy to PR it now, but how should I do concretely?

1. PR a branch with data/matrix/basic.lean modified with the above two lemmas, and with the new file about the Kronecker product
2. Add these lemmas to my file about Kronecker product (marking them to move, or something) - this might be slightly painful with variables names
3. Other ideas?

[faenuccio]

I have created #8152 (marked as blocked-by-this-PR) with the definition of Kronecker product.

[jcommelin]

@faenuccio I suggest that you move these to the reindex file, and prove them as one-liners, the way that Eric suggests.
After that, merge this branch into the Kronecker branch, and then we take a look at that PR.

[faenuccio]

@faenuccio I suggest that you move these to the reindex file, and prove them as one-liners, the way that Eric suggests.
After that, merge this branch into the Kronecker branch, and then we take a look at that PR.

Done: I've created data.matrix.reindex and I have inserted these two equivalences there. The first is a one-linear, as suggested by @eric-wieser . The second is not, because we don't have the linear equivalence one yet.

[eric-wieser]

We do have the linear equivalence, it's here: https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix/reindex.html#matrix.reindex_linear_equiv

[faenuccio]

Ok, I've imported it but I still get an error. I'll be back on this in half a hour or so. In the meanwhile, I have updated the PR concerning the Kronecker product.

[eric-wieser]

The reason you get the error is because reindex_linear_equiv produces the stronger R-linear equiv; there is no need to introduce α.

The caller can always weaken the strength of the linearity using linear_equiv.restrict_scalars.

[eric-wieser]

Suggested change

	def linear_equiv_index_assoc [comm_semiring α] [add_comm_monoid R] [module α R] :
	matrix ((m × n) × o) ((m₁ × n₁) × o₁) R ≃ₗ[α] matrix (m × n × o) (m₁ × n₁ × o₁) R :=
	def linear_equiv_index_assoc :
	matrix ((m × n) × o) ((m₁ × n₁) × o₁) R ≃ₗ[R] matrix (m × n × o) (m₁ × n₁ × o₁) R :=

[eric-wieser]

Oh, I now see that your statement is actually more general - I think we should modify matrix.reindex_linear_equiv to use your formulation with an extra (explicit) α variable!

[eric-wieser]

Done in

• [Merged by Bors] - feat(linear_algebra/matrix/reindex): generalize reindex_linear_equiv to operate on an arbitrary ring #8159

[pechersky]

Sorry for the earlier confusion -- I meant that these reindexing specializations should likely go in the file that defines the more general ones -- linear_algebra.matrix.reindex. I mixed up the prefix linear_algebra with data, apologies.

[eric-wieser]

In https://github.com/leanprover-community/mathlib/pull/8289/files#r669516077, @l534zhan suggested adding the following variants, one of which is the one in this PR:

mathlib/src/data/matrix/basic.lean

Lines 1204 to 1215 in 75a4d4a

	def reindex_prod_assoc :
	matrix ((l × m) × n) ((o × p) × q) α ≃ matrix (l × m × n) (o × p × q) α :=
	reindex (equiv.prod_assoc _ _ _) (equiv.prod_assoc _ _ _)
	def reindex_prod_comm_snd : matrix l (m × n) α ≃ matrix l (n × m) α :=
	reindex (equiv.refl _) (equiv.prod_comm _ _)
	def reindex_prod_comm_fst : matrix (l × m) n α ≃ matrix (m × l) n α :=
	reindex (equiv.prod_comm _ _) (equiv.refl _)
	def reindex_prod_comm : matrix (m × n) (p × q) α ≃ matrix (n × m) (q × p) α :=
	reindex (equiv.prod_comm _ _) (equiv.prod_comm _ _)

I don't know where we want to draw the line here on, but thought we should at least be aware of these when reviewing this PR.

[faenuccio]

I have updated the file using @eric-wieser PR #8159. Concerning https://github.com/leanprover-community/mathlib/pull/8289/files#r669516077, I am happy to follow your advice (and don't have any particular opinion, a part the fact that if these things need to land in mathlib, this is probably the right place to have them).

[eric-wieser]

To reiterate my stance; I think these definitions are probably harmless, but since they now amount only to a single line each, it would make more sense to me just review them at the same time as the rest of #8152, where they can be reviewed in context.

[faenuccio]

Right: if I get your point, you're suggesting to try to use these one-line proofs in #8152 directly, and only then to judge whether we really want this PR or not?

[eric-wieser]

I'm suggesting merge this commit into that PR, and assume that the new defs are ok. We can then review that PR, and decide whether the places you use them justify their existence.

[faenuccio]

Shall we kill this PR?

[jcommelin]

I don't think we need this anymore, so let's close it. Thanks for all the Kronecker stuff!