Associative rings and algebras

Noncommutative rings and finite-dimensional associative algebras, including division and central simple algebras, quaternion algebras, polynomial identities, nil ideals and Hopf algebras. Group rings are under Group Theory.

TheoremAmitsur–Levitzki theorem#✓fully proved

Let \(R\) be a commutative ring and \(n\) a natural number. For all \(n \times n\) matrices \(M_1, \dots, M_{2n}\) over \(R\), the sum over all permutations \(\sigma\) of \(\{1, \dots, 2n\}\) of \(\mathrm{sgn}(\sigma) M_{\sigma(1)} M_{\sigma(2)} \cdots M_{\sigma(2n)}\) is the zero matrix, where \(\mathrm{sgn}(\sigma) \in \{1, -1\}\) is the sign of \(\sigma\). In other words, the standard polynomial of degree \(2n\) vanishes on \(n \times n\) matrices over \(R\).

theorem amitsur_levitzki
    {R : Type*} [CommRing R] (n : ℕ)
    (M : Fin (2 * n) → Matrix (Fin n) (Fin n) R) :
    ∑ σ : Equiv.Perm (Fin (2 * n)),
      (σ.sign : ℤ) • (List.ofFn fun i => M (σ i)).prod = 0
Sources
  • A. S. Amitsur and J. Levitzki, Minimal identities for algebras, Proc. Amer. Math. Soc. 1 (1950), 449-463, DOI 10.1090/S0002-9939-1950-0036751-9; textbook in Rowen, Polynomial Identities in Ring Theory.

TheoremBurnside's theorem on matrix algebras#✓fully proved

Let \(k\) be an algebraically closed field, \(n\) a natural number, and \(A\) a \(k\)-subalgebra of the algebra \(M_n(k)\) of \(n \times n\) matrices over \(k\). Suppose that the only subspaces \(W\) of \(k^n\) with \(Mv \in W\) for all \(M \in A\) and all \(v \in W\) are \(0\) and \(k^n\). Then \(A = M_n(k)\).

theorem burnside_matrix
    {k : Type*} [Field k] [IsAlgClosed k]
    {n : ℕ}
    (A : Subalgebra k (Matrix (Fin n) (Fin n) k))
    (h : ∀ W : Submodule k (Fin n → k),
      (∀ M ∈ A, ∀ v ∈ W, M.mulVec v ∈ W) → W = ⊥ ∨ W = ⊤) :
    A = ⊤
Sources
  • W. Burnside, On the condition of reducibility of any group of linear substitutions, Proc. London Math. Soc. 3 (1905), 430–434, DOI 10.1112/plms/s2-3.1.430; textbook in Lam, First Course in Noncommutative Rings, Thm 1.2. Burnside's theorem on matrix algebras / Burnside density.

TheoremFrobenius theorem on real division algebras#✓fully proved

Let \(A\) be a finite-dimensional associative unital division algebra over \(\mathbb{R}\). Then \(A\) is isomorphic as an \(\mathbb{R}\)-algebra to \(\mathbb{R}\), to \(\mathbb{C}\), or to the algebra \(\mathbb{H}\) of real quaternions.

theorem frobenius_real_division_algebra
    {A : Type*} [DivisionRing A] [Algebra ℝ A] [FiniteDimensional ℝ A] :
    Nonempty (A ≃ₐ[ℝ] ℝ) ∨ Nonempty (A ≃ₐ[ℝ] ℂ) ∨ Nonempty (A ≃ₐ[ℝ] Quaternion ℝ)
Sources
  • G. Frobenius, Ueber lineare Substitutionen und bilineare Formen, J. reine angew. Math. 84 (1878), 1–63, DOI 10.1515/crelle-1878-18788403; textbook in Jacobson, Basic Algebra II; Lean states associative unital case via DivisionRing excluding octonions intentionally.

TheoremSkolem–Noether theorem#✓fully proved

Let \(k\) be a field and let \(A\) be a finite-dimensional central simple algebra over \(k\). Then every \(k\)-algebra automorphism \(\sigma\) of \(A\) is inner: there is a unit \(u \in A^\times\) such that \(\sigma(x) = u x u^{-1}\) for all \(x \in A\).

theorem skolem_noether
    {k : Type*} {A : Type*} [Field k] [Ring A] [Algebra k A]
    [FiniteDimensional k A] [Algebra.IsCentral k A] [IsSimpleRing A]
    (σ : A ≃ₐ[k] A) : ∃ u : Aˣ, ∀ x : A, σ x = (u : A) * x * (↑(u⁻¹ : Aˣ) : A)
Sources
  • T. Skolem, Zur Theorie der assoziativen Zahlensysteme, Skrifter Vidensk. Kristiania I (1927), no. 12; E. Noether, Nichtkommutative Algebra, Math. Z. 37 (1933), 514-541, DOI 10.1007/BF01474591.
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.