Base change of a matrix algebra

Extending scalars along an algebra map R → S of commutative semirings turns matrices over R into matrices over S, entrywise: TauCeti.Algebra.matrixBaseChangeAlgEquiv : S ⊗[R] Matrix n n R ≃ₐ[S] Matrix n n S.

Mathlib's matrixEquivTensor is this isomorphism read as an R-algebra isomorphism; the content here is that it is S-linear, which is the form base change is used in. Mathlib's Kronecker version Matrix.kroneckerTMulAlgEquiv is the two-sided statement and does not specialize to this one without reindexing.

Both directions are characterized on generators by the simp lemmas TauCeti.Algebra.matrixBaseChangeAlgEquiv_tmul and TauCeti.Algebra.matrixBaseChangeAlgEquiv_symm_single, so the definition need never be unfolded.

The same statement with an arbitrary, possibly noncommutative, coefficient algebra A in place of R is TauCeti.Algebra.matrixCoeffBaseChangeAlgEquiv: S ⊗[R] Matrix n n A ≃ₐ[S] Matrix n n (S ⊗[R] A). It is not a generalization of the first equivalence, whose target Matrix n n S is Matrix n n (S ⊗[R] R) only up to Algebra.TensorProduct.rid; and it is the first equivalence, applied to the scalar matrices, that makes the second one go through.

def TauCeti.Algebra.matrixBaseChangeAlgEquiv (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (n : Type u_3) [Fintype n] [DecidableEq n] : TensorProduct R S (Matrix n n R) ≃ₐ[S] Matrix n n S

Extending scalars turns matrices over R into matrices over S: S ⊗[R] Matrix n n R ≃ₐ[S] Matrix n n S, entrywise.

Mathlib's matrixEquivTensor is this isomorphism read as an R-algebra isomorphism; the content here is that it is S-linear.

Equations

• TauCeti.Algebra.matrixBaseChangeAlgEquiv R S n = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem TauCeti.Algebra.matrixBaseChangeAlgEquiv_tmul (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (n : Type u_3) [Fintype n] [DecidableEq n] (s : S) (M : Matrix n n R) : (matrixBaseChangeAlgEquiv R S n) (s ⊗ₜ[R] M) = s • M.map ⇑(algebraMap R S)

@[simp]

theorem TauCeti.Algebra.matrixBaseChangeAlgEquiv_symm_single (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (n : Type u_3) [Fintype n] [DecidableEq n] (i j : n) (x : S) : (matrixBaseChangeAlgEquiv R S n).symm (Matrix.single i j x) = x ⊗ₜ[R] Matrix.single i j 1

def TauCeti.Algebra.matrixCoeffBaseChangeAlgEquiv (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (n : Type u_3) [Fintype n] [DecidableEq n] (A : Type u_4) [Semiring A] [Algebra R A] : TensorProduct R S (Matrix n n A) ≃ₐ[S] Matrix n n (TensorProduct R S A)

Base change commutes with forming a matrix algebra: S ⊗[R] Matrix n n A ≃ₐ[S] Matrix n n (S ⊗[R] A), entrywise, for an arbitrary and possibly noncommutative coefficient algebra A.

The four steps are Mathlib's matrixEquivTensor, splitting off the scalar matrices as Matrix n n A ≃ₐ[R] A ⊗[R] Matrix n n R; the distributivity TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv of base change over ⊗; TauCeti.Algebra.matrixBaseChangeAlgEquiv on the scalar factor; and matrixEquivTensor again, backwards, over S.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Algebra.matrixCoeffBaseChangeAlgEquiv_tmul_apply (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (n : Type u_3) [Fintype n] [DecidableEq n] (A : Type u_4) [Semiring A] [Algebra R A] (s : S) (M : Matrix n n A) (i j : n) : (matrixCoeffBaseChangeAlgEquiv R S n A) (s ⊗ₜ[R] M) i j = s ⊗ₜ[R] M i j

@[simp]

theorem TauCeti.Algebra.matrixCoeffBaseChangeAlgEquiv_symm_single (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (n : Type u_3) [Fintype n] [DecidableEq n] (A : Type u_4) [Semiring A] [Algebra R A] (i j : n) (s : S) (a : A) : (matrixCoeffBaseChangeAlgEquiv R S n A).symm (Matrix.single i j (s ⊗ₜ[R] a)) = s ⊗ₜ[R] Matrix.single i j a