Conjugation invariants in the general linear group

This file records elementary invariants of conjugation in a general linear group that are useful across the concrete subgroup and conjugacy-class computations, and the fact that conjugation by an element of GL n R determines that element up to a unit scalar. The latter is what makes the conjugators of a family of inner automorphisms of Mₙ(R) multiply up to scalars, as in the construction of the Galois 2-cocycle of a split central simple algebra.

Main results

• Matrix.GeneralLinearGroup.det_sub_algebraMap_conj: shifting a matrix by a scalar and taking its determinant is invariant under conjugation.
• Matrix.GeneralLinearGroup.exists_scalar_mul_eq_of_forall_conj_eq: two elements of GL n R inducing the same conjugation of GL n R differ by a unit scalar.
• Matrix.GeneralLinearGroup.scalar_injective: for nonempty n, the scalar embedding Rˣ → GL n R is injective.

theorem Matrix.GeneralLinearGroup.scalar_injective {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [Nonempty n] : Function.Injective ⇑(scalar n)

For nonempty n, the scalar embedding Rˣ → GL n R is injective.

theorem Matrix.GeneralLinearGroup.det_sub_algebraMap_conj {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (g x : GL n R) (a : R) : (↑(x⁻¹ * g * x) - (algebraMap R (Matrix n n R)) a).det = (↑g - (algebraMap R (Matrix n n R)) a).det

Shifting a matrix by a scalar and taking its determinant is invariant under conjugation in the general linear group.

theorem Matrix.GeneralLinearGroup.exists_scalar_mul_eq_of_forall_conj_eq {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {g h : GL n R} (H : ∀ (x : GL n R), g * x * g⁻¹ = h * x * h⁻¹) : ∃ (u : Rˣ), (scalar n) u * h = g

An inner automorphism determines its conjugator up to a scalar. If g and h in GL n R conjugate every element of GL n R in the same way, then g is h multiplied by the scalar matrix of a unit u.