Centralizers of simple subalgebras

A simple subalgebra B of a finite-dimensional central simple algebra A is its own double centralizer, even when B is not central over the base field. Its centralizer is simple, and the centers of B and its centralizer have the same image in A.

In particular, the center of the centralizer of a subfield is that subfield itself. This is the center identification needed to regard a centralizer as a central algebra over the subfield and enlarge separable subfields using the Jacobson–Noether theorem. No separability assumption on the subfield is needed for the centralizer statements here.

The simplicity and dimension count reuse the bimodule identification TauCeti.centralizerAlgEquivEnd and the tensor-product simplicity theorem with the central factor on the right. Applying the dimension count twice proves the double-centralizer equality.

References

R. S. Pierce, Associative Algebras, Chapter 12; P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.2.

@[simp]

theorem Subalgebra.centralizer_centralizer_of_isSimpleRing {K : Type u_1} {A : Type u_2} [Field K] [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (B : Subalgebra K A) [IsSimpleRing ↥B] : centralizer K (↑B).centralizer = B

A simple subalgebra of a finite-dimensional central simple algebra is its own double centralizer. In particular, this applies to subfields larger than the base field.

theorem Subalgebra.map_center_centralizer_val {K : Type u_1} {A : Type u_2} [Field K] [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (B : Subalgebra K A) [IsSimpleRing ↥B] : map (centralizer K ↑B).val (center K ↥(centralizer K ↑B)) = map B.val (center K ↥B)

The centers of a simple subalgebra and its centralizer have the same image in the ambient central simple algebra. The centralizer need not be central over the base field.

theorem Subalgebra.isCentral_centralizer {K : Type u_1} {A : Type u_2} [Field K] [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (B : Subalgebra K A) [IsSimpleRing ↥B] [IsMulCommutative ↥B] : Algebra.IsCentral ↥B ↥(centralizer K ↑B)

The centralizer of a commutative simple subalgebra is central over that subalgebra, with its canonical action by inclusion. In particular, this applies to subfields.