Kronecker product

Stream: condensed mathematics

[Filippo A. E. Nuccio]

I am preparing a file defining the Kronecker product and I have defined it in a somewhat general setting of two R-algebras A,B as a map

$$M_{l, m} (A) \rightarrow M_{n, p} (B) \rightarrow M_{(l\cdot n), (m\cdot p)} (A\otimes_R B)$$

and I wonder if it is the right setting

[Eric Wieser]

@Johan Commelin and I discussed this privately, and I think we concluded it was, but we might also need a shorthand for the multiplication version

[Filippo A. E. Nuccio]

Yes, this is what I though. May be the best option is to discuss having a look at the mathlib branch fae_kronecker where I define it and to tell me what you came up with?

[Johan Commelin]

@Filippo A. E. Nuccio Great! Are both maps lean-R-linear?

[Filippo A. E. Nuccio]

They are

[Johan Commelin]

If LTE compiles using your version, then I'm happy

[Filippo A. E. Nuccio]

Well, the problem is that I have to do a thousands modifications and I'd like a bit of feedback before starting them. The main point, as @Eric Wieser was observing, is that in LTE we mostly use it for A=R=B=$\mathbb{Z}$ and it might be important to have a simplified version, no?

[Filippo A. E. Nuccio]

I don't know if you have time now, at any rate my definition is is linear_algebra/matrix/kronecker_product of the branch fae_kronecker https://github.com/leanprover-community/mathlib/tree/fae_kronecker

[Johan Commelin]

I think the question I have is mainly with things like https://github.com/leanprover-community/mathlib/compare/fae_kronecker#diff-3fccdc12101122868979386cc6fcf6a22bb09a32cff57bc5d0fc92a7480a6f6bR30 how often will Lean complain that it can't figure out $\alpha$?

[Filippo A. E. Nuccio]

Indeed it sometimes/often does.

[Johan Commelin]

And also, if $A = R = B$, then $A \otimes_{R} B \cong R$, but that's of course not defeq. So we want a version that is post-composed with the canonical iso $A \otimes_R B \to R$ so that it takes values in $\mathrm{Mat}_{m,n}(R)$.

[Filippo A. E. Nuccio]

Yes, I see.

[Filippo A. E. Nuccio]

This should not be hard having what I have already.

[Filippo A. E. Nuccio]

But would you keep in the new version $R$ as an explicit or implicit variable?

[Johan Commelin]

In the case where $A = R = B$, then $R$ can be implicit, because it can be inferred from either of the two matrices.

[Filippo A. E. Nuccio]

And, secondly, is there a way to make all lemmas about additivity/transitivity/associativity/blabla go through automagically from the previous versions or should I restate them all?

[Filippo A. E. Nuccio]

It won't take long but I just want to avoid stupid work...

[Johan Commelin]

I'm afraid we don't have any magic for that yet :sad:

[Filippo A. E. Nuccio]

OK. Does it then sound like a good plan that I start a second section in that file introducing the special case $A=B=R$ and that I restate and prove all the previous results?

[Filippo A. E. Nuccio]

I will then try to use this in LTE and keep you informed.

[Johan Commelin]

Sounds good!

[Filippo A. E. Nuccio]

And is there a way to specify this in the notation? Because I have introduced

variables {α}
infix ` ⊗ₖ `:100 := kronecker_prod _
notation x ` ⊗ₖ[`:100 α `] `:0 y:100 := kronecker_prod x y

for the generic Kronecker product, and was wondering if this can be "specialized" to the case where $A=R=B$.

[Johan Commelin]

Maybe reserve

infix ` ⊗ₖ `:100 := _

for the specialized version?

[Filippo A. E. Nuccio]

This is certainly one option, but it is a bit sad.

[Filippo A. E. Nuccio]

At any rate, if that's your advice, I'll follow it.

[Johan Commelin]

Well, probably the other option is to add a ' somewhere.

[Filippo A. E. Nuccio]

Ah, can I also do this on the notation?

[Filippo A. E. Nuccio]

(in the sense: is it enough for Lean to figure out they're different operations according at whether the apostrophe is there or not?)

[Johan Commelin]

⊗ₖ' can certainly be a new sort of notation

[Adam Topaz]

I'm a bit late to the party, but to avoid defeq stuff, you can replace the tensor product with an arbitrary algebra endowed with morphisms from A and B.

[Filippo A. E. Nuccio]

I'm also a little bit late now (and am running away, but will read your answer later): do you mean to replace which of the three terms? Are you speaking about the general definition, so defining something along the lines of

$$\mathrm{Mat}_{l,m}(A)\longrightarrow \mathrm{Mat}_{p,q}(B)\longrightarrow \mathrm{Mat}_{l\cdot p, m\cdot q}(R)$$

where $R$ is a $(A,B)$-bimodule/bialgebra? If I got it right, it seems a nice idea and I will probably try to implement this.

[Adam Topaz]

TBH I only had the commutative case in mind (i.e. where the base-ring, $A$ and $B$ are all commutative)

[Filippo A. E. Nuccio]

Following @Adam Topaz and @Johan Commelin suggestions, I have finally created a file developing Kronecker product in the general setting of three algebras as a map

$$\mathrm{Mat}_{l,m}(A)\longrightarrow \mathrm{Mat}_{p,q}(B)\longrightarrow \mathrm{Mat}_{l\cdot p, m\cdot q}(R)$$

I have just pushed the PR #8147 constructing the equivalence between ((l x m) x n) ((l' x m') x n')-matrices and (l x m x n) (l' x m' x n')-matrices. Once it will be merged, I will be able to push the file about Kronecker product.

[Filippo A. E. Nuccio]

I think I will also introduce some version of Kronecker product for tensor algebras (and compare the two) to show that the Kronecker product of matrices corresponds to the abstract tensor product of linear maps.

[Kevin Buzzard]

@Alex Zhang

[Filippo A. E. Nuccio]

I have created #8152 containing the Kronecker product as above. It relies on the previous one, so it is marked blocked-by-other-PR.

[Filippo A. E. Nuccio]

@Johan Commelin @Eric Wieser The last suggestions on #8147 are committed and I have made a couple of small changes to #8152. I am leaving for 2/3 weeks on vacation. If nothing is too urgent, you can add a waiting-for-author tag and I can resume working on both PR as well as implementing the tensor-product version of Kronecker product. Thanks to both for your suggestions and improvements!

[Johan Commelin]

Enjoy your holidays!

[Eric Wieser]

I think @Adam Topaz's suggestion to replace the tensor product with an algebra endowed with a pair of morphisms was a distraction; that's just composing the simple * version with algebra_map, and pulls in lots of unnecessary assumptions and noise in proofs as a result. A better generalization in my opinion is just "any bilinear operation", which is what I've tried in #8560.

[Eric Wieser]

(or actually just "any binary operation", but the interesting lemmas require bilinearity)

[Johan Commelin]

the kronecker PRs have been merged!

[Filippo A. E. Nuccio]

Yes, I am working on the mathlib bumpright now!

[Filippo A. E. Nuccio]

I wanted to check everything works with the new versions before merging

[Filippo A. E. Nuccio]

OK, I have bumped mathlib and merged. Most of the files are still OK but I have sorryd out four lemmas which need to be refactored a bit. I won't have time today but I'll do it tomorrow.

[Johan Commelin]

Thanks!

[Johan Commelin]

It looks like we are missing lemmas that say how kronecker interacts with reindex

[Eric Wieser]

Probably because those statements are all proved with ext; refl and there are tonnes of variants.

[Eric Wieser]

I guess docs#matrix.kronecker_assoc is not the right variant?

[Eric Wieser]

(also, I don't understand why the simp_nf linter accepts that lemma, reindex is not simp-normal)

[Johan Commelin]

Maybe it is in LTE's nolints.txt?

[Eric Wieser]

Given the lemma is in mathlib that probably wouldn't have an effect ;)

[Filippo A. E. Nuccio]

Yes, this is exactly the point.

[Filippo A. E. Nuccio]

My first option would be to re-add them to LTE as they were (it would suffice to add them to Breen-Deligne/universal.lean), given that they have not been accepted as part of mathlib. Another option is to play a bit with the simp call in these four LTE lemmas and work out the situation. I am happy with the second, although the first is certainly quicker.

[Johan Commelin]

I think option (1) is fine. We can always improve later.

[Filippo A. E. Nuccio]

Ok, this won't take a lot of time. I'll do it later this morning.

[Eric Wieser]

Could you link to a place in lean-liquid where the lemmas are used?

[Filippo A. E. Nuccio]

Give me 3 mins

[Filippo A. E. Nuccio]

From the first file:
https://github.com/leanprover-community/lean-liquid/blob/5ee83405041faa4c50807333477f0949a47a2c2f/src/breen_deligne/universal_map.lean#L257

[Filippo A. E. Nuccio]

Then
https://github.com/leanprover-community/lean-liquid/blob/5ee83405041faa4c50807333477f0949a47a2c2f/src/breen_deligne/category.lean#L76
and
https://github.com/leanprover-community/lean-liquid/blob/5ee83405041faa4c50807333477f0949a47a2c2f/src/breen_deligne/category.lean#L104

[Filippo A. E. Nuccio]

And finally
https://github.com/leanprover-community/lean-liquid/blob/5ee83405041faa4c50807333477f0949a47a2c2f/src/thm95/row_iso.lean#L279

[Filippo A. E. Nuccio]

All other occurrences of kronecker-stuff are OK (AFAIK).

[Filippo A. E. Nuccio]

The first lemma (in breen_deligne/universal_map) is now OK (without reinserting the reindex lemmas)

[Filippo A. E. Nuccio]

@Eric Wieser Are you working on some of the others (I ask simply to avoid working on the same lemma at the same time)?

[Eric Wieser]

Nope, I was just curious

[Eric Wieser]

I'm surprised your proof doesn't use the assoc lemma we have already though

[Eric Wieser]

Why doesn't that lemma apply?

[Filippo A. E. Nuccio]

Well, because it needed some application of the reindexing lemmas and apparently the simplifier was not able to work things through.

[Eric Wieser]

Do you have the goal state which the lemma wouldn't match against?

[Filippo A. E. Nuccio]

No, I am sorry. I have refactored the proof a bit and now I don't have it anymore (it is in some past commit, though, of course).

[Filippo A. E. Nuccio]

One lemma left to go. For mul_mul_iso_aux I had to re-insert two of the three kronecker-reindex lemmas (see https://github.com/leanprover-community/lean-liquid/blob/342f4779232d0b7a54305058e2c4566d2fbb4782/src/breen_deligne/category.lean#L129 for the rw, which I have intentionally not merged with the one in the previous line, where these lemmas are needed).

[Filippo A. E. Nuccio]

IMHO it is worth opening a PR and insert these two into mathlib, but I would like @Eric Wieser and @Johan Commelin 's opinion before starting another tour de force for just two small lemmas.

[Eric Wieser]

If those go into mathlib they should probably be expressed with matrix.reindex or even matrix.minor since that's the simp normal form

[Eric Wieser]

I think otherwise they'd be fine though

[Filippo A. E. Nuccio]

instead of matrix.reindex_linear_equiv, you mean?

[Filippo A. E. Nuccio]

but how to derive the linear version from that one, then?

[Eric Wieser]

simp will unfold matrix.reindex_linear_equiv to minor via reindex

[Filippo A. E. Nuccio]

but they are not simp lemma now: you would like them to be marked as such?

[Eric Wieser]

No, I mean that if you have an appliedmatrix.reindex_linear_equiv in your goal state, you should dsimp it to minor before looking for a suitable lemma to rewrite by

[Eric Wieser]

Having said that, I think this would be a good simp lemma:

(M ⊗ₖ N).minor (e1.prod_congr e2) (e3.prod_congr e4) = (M.minor e1 e3) ⊗ₖ (N.minor e1 e3)

[Eric Wieser]

I would possibly argue that this lemma:
https://github.com/leanprover-community/lean-liquid/blob/7fc9a246aba1ff88996d2a3a8a8b3dc7ed7b833a/src/breen_deligne/universal_map.lean#L128-L130
should state

lemma mul_apply (N : ℕ) (f : basic_universal_map m n) :
  mul N f = matrix.reindex fin_prod_fin_equiv fin_prod_fin_equiv (1 ⊗ₖ f) :=
rfl

which would get reindex_linear_equiv out of the way immediately.

[Filippo A. E. Nuccio]

But would probably entail a huge deal of refactor for all other lemmas calling it, no?

[Filippo A. E. Nuccio]

I guess this is the statement you had in mind, right?

lemma kronecker_reindex_right' [semiring R] (em : m₂ ≃ m₁) (en : n₂ ≃ n₁) (M : matrix l₁ l₂ R)
  (N : matrix m₁ n₁ R) : M ⊗ₖ (N.minor em en)  =
    (M ⊗ₖ N).minor ((equiv.refl _).prod_congr em) ((equiv.refl _).prod_congr en) :=
by { ext ⟨i, i'⟩ ⟨j, j'⟩, refl }

Yet I have not understood what you mean by "dsimp my goal (where I have matrix.reindex_linear_equiv) to minor.

[Eric Wieser]

I wouldn't expect the refactor to be that bad

[Eric Wieser]

I mean "if you have that def in your goal state, run dsimp before looking for a suitable lemma"

[Johan Commelin]

Some of the proofs in col_exact.lean can timeout by adding an extra dsimp... it's that bad

[Eric Wieser]

Then I guess I mean pretend to be dsimp and rw matrix.reindex_linear_equiv_apply (docs#matrix.reindex_linear_equiv_apply)

[Johan Commelin]

Btw, CI is now showing a :cross_mark: since we enabled a check that shows thm95 is sorry free.

[Johan Commelin]

@Filippo A. E. Nuccio do you think you can fix the Kronecker sorry's today? Or would you like some help?

[Filippo A. E. Nuccio]

@Johan Commelin I think it will be OK very soon (with the two added lemmas, while we decide whether or not to integrate them in mathlib but the :cross_mark: will disappear).

[Filippo A. E. Nuccio]

Ok, done. I have also applied some of @Eric Wieser 's suggestions: the lemmas to add to mathlib would be

lemma kronecker_reindex_right [semiring R] (em : m₁ ≃ m₂) (en : n₁ ≃ n₂) (M : matrix l₁ l₂ R)
  (N : matrix m₁ n₁ R) : M ⊗ₖ (matrix.reindex em en N) =
  matrix.reindex
    ((equiv.refl _).prod_congr em) ((equiv.refl _).prod_congr en) (M ⊗ₖ N) :=
by { ext ⟨i, i'⟩ ⟨j, j'⟩, refl }

together with the left variant. If this seems OK I can open a PR (the variant with .minor is like an _apply-version, I guess: in particular, it requires more rewriting than the above ones).

[Eric Wieser]

That looks reasonable to me, and matches the style of the existing assoc lemmas

[Eric Wieser]

Although it should be about kronecker_map f not kronecker, since it's true for all f

[Filippo A. E. Nuccio]

Filippo A. E. Nuccio said:

Johan Commelin I think it will be OK very soon (with the two added lemmas, while we decide whether or not to integrate them in mathlib, but the :cross_mark: will disappear).

Green again! :check_mark:

[Filippo A. E. Nuccio]

Eric Wieser said:

Although it should be about kronecker_map f not kronecker, since it's true for all f

Done! #8774