The normalizer of the diagonal torus of the special linear group

The diagonal torus of SL_n(k) is the group of determinant-one diagonal matrices, the preimage of the diagonal torus of GL_n(k). When this torus separates every pair of coordinates, its normalizer in SL_n(k) consists of the determinant-one monomial matrices, and the normalizer quotient is the symmetric group on the coordinate lines, exactly as for GL_n(k).

The separation hypothesis cannot simply be dropped. Over 𝔽₃ the torus of SL₂ is the central subgroup {±1}, so its normalizer is all of SL₂(𝔽₃) and the normalizer quotient has order twelve rather than two; over 𝔽₂ the torus is trivial. In dimensions at least three, however, the determinant-one torus over 𝔽₃ does separate coordinates, so the natural separation hypothesis retains that valid case.

This is the group-of-points computation of the Weyl group of the standard split maximal torus of SL_n. It reduces to the GL_n computation of TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Diagonal.Normalizer: a normalizer element in SL_n(k) normalizes the diagonal torus of GL_n(k), and its coordinate permutation is read off there.

Main declarations

• Matrix.SpecialLinearGroup.diagonalTorus: the diagonal torus of SL_n(k).
• Matrix.SpecialLinearGroup.DiagonalTorusSeparatesCoordinates: the coordinate-separation hypothesis used by the normalizer computation.
• Matrix.SpecialLinearGroup.mem_normalizer_diagonalTorus_iff_toGL_mem: an element of SL_n(k) normalizes its diagonal torus exactly when it normalizes the diagonal torus of GL_n(k).
• Matrix.SpecialLinearGroup.diagonalNormalizerPerm: the coordinate permutation of a normalizer element.
• Matrix.SpecialLinearGroup.diagonalNormalizerPerm_eq_one_iff: its kernel is the torus.
• Matrix.SpecialLinearGroup.diagonalNormalizerPerm_surjective: every permutation arises.
• Matrix.SpecialLinearGroup.diagonalNormalizerQuotientMulEquivPerm: the normalizer quotient is the symmetric group.

References

• J. S. Milne, Algebraic Groups (2017), Example 21.2 and Section 21.1.
• J. E. Humphreys, Linear Algebraic Groups (1975), Section 26.3.

theorem Matrix.SpecialLinearGroup.mem_normalizer_diagonalTorus_of_toGL_mem {k : Type u} {n : ℕ} [CommRing k] {g : SpecialLinearGroup (Fin n) k} (hg : toGL g ∈ Subgroup.normalizer ↑(TauCeti.diagonalTorus k n)) : g ∈ Subgroup.normalizer ↑(diagonalTorus k n)

An element of SL_n(k) normalizing the diagonal torus of GL_n(k) normalizes the diagonal torus of SL_n(k).

def Matrix.SpecialLinearGroup.DiagonalTorusSeparatesCoordinates (k : Type u) [Field k] (n : ℕ) : Prop

The determinant-one diagonal torus separates coordinates if each pair of distinct coordinates receives different values under some diagonal element of determinant one.

Equations

• Matrix.SpecialLinearGroup.DiagonalTorusSeparatesCoordinates k n = ∀ (i j : Fin n), i ≠ j → ∃ (t : Fin n → kˣ), ∏ r : Fin n, ↑(t r) = 1 ∧ t i ≠ t j

theorem Matrix.SpecialLinearGroup.diagonalTorusSeparatesCoordinates_of_exists_sq_ne_one {k : Type u} {n : ℕ} [Field k] (hk : ∃ (a : kˣ), a ^ 2 ≠ 1) : DiagonalTorusSeparatesCoordinates k n

A unit whose square is not one makes the determinant-one diagonal torus separate coordinates.

theorem Matrix.SpecialLinearGroup.mem_normalizer_diagonalTorus_iff_toGL_mem {k : Type u} {n : ℕ} [Field k] (hsep : DiagonalTorusSeparatesCoordinates k n) {g : SpecialLinearGroup (Fin n) k} : g ∈ Subgroup.normalizer ↑(diagonalTorus k n) ↔ toGL g ∈ Subgroup.normalizer ↑(TauCeti.diagonalTorus k n)

When the determinant-one diagonal torus separates coordinates, an element of SL_n(k) normalizes it exactly when it normalizes the diagonal torus of GL_n(k), that is, exactly when it is a monomial matrix.

theorem Matrix.SpecialLinearGroup.DiagonalTorusSeparatesCoordinates.nontrivial_of_not_subsingleton {k : Type u} {n : ℕ} [Field k] (hsep : DiagonalTorusSeparatesCoordinates k n) (hn : ¬Subsingleton (Fin n)) : Nontrivial kˣ

Coordinate separation implies that the unit group is nontrivial when there are at least two coordinates.

noncomputable def Matrix.SpecialLinearGroup.diagonalNormalizerPerm {k : Type u} {n : ℕ} [Field k] (hsep : DiagonalTorusSeparatesCoordinates k n) : ↥(Subgroup.normalizer ↑(diagonalTorus k n)) →* Equiv.Perm (Fin n)

The permutation of coordinate lines induced by an element of SL_n(k) normalizing its diagonal torus. It is the coordinate permutation of the same matrix in GL_n(k).

Equations

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

theorem Matrix.SpecialLinearGroup.diagonalNormalizerPerm_apply {k : Type u} {n : ℕ} [Field k] (hsep : DiagonalTorusSeparatesCoordinates k n) (hn : ¬Subsingleton (Fin n)) (g : ↥(Subgroup.normalizer ↑(diagonalTorus k n))) : (diagonalNormalizerPerm hsep) g = have x := ⋯; TauCeti.diagonalNormalizerPerm ⟨toGL ↑g, ⋯⟩

The coordinate permutation of a normalizer element of SL_n(k) is the coordinate permutation of the same matrix in GL_n(k).

@[simp]

theorem Matrix.SpecialLinearGroup.diagonalNormalizerPerm_apply_of_subsingleton {k : Type u} {n : ℕ} [Field k] (hsep : DiagonalTorusSeparatesCoordinates k n) [Subsingleton (Fin n)] (g : ↥(Subgroup.normalizer ↑(diagonalTorus k n))) : (diagonalNormalizerPerm hsep) g = 1

There is only the trivial coordinate permutation when the coordinate type is a subsingleton.

theorem Matrix.SpecialLinearGroup.diagonalNormalizerPerm_eq_one_iff {k : Type u} {n : ℕ} [Field k] (hsep : DiagonalTorusSeparatesCoordinates k n) (g : ↥(Subgroup.normalizer ↑(diagonalTorus k n))) : (diagonalNormalizerPerm hsep) g = 1 ↔ ↑g ∈ diagonalTorus k n

The coordinate permutation of a normalizer element of the diagonal torus of SL_n(k) is trivial exactly for elements of the torus.

theorem Matrix.SpecialLinearGroup.diagonalNormalizerPerm_surjective {k : Type u} {n : ℕ} [Field k] (hsep : DiagonalTorusSeparatesCoordinates k n) : Function.Surjective ⇑(diagonalNormalizerPerm hsep)

Every permutation of the coordinate lines is induced by an element of SL_n(k) normalizing the diagonal torus: a permutation matrix with a sign correcting its determinant.

noncomputable def Matrix.SpecialLinearGroup.diagonalNormalizerQuotientMulEquivPerm {k : Type u} {n : ℕ} [Field k] (hsep : DiagonalTorusSeparatesCoordinates k n) : (diagonalTorus k n).normalizerQuotient ≃* Equiv.Perm (Fin n)

The Weyl group of the diagonal torus of SL_n(k): when the determinant-one diagonal torus separates coordinates, its normalizer modulo the torus is canonically the symmetric group on the coordinate lines.

Equations

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

@[simp]

theorem Matrix.SpecialLinearGroup.diagonalNormalizerQuotientMulEquivPerm_mk {k : Type u} {n : ℕ} [Field k] (hsep : DiagonalTorusSeparatesCoordinates k n) (g : ↥(Subgroup.normalizer ↑(diagonalTorus k n))) : (diagonalNormalizerQuotientMulEquivPerm hsep) ↑g = (diagonalNormalizerPerm hsep) g

The quotient equivalence sends the class of a normalizer element to its coordinate permutation.