Matrix subalgebras

In this file we define the subalgebra of square matrices with entries in some subalgebra.

Main definitions

• Subalgebra.matrix: the subalgebra of square matrices with entries in some subalgebra.

def Subalgebra.matrix {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {n : Type u_3} [Fintype n] [DecidableEq n] (S : Subalgebra R A) : Subalgebra R (Matrix n n A)

A version of Set.matrix for Subalgebras. Given a Subalgebra S, S.matrix is the Subalgebra of square matrices m all of whose entries m i j belong to S.

Equations

• S.matrix = { toSubsemiring := S.matrix, algebraMap_mem' := ⋯ }

@[simp]

theorem Subalgebra.coe_matrix {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {n : Type u_3} [Fintype n] [DecidableEq n] (S : Subalgebra R A) : ↑S.matrix = S.toAddSubmonoid.matrix.carrier