Inner automorphisms of a matrix algebra #

An invertible matrix g ∈ GL n R over a commutative ring acts on the matrix algebra Matrix n n R by the algebra automorphism x ↦ g x g⁻¹. This file packages that action as a group homomorphism GL n R →* (Matrix n n R ≃ₐ[R] Matrix n n R) and proves:

its kernel is the center of GL n R, the invertible scalar matrices;
over a field it is surjective: every automorphism of a matrix algebra is inner (Skolem–Noether);
hence it induces an injective homomorphism from Mathlib's projective general linear group PGL(n, R) = GL n R / Z(GL n R), which is bijective over a field.

These are the pointwise facts behind the identification of the projective general linear group scheme with the automorphism group scheme of the matrix algebra.

Main declarations #

Matrix.GeneralLinearGroup.innerAut: conjugation as algebra automorphisms.
Matrix.GeneralLinearGroup.ker_innerAut: its kernel is the center.
Matrix.GeneralLinearGroup.innerAut_surjective: surjectivity over a field.
Matrix.ProjGenLinGroup.innerAut: the induced homomorphism on PGL(n, R), with Matrix.ProjGenLinGroup.innerAut_injective and Matrix.ProjGenLinGroup.innerAut_bijective.

References #

R. S. Pierce, Associative Algebras, GTM 88, Chapter 12, for the Skolem–Noether theorem; the form used is TauCeti.exists_unit_conj_of_algEquiv.

source

noncomputable def Matrix.GeneralLinearGroup.innerAut {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] :

GL n R →* Matrix n n R ≃ₐ[R] Matrix n n R

Conjugation by an invertible matrix, x ↦ g x g⁻¹, as an algebra automorphism of the matrix algebra.

Equations

Matrix.GeneralLinearGroup.innerAut = (MulSemiringAction.toAlgAut (ConjAct (GL n R)) R (Matrix n n R)).comp ConjAct.toConjAct.toMonoidHom

Instances For

source

@[simp]

theorem Matrix.GeneralLinearGroup.innerAut_apply {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (g : GL n R) (x : Matrix n n R) :

(innerAut g) x = ↑g * x * (↑g)⁻¹

The inner automorphism by g sends x to g x g⁻¹.

source

theorem Matrix.GeneralLinearGroup.innerAut_eq_one_iff {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (g : GL n R) :

innerAut g = 1 ↔ g ∈ Subgroup.center (GL n R)

An inner automorphism of a matrix algebra is trivial exactly when the conjugating matrix is central, that is, an invertible scalar matrix.

source

@[simp]

theorem Matrix.GeneralLinearGroup.ker_innerAut {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] :

innerAut.ker = Subgroup.center (GL n R)

The kernel of conjugation is the center of the general linear group.

source

theorem Matrix.GeneralLinearGroup.innerAut_surjective {n : Type u_1} [Fintype n] [DecidableEq n] (K : Type u_3) [Field K] :

Function.Surjective ⇑innerAut

Skolem–Noether for matrix algebras: over a field, every algebra automorphism of a matrix algebra is inner.

source

noncomputable def Matrix.ProjGenLinGroup.innerAut {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] :

ProjGenLinGroup n R →* Matrix n n R ≃ₐ[R] Matrix n n R

Conjugation induces a homomorphism from the projective general linear group PGL(n, R) = GL n R / Z(GL n R) to the automorphism group of the matrix algebra.

Equations