Centrality descends from a matrix algebra to its coefficients

Mathlib proves that a matrix algebra over a central algebra is central (Algebra.IsCentral.matrix). This file supplies the converse over a nonempty finite index type: the centre of Matrix ι ι D is the image of the centre of D under the scalar embedding Matrix.scalarAlgHom, which is injective as soon as ι is nonempty, so the centre of D is ⊥ whenever the centre of Matrix ι ι D is.

• TauCeti.isCentral_of_isCentral_matrix: if Matrix ι ι D is central over K, then so is D;
• TauCeti.isCentral_matrix_iff packages this with Mathlib's converse.

Implementation notes

TauCeti.isCentral_of_isCentral_matrix is deliberately not an instance: its hypothesis mentions Matrix ι ι D while its conclusion mentions only D, so instance search could not run it backwards, and the index type ι is unconstrained by the goal.

theorem TauCeti.isCentral_of_isCentral_matrix (K : Type u_1) (D : Type u_2) [CommSemiring K] [Semiring D] [Algebra K D] (ι : Type u_3) [Fintype ι] [DecidableEq ι] [Nonempty ι] [Algebra.IsCentral K (Matrix ι ι D)] : Algebra.IsCentral K D

If a matrix algebra Matrix ι ι D over a nonempty finite index type is central over K, then its coefficient algebra D is central over K.

The centre of Matrix ι ι D is the image of the centre of D under the scalar embedding Matrix.scalarAlgHom, which is injective because ι is nonempty; so the centre of D is ⊥ as soon as the centre of the matrix algebra is. This is the converse of Algebra.IsCentral.matrix.

@[simp]

theorem TauCeti.isCentral_matrix_iff (K : Type u_1) (D : Type u_2) [CommSemiring K] [Semiring D] [Algebra K D] (ι : Type u_3) [Fintype ι] [DecidableEq ι] [Nonempty ι] : Algebra.IsCentral K (Matrix ι ι D) ↔ Algebra.IsCentral K D

A matrix algebra over a nonempty finite index type is central exactly when its coefficient algebra is.