Mathlib upstream candidate: the Kronecker factor embeddings as algebra homomorphisms

Category: 1-Mathlib (CSD-free).

Mathlib packages the Kronecker product as the algebra equivalence Matrix.kroneckerAlgEquiv m n R : (Matrix m m R ⊗[R] Matrix n n R) ≃ₐ[R] Matrix (m × n) (m × n) R but has no bundled form of the two factor embeddings A ↦ A ⊗ₖ 1 and B ↦ 1 ⊗ₖ B. They are the compositions of that equivalence with the tensor-factor inclusions Algebra.TensorProduct.includeLeft / includeRight:

• Matrix.kroneckerLeftAlgHom R m n : Matrix m m R →ₐ[R] Matrix (m × n) (m × n) R, A ↦ A ⊗ₖ 1;
• Matrix.kroneckerRightAlgHom R m n : Matrix n n R →ₐ[R] Matrix (m × n) (m × n) R, B ↦ 1 ⊗ₖ B;

with the API a bipartite-system consumer needs: the images commute (commute_kroneckerLeftAlgHom_kroneckerRightAlgHom), their products are the Kronecker products (kroneckerLeftAlgHom_mul_kroneckerRightAlgHom), they preserve the conjugate transpose (kroneckerLeftAlgHom_conjTranspose), and they generate: the subalgebra generated by the two images is everything (adjoin_range_kroneckerLeftAlgHom_union_eq_top), because the matrix units single (i, j) (k, l) 1 = single i k 1 ⊗ₖ single j l 1 lie in it.

The generation step is factored through the matrix-unit criteria Submodule.eq_top_of_forall_single_mem / Subalgebra.eq_top_of_forall_single_mem (a submodule or subalgebra of a matrix algebra containing every matrix unit is everything — Matrix.stdBasis spans), which are useful on their own.

Namespace / staging

Declarations live in namespace Matrix (Mathlib's symbol namespace for the Kronecker product), so upstreaming is a file move onto Mathlib/RingTheory/MatrixAlgebra.lean (where kroneckerAlgEquiv lives), no symbol rename. Mathlib has none of these as of the pinned revision. MATHLIB-ABSENT(Matrix.kroneckerLeftAlgHom) MATHLIB-ABSENT(Matrix.kroneckerRightAlgHom)

Consumers

• CsdLean4/CV/CompositeArena.lean (leftHom / rightHom, composite_generate);
• CsdLean4/SigmaLayer/TensorTomography.lean (aliceHom / bobHom, kronecker_adjoin_eq_top).

Generation by matrix units

theorem Submodule.eq_top_of_forall_single_mem {R : Type u_1} [Semiring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] {p : Submodule R (Matrix m n R)} (h : ∀ (i : m) (j : n), Matrix.single i j 1 ∈ p) : p = ⊤

A submodule of a matrix module containing every matrix unit single i j 1 is everything.

theorem Subalgebra.eq_top_of_forall_single_mem {R : Type u_1} [CommSemiring R] {n : Type u_2} [Fintype n] [DecidableEq n] {S : Subalgebra R (Matrix n n R)} (h : ∀ (i j : n), Matrix.single i j 1 ∈ S) : S = ⊤

A subalgebra of a matrix algebra containing every matrix unit single i j 1 is everything.

The factor embeddings

noncomputable def Matrix.kroneckerLeftAlgHom (R : Type u_1) [CommSemiring R] (m : Type u_2) (n : Type u_3) [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : Matrix m m R →ₐ[R] Matrix (m × n) (m × n) R

The left Kronecker factor embedding A ↦ A ⊗ₖ 1 as an R-algebra homomorphism.

Equations

• Matrix.kroneckerLeftAlgHom R m n = (↑(Matrix.kroneckerAlgEquiv m n R)).comp Algebra.TensorProduct.includeLeft

noncomputable def Matrix.kroneckerRightAlgHom (R : Type u_1) [CommSemiring R] (m : Type u_2) (n : Type u_3) [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : Matrix n n R →ₐ[R] Matrix (m × n) (m × n) R

The right Kronecker factor embedding B ↦ 1 ⊗ₖ B as an R-algebra homomorphism.

Equations

• Matrix.kroneckerRightAlgHom R m n = (↑(Matrix.kroneckerAlgEquiv m n R)).comp Algebra.TensorProduct.includeRight

@[simp]

theorem Matrix.kroneckerLeftAlgHom_apply {R : Type u_1} [CommSemiring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m R) : (kroneckerLeftAlgHom R m n) A = kroneckerMap (fun (x1 x2 : R) => x1 * x2) A 1

@[simp]

theorem Matrix.kroneckerRightAlgHom_apply {R : Type u_1} [CommSemiring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (B : Matrix n n R) : (kroneckerRightAlgHom R m n) B = kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 B

theorem Matrix.kroneckerLeftAlgHom_mul_kroneckerRightAlgHom {R : Type u_1} [CommSemiring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m R) (B : Matrix n n R) : (kroneckerLeftAlgHom R m n) A * (kroneckerRightAlgHom R m n) B = kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B

The product of the two embeddings is the Kronecker product.

theorem Matrix.commute_kroneckerLeftAlgHom_kroneckerRightAlgHom {R : Type u_1} [CommSemiring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m R) (B : Matrix n n R) : Commute ((kroneckerLeftAlgHom R m n) A) ((kroneckerRightAlgHom R m n) B)

The two factor embeddings commute.

theorem Matrix.kroneckerLeftAlgHom_conjTranspose {R : Type u_1} [CommSemiring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [StarRing R] (A : Matrix m m R) : (kroneckerLeftAlgHom R m n) A.conjTranspose = ((kroneckerLeftAlgHom R m n) A).conjTranspose

The left embedding preserves the conjugate transpose.

theorem Matrix.kroneckerRightAlgHom_conjTranspose {R : Type u_1} [CommSemiring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [StarRing R] (B : Matrix n n R) : (kroneckerRightAlgHom R m n) B.conjTranspose = ((kroneckerRightAlgHom R m n) B).conjTranspose

The right embedding preserves the conjugate transpose.

theorem Matrix.kroneckerLeftAlgHom_star {R : Type u_1} [CommSemiring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [StarRing R] (A : Matrix m m R) : (kroneckerLeftAlgHom R m n) (star A) = star ((kroneckerLeftAlgHom R m n) A)

The left embedding preserves star.

theorem Matrix.kroneckerRightAlgHom_star {R : Type u_1} [CommSemiring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [StarRing R] (B : Matrix n n R) : (kroneckerRightAlgHom R m n) (star B) = star ((kroneckerRightAlgHom R m n) B)

The right embedding preserves star.

theorem Matrix.single_eq_kroneckerLeftAlgHom_mul_kroneckerRightAlgHom {R : Type u_1} [CommSemiring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (i k : m) (j l : n) : single (i, j) (k, l) 1 = (kroneckerLeftAlgHom R m n) (single i k 1) * (kroneckerRightAlgHom R m n) (single j l 1)

Every matrix unit of the product index is a product of embedded matrix units.

theorem Matrix.adjoin_range_kroneckerLeftAlgHom_union_eq_top {R : Type u_1} [CommSemiring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : Algebra.adjoin R (Set.range ⇑(kroneckerLeftAlgHom R m n) ∪ Set.range ⇑(kroneckerRightAlgHom R m n)) = ⊤

The two factor embeddings generate the matrix algebra of the product index.