[Merged by Bors] - feat(matrix/kronecker): Add the Kronecker product

[eric-wieser]

Largely derived from #8152, avoiding the complexity of introducing algebra_maps.

This introduces an abstraction kronecker_map, which is used to support both mul and tmul without having to redo any proofs.

---

Present in this PR but not #8152:

• Lemmas about map and transpose
• The name kronecker instead of kronecker_prod; prod usually means an n-ary product in mathlib. not *. I am happy to change this.
• Arithmetic lemmas specializd to ⊗ₖ like (A₁ + A₂) ⊗ₖ B = A₁ ⊗ₖ B + A₂ ⊗ₖ B
• The tensor product version A ⊗ₖₜ[R] B (which was almost but not quite in the original PR

Present in #8152 but not this PR (left for a follow-up):

• A kronecker_biprod equivalent to (algebra.linear_map _ _).map_matrix A ⊗ₖ (algebra.linear_map _ _).map_matrix B
• Lemmas about associativity

Things I particularly want feedback on:

• Is the notation reasonable?
• Are the names reasonable?
• Should the tensor product versions go in a different file?

[faenuccio]

I think it is a very good file, both concerning notations and definitions. I have some comments which I will insert below, but I believe that associativity is really necessary (it certainly is in LTE). Creating a different file for the tensor products seems too much (to me), I would rather consider creating a different file (probably in linear_algebra) showing that the Kronecker product corresponds to the tensor product of linear maps when fixing basis.

[faenuccio]

I would call this kronecker_prod or kronecker_mul rather than simply kronecker.

[eric-wieser]

My only fear with kronecker_mul is that we end up with the lemma mul_kronecker_mul_mul which is confusing!

[eric-wieser]

Another option would be kmul to match tmul, smul.

[faenuccio]

Good option! My point is that kronecker is a name for a thousand things in maths (from Wikipedia: Kronecker limit formula, Kronecker's congruence, Kronecker delta, Kronecker comb, Kronecker symbol, Kronecker product, Kronecker's method for factorizing polynomials, Kronecker substitution, Kronecker's theorem in number theory, Kronecker's lemma, and Eisenstein–Kronecker numbers) and I'd rather help a user specifying this is the product.

[jcommelin]

@faenuccio but it is namespaced to matrix.kronecker. I think that's sufficiently unambiguous, right?

[eric-wieser]

Creating a different file for the tensor products seems too much (to me)

The reason I suggest this is that the tensor product version brings in an import of ring_theory.tensor_algebra, which probably pulls in a lot of imports. It's entirely plausible no one cares though.

[faenuccio]

Creating a different file for the tensor products seems too much (to me)

The reason I suggest this is that the tensor product version brings in an import of ring_theory.tensor_algebra, which probably pulls in a lot of imports. It's entirely plausible no one cares though.

Ok, mine was just an "organizational" point of view (in my mind, something substantial requires a new file, while things here seem so close to each other that this is not needed) but if you have stronger arguments I don't have any objection.

[eric-wieser]

I believe that associativity is really necessary (it certainly is in LTE).

I agree, but I'd like to leave that to a follow up. In particular, I'm considering introducing a new Prop for that kind of statement:

/-- A property indicating that two matrices are equal modulo reindexing --/
def equal_mod_reindex (A : matrix l m α) (B : matrix n p α) (e : l ≃ n) (e' : m ≃ p) : Prop :=
A = B.minor e e'

notation A ` =ᵢ[`:50 e `, ` e' `] ` B:50 := equal_mod_reindex A B e e'

def equal_mod_reindex.eq {A : matrix l m α} {B : matrix n p α} {e : l ≃ n} {e' : m ≃ p}
  (h : A =ᵢ[e, e'] B) : A = B.minor e e' := h

@[symm]  -- TODO: add trans and refl
def equal_mod_reindex.symm {A : matrix l m α} {B : matrix n p α} {e : l ≃ n} {e' : m ≃ p}
  (h : A =ᵢ[e, e'] B) : B =ᵢ[e.symm, e'.symm] A :=
by convert ((matrix.reindex e.symm e'.symm).symm_apply_apply B).symm

def equal_mod_reindex_comm {A : matrix l m α} {B : matrix n p α} {e : l ≃ n} {e' : m ≃ p} :
  A =ᵢ[e, e'] B ↔ B =ᵢ[e.symm, e'.symm] A :=
⟨equal_mod_reindex.symm, equal_mod_reindex.symm⟩

lemma kronecker_map_comm (f : α → β → γ) (g : β → α → γ) (hcomm : ∀ a b, f a b = g b a)
  (A : matrix l m α) (B : matrix n p β) :
  kronecker_map f A B =ᵢ[prod_comm _ _, prod_comm _ _] kronecker_map g B A :=
ext $ λ i j, hcomm _ _

lemma kronecker_map_assoc (f : α → β' → γ') (g : β → γ → β') (f' : α' → γ → γ') (g' : α → β → α')
  (hassoc : ∀ a b c, f a (g b c) = f' (g' a b) c)
  (A : matrix l m α) (B : matrix n p β) (C : matrix l' m' γ):
  kronecker_map f A (kronecker_map g B C)
    =ᵢ[(prod_assoc _ _ _).symm, (prod_assoc _ _ _).symm]
      (kronecker_map f' (kronecker_map g' A B) C) :=
ext $ λ i j, hassoc _ _ _

[faenuccio]

I believe that associativity is really necessary (it certainly is in LTE).

I agree, but I'd like to leave that to a follow up. In particular, I'm considering introducing a new Prop for that kind of statement:

/-- A property indicating that two matrices are equal modulo reindexing --/
def equal_mod_reindex (A : matrix l m α) (B : matrix n p α) (e : l ≃ n) (e' : m ≃ p) : Prop :=
A = B.minor e e'

notation A ` =ᵢ[`:50 e `, ` e' `] ` B:50 := equal_mod_reindex A B e e'

def equal_mod_reindex.eq {A : matrix l m α} {B : matrix n p α} {e : l ≃ n} {e' : m ≃ p}
  (h : A =ᵢ[e, e'] B) : A = B.minor e e' := h

@[symm]  -- TODO: add trans and refl
def equal_mod_reindex.symm {A : matrix l m α} {B : matrix n p α} {e : l ≃ n} {e' : m ≃ p}
  (h : A =ᵢ[e, e'] B) : B =ᵢ[e.symm, e'.symm] A :=
by convert ((matrix.reindex e.symm e'.symm).symm_apply_apply B).symm

def equal_mod_reindex_comm {A : matrix l m α} {B : matrix n p α} {e : l ≃ n} {e' : m ≃ p} :
  A =ᵢ[e, e'] B ↔ B =ᵢ[e.symm, e'.symm] A :=
⟨equal_mod_reindex.symm, equal_mod_reindex.symm⟩

lemma kronecker_map_comm (f : α → β → γ) (g : β → α → γ) (hcomm : ∀ a b, f a b = g b a)
  (A : matrix l m α) (B : matrix n p β) :
  kronecker_map f A B =ᵢ[prod_comm _ _, prod_comm _ _] kronecker_map g B A :=
ext $ λ i j, hcomm _ _

lemma kronecker_map_assoc (f : α → β' → γ') (g : β → γ → β') (f' : α' → γ → γ') (g' : α → β → α')
  (hassoc : ∀ a b c, f a (g b c) = f' (g' a b) c)
  (A : matrix l m α) (B : matrix n p β) (C : matrix l' m' γ):
  kronecker_map f A (kronecker_map g B C)
    =ᵢ[(prod_assoc _ _ _).symm, (prod_assoc _ _ _).symm]
      (kronecker_map f' (kronecker_map g' A B) C) :=
ext $ λ i j, hassoc _ _ _

I see. Well, I guess that you will need a maintainer to verify and validate this PR. IMHO all this deserves to land in mathlib only once associativity is there, but of course someone more experienced than myself will decide. Same for kmul, bilinear vs linear and the other commit I proposed.

[jcommelin]

This looks like a nice abstraction! Thanks for the PR!

[jcommelin]

@faenuccio but it is namespaced to matrix.kronecker. I think that's sufficiently unambiguous, right?

[jcommelin]

Should this be a simp-lemma? Same for the next lemma.

[eric-wieser]

I think probably not, since we don't make the corresponding lemma for mul instead of kronecker simp.

[eric-wieser]

@jcommelin, are you happy with the idea of renaming kronecker_tmul to ktmul and kronecker to kmul?

[jcommelin]

@eric-wieser I think I would just keep the name matrix.kronecker. But if people think it is too long, then kmul is fine.

[eric-wieser]

Alright, I'll leave the name as is and let someone who gets annoyed by the long name rename it later.

[jcommelin]

bors d+

[bors]

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests