The normalizer of the diagonal torus

Over a field with at least two units, an invertible matrix normalizes the diagonal torus exactly when it is monomial: it is a diagonal matrix followed by a permutation matrix. The permutation is unique, and multiplication of monomial matrices multiplies these permutations. Consequently the quotient of the normalizer by the diagonal torus is canonically the symmetric group.

This is the group-of-points calculation behind the Weyl group of the diagonal maximal torus in GL_n. It complements TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup, which identifies the Weyl group of the corresponding coordinate root datum with the same permutation group.

Main declarations

• TauCeti.permutationGL: the permutation-matrix embedding in GL.
• TauCeti.coe_permutationGL_inv_mul_mul_permutationGL_apply: conjugation by a permutation matrix relabels both matrix indices.
• TauCeti.diagGL_mul_permutationGL: moving a permutation matrix past a diagonal one relabels the diagonal entries.
• TauCeti.exists_eq_diagGL_mul_permutationGL_of_forall_ne: an invertible matrix whose conjugation keeps a coordinate-separating family of diagonal matrices diagonal is monomial.
• TauCeti.mem_normalizer_diagonalTorus_iff_exists: normalizing matrices are precisely products of a diagonal matrix and a permutation matrix.
• TauCeti.diagonalNormalizerPerm: the permutation homomorphism from the normalizer.
• TauCeti.diagonalNormalizer_mul_diagGL_mul_inv: conjugation by a normalizer element relabels diagonal coordinates by its coordinate permutation.
• TauCeti.diagonalNormalizerQuotientMulEquivPerm: the normalizer quotient is the symmetric group.

References

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

This advances Layer 7, "Borel subgroups, maximal tori" and "Root datum (G, T)", of the ReductiveGroups roadmap through the standard split maximal torus of GL_n.

def TauCeti.permutationGL {k : Type u} [Semiring k] {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Equiv.Perm ι →* GL ι k

A permutation as an invertible matrix. The inverse in the matrix entry is what makes this a homomorphism with Mathlib's convention for multiplication in Equiv.Perm.

Equations

• TauCeti.permutationGL = Matrix.permMatrixHom.toHomUnits

@[simp]

theorem TauCeti.permutationGL_coe {k : Type u} [Semiring k] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) : ↑(permutationGL σ) = Equiv.Perm.permMatrix k σ⁻¹

The matrix underlying permutationGL σ is the permutation matrix of σ⁻¹.

@[simp]

theorem TauCeti.coe_mul_permutationGL_apply {k : Type u} [Semiring k] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : GL ι k) (σ : Equiv.Perm ι) (i j : ι) : ↑(g * permutationGL σ) i j = ↑g i (σ j)

Right multiplication by permutationGL σ permutes the columns: the (i, j) entry of g * permutationGL σ is the (i, σ j) entry of g.

theorem TauCeti.coe_permutationGL_inv_mul_mul_permutationGL_apply {k : Type u} [Semiring k] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) (g : GL ι k) (i j : ι) : ↑((permutationGL σ)⁻¹ * g * permutationGL σ) i j = ↑g (σ i) (σ j)

Conjugation by permutationGL σ relabels both indices: the (i, j) entry of (permutationGL σ)⁻¹ * g * permutationGL σ is the (σ i, σ j) entry of g.

@[simp]

theorem TauCeti.permutationGL_mul_diagGL_mul_inv {k : Type u} {n : ℕ} [Semiring k] (σ : Equiv.Perm (Fin n)) (t : Fin n → kˣ) : permutationGL σ * diagGL t * (permutationGL σ)⁻¹ = diagGL fun (i : Fin n) => t (σ⁻¹ i)

Conjugating a diagonal matrix by a permutation matrix relabels its diagonal entries.

theorem TauCeti.diagGL_mul_permutationGL {k : Type u} {n : ℕ} [Semiring k] (σ : Equiv.Perm (Fin n)) (t : Fin n → kˣ) : diagGL t * permutationGL σ = permutationGL σ * diagGL fun (i : Fin n) => t (σ i)

Moving a permutation matrix past a diagonal one relabels the diagonal entries.

theorem TauCeti.permutationGL_mem_normalizer {k : Type u} {n : ℕ} [Semiring k] (σ : Equiv.Perm (Fin n)) : permutationGL σ ∈ Subgroup.normalizer ↑(diagonalTorus k n)

Permutation matrices normalize the diagonal torus.

theorem TauCeti.exists_eq_diagGL_mul_permutationGL_of_forall_ne {k : Type u} {n : ℕ} [Field k] {g : GL (Fin n) k} (hsep : ∀ (i j : Fin n), i ≠ j → ∃ (t : Fin n → kˣ), g * diagGL t * g⁻¹ ∈ diagonalTorus k n ∧ t i ≠ t j) : ∃ (d : Fin n → kˣ) (σ : Equiv.Perm (Fin n)), g = diagGL d * permutationGL σ

An invertible matrix is monomial, a diagonal matrix followed by a permutation matrix, as soon as conjugation by it keeps enough diagonal matrices diagonal to tell every two coordinates apart.

theorem TauCeti.mem_normalizer_diagonalTorus_iff_exists {k : Type u} {n : ℕ} [Field k] [Nontrivial kˣ] {g : GL (Fin n) k} : g ∈ Subgroup.normalizer ↑(diagonalTorus k n) ↔ ∃ (d : Fin n → kˣ) (σ : Equiv.Perm (Fin n)), g = diagGL d * permutationGL σ

An invertible matrix normalizes the diagonal torus exactly when it is a diagonal matrix followed by a permutation matrix.

noncomputable def TauCeti.diagonalNormalizerPerm {k : Type u} {n : ℕ} [Field k] [Nontrivial kˣ] : ↥(Subgroup.normalizer ↑(diagonalTorus k n)) →* Equiv.Perm (Fin n)

The permutation of coordinate lines induced by a matrix normalizing the diagonal torus.

Equations

• TauCeti.diagonalNormalizerPerm = { toFun := TauCeti.diagonalNormalizerPermFun✝, map_one' := ⋯, map_mul' := ⋯ }

theorem TauCeti.diagonalNormalizerPerm_eq_of_eq_diagGL_mul_permutationGL {k : Type u} {n : ℕ} [Field k] [Nontrivial kˣ] (g : ↥(Subgroup.normalizer ↑(diagonalTorus k n))) (d : Fin n → kˣ) (σ : Equiv.Perm (Fin n)) (h : ↑g = diagGL d * permutationGL σ) : diagonalNormalizerPerm g = σ

A monomial factorization of a diagonal-normalizer element has the coordinate permutation selected by diagonalNormalizerPerm.

@[simp]

theorem TauCeti.diagonalNormalizerPerm_permutationGL {k : Type u} {n : ℕ} [Field k] [Nontrivial kˣ] (σ : Equiv.Perm (Fin n)) : diagonalNormalizerPerm ⟨permutationGL σ, ⋯⟩ = σ

The coordinate permutation induced by a permutation matrix is the original permutation.

@[simp]

theorem TauCeti.diagonalNormalizer_mul_diagGL_mul_inv {k : Type u} {n : ℕ} [Field k] [Nontrivial kˣ] (g : ↥(Subgroup.normalizer ↑(diagonalTorus k n))) (t : Fin n → kˣ) : ↑g * diagGL t * (↑g)⁻¹ = diagGL fun (i : Fin n) => t ((Equiv.symm (diagonalNormalizerPerm g)) i)

Conjugation by a diagonal-normalizer element relabels the diagonal entries by its coordinate permutation: the entry at i becomes the original entry at the inverse image of i.

theorem TauCeti.diagonalNormalizerPerm_surjective {k : Type u} {n : ℕ} [Field k] [Nontrivial kˣ] : Function.Surjective ⇑diagonalNormalizerPerm

Every coordinate permutation is induced by a permutation matrix in the normalizer.

@[simp]

theorem TauCeti.diagonalNormalizerPerm_eq_one_iff {k : Type u} {n : ℕ} [Field k] [Nontrivial kˣ] (g : ↥(Subgroup.normalizer ↑(diagonalTorus k n))) : diagonalNormalizerPerm g = 1 ↔ ↑g ∈ diagonalTorus k n

The coordinate permutation induced by a normalizer element is trivial exactly for elements of the diagonal torus.

noncomputable def TauCeti.diagonalNormalizerQuotientMulEquivPerm {k : Type u} {n : ℕ} [Field k] [Nontrivial kˣ] : (diagonalTorus k n).normalizerQuotient ≃* Equiv.Perm (Fin n)

The normalizer of the diagonal torus modulo the torus is canonically the symmetric group.

Equations

• TauCeti.diagonalNormalizerQuotientMulEquivPerm = MulEquiv.ofBijective ((TauCeti.diagonalTorus k n).normalizerQuotientLift TauCeti.diagonalNormalizerPerm ⋯) ⋯

@[simp]

theorem TauCeti.diagonalNormalizerQuotientMulEquivPerm_mk {k : Type u} {n : ℕ} [Field k] [Nontrivial kˣ] (g : ↥(Subgroup.normalizer ↑(diagonalTorus k n))) : diagonalNormalizerQuotientMulEquivPerm ↑g = diagonalNormalizerPerm g

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

@[simp]

theorem TauCeti.diagonalNormalizerQuotientMulEquivPerm_symm_apply {k : Type u} {n : ℕ} [Field k] [Nontrivial kˣ] (σ : Equiv.Perm (Fin n)) : diagonalNormalizerQuotientMulEquivPerm.symm σ = (diagonalTorus k n).normalizerQuotientMk ⟨permutationGL σ, ⋯⟩

The inverse quotient equivalence sends a coordinate permutation to the class of its permutation matrix.