LeanPool.BrauerGroupNew.MatrixCenterEquiv

Imported Lean Pool material for LeanPool.BrauerGroupNew.MatrixCenterEquiv.

theorem Matrix.mem_center_iff (R : Type u_1) [Ring R] (n : ℕ) (M : Matrix (Fin n) (Fin n) R) : M ∈ Subring.center (Matrix (Fin n) (Fin n) R) ↔ ∃ (α : ↥(Subring.center R)), M = α • 1

def Matrix.centerEquivBase (n : ℕ) (hn : 0 < n) (R : Type u_1) [Ring R] : ↥(Subring.center (Matrix (Fin n) (Fin n) R)) ≃+* ↥(Subring.center R)

The center of a nonempty square matrix ring is ring-equivalent to the center of the base ring.

Equations

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

def Matrix.centerAlgEquiv (R A : Type u) [CommSemiring R] [Ring A] [Algebra R A] (n : ℕ) (hn : 0 < n) : ↥(Subalgebra.center R (Matrix (Fin n) (Fin n) A)) ≃ₐ[R] ↥(Subalgebra.center R A)

The center of a nonempty matrix algebra is algebra-equivalent to the center of the algebra.

Equations

• Matrix.centerAlgEquiv R A n hn = { toEquiv := (Matrix.centerEquivBase n hn A).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }