The diagonal normalizer and the Bruhat data of GL₂

This file aligns upper-triangular Bruhat data with the diagonal normalizer. For GLₙ, an upper-triangular monomial matrix is diagonal, and hence

Bₙ ⊓ N(Tₙ) = Tₙ.

Specializing to GL₂, the Weyl element used in the Bruhat decomposition is the permutation matrix of the transposition, so it lies in N(T) and induces the nontrivial element of its permutation quotient. In particular,

B ⊓ N(T) = T,

where B is the standard Borel subgroup. This is the kernel identification in the rank-one (B, N)-pair: the already-established quotient N(T) / T ≃ S₂ can equivalently be written with B ⊓ N(T) as its denominator.

The assumption Nontrivial kˣ in the intersection theorems is necessary for the full group-theoretic normalizer. For example, over 𝔽₂ the diagonal torus of GL₂ is trivial, so its normalizer is all of GL₂ and the displayed rank-one intersection would instead be B.

Main results

• TauCeti.gl2WeylElement_eq_permutationGL_swap: the Bruhat Weyl element is the permutation matrix of the transposition.
• TauCeti.gl2WeylElement_mem_normalizer_diagonalTorus: the Weyl element normalizes the diagonal torus.
• TauCeti.diagonalNormalizerPerm_gl2WeylElement: the Weyl element induces the transposition on the coordinate lines.
• TauCeti.UpperTriangularGroup.inf_normalizer_diagonalTorus_eq: in every dimension, the intersection of the upper-triangular subgroup with the diagonal normalizer is the diagonal torus.
• TauCeti.UpperTriangularGroup.permutationGL_inv_mul_mul_permutationGL_mem_iff: when a conjugate by a permutation matrix is upper triangular.
• TauCeti.closure_upperTriangularGroup_union_range_permutationGL: the upper-triangular subgroup and permutation matrices generate GLₘ(k).
• TauCeti.exists_mem_doubleCoset_permutationGL: the Bruhat decomposition of GLₘ(k) over any field, every element lies in B τ B for a permutation τ.

References

• J. E. Humphreys, Linear Algebraic Groups (1975), Sections 26.2–26.3 and 28.1.
• T. A. Springer, Linear Algebraic Groups, second edition (1998), Sections 8.3–8.4.

This advances Layer 7, "Bruhat decomposition and BN-pairs / Tits systems", of the ReductiveGroups roadmap by identifying the intersection subgroup, including in the rank-one GL₂ example.

theorem TauCeti.gl2WeylElement_eq_permutationGL_swap (R : Type u) [Semiring R] : GL2WeylElement R = permutationGL (Equiv.swap 0 1)

The Weyl element in the Bruhat decomposition of GL₂ is the permutation matrix of the transposition of the two coordinate lines.

theorem TauCeti.gl2WeylElement_mem_normalizer_diagonalTorus (R : Type u) [Semiring R] : GL2WeylElement R ∈ Subgroup.normalizer ↑(diagonalTorus R 2)

The Bruhat Weyl element normalizes the diagonal torus.

theorem TauCeti.diagonalNormalizerPerm_gl2WeylElement {k : Type u} [Field k] [Nontrivial kˣ] : diagonalNormalizerPerm ⟨GL2WeylElement k, ⋯⟩ = Equiv.swap 0 1

The coordinate permutation induced by the Bruhat Weyl element is the transposition.

theorem TauCeti.UpperTriangularGroup.diagonalTorus_le {R : Type u} [CommRing R] {n : ℕ} : diagonalTorus R n ≤ upperTriangularGroup (Fin n) R

Every diagonal matrix is upper triangular, so the diagonal torus lies in the standard upper-triangular subgroup.

theorem TauCeti.UpperTriangularGroup.permutationGL_inv_mul_mul_permutationGL_mem_iff {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] [LinearOrder ι] (σ : Equiv.Perm ι) (g : GL ι R) : (permutationGL σ)⁻¹ * g * permutationGL σ ∈ upperTriangularGroup ι R ↔ ∀ ⦃i j : ι⦄, j < i → ↑g (σ i) (σ j) = 0

Conjugating by the permutation matrix of σ gives an upper-triangular matrix exactly when the entries of g at (σ i, σ j) vanish for all j < i.

theorem TauCeti.UpperTriangularGroup.mem_diagonalTorus_of_mem {k : Type u} [Field k] [Nontrivial kˣ] {n : ℕ} (g : ↥(Subgroup.normalizer ↑(diagonalTorus k n))) (hg : ↑g ∈ upperTriangularGroup (Fin n) k) : ↑g ∈ diagonalTorus k n

A diagonal-normalizer element that is upper triangular is diagonal. Equivalently, an upper-triangular monomial matrix cannot carry a nontrivial coordinate permutation.

theorem TauCeti.UpperTriangularGroup.inf_normalizer_diagonalTorus_eq {k : Type u} [Field k] [Nontrivial kˣ] {n : ℕ} : upperTriangularGroup (Fin n) k ⊓ Subgroup.normalizer ↑(diagonalTorus k n) = diagonalTorus k n

Over a field with at least two units, the intersection of the upper-triangular subgroup of GLₙ with the normalizer of the diagonal torus is exactly the diagonal torus.

theorem TauCeti.permutationGL_swap_mul_mul_permutationGL_mem {k : Type u} [Field k] {m : ℕ} {a b : Fin m} (hab : ↑a + 1 = ↑b) {x : GL (Fin m) k} (hx : x ∈ upperTriangularGroup (Fin m) k) (τ : Equiv.Perm (Fin m)) : permutationGL (Equiv.swap a b) * x * permutationGL τ ∈ DoubleCoset.doubleCoset (permutationGL (Equiv.swap a b) * permutationGL τ) ↑(upperTriangularGroup (Fin m) k) ↑(upperTriangularGroup (Fin m) k) ∪ DoubleCoset.doubleCoset (permutationGL τ) ↑(upperTriangularGroup (Fin m) k) ↑(upperTriangularGroup (Fin m) k)

The Tits multiplication step for an adjacent transposition s: for x ∈ B and a permutation τ, the product s x τ lies in B s τ B ∪ B τ B.

theorem TauCeti.closure_upperTriangularGroup_union_range_permutationGL (k : Type u) [Field k] (m : ℕ) : Subgroup.closure (↑(upperTriangularGroup (Fin m) k) ∪ Set.range ⇑permutationGL) = ⊤

The upper-triangular subgroup and the permutation matrices generate GLₘ(k).

theorem TauCeti.exists_mem_doubleCoset_permutationGL {k : Type u} [Field k] {m : ℕ} (g : GL (Fin m) k) : ∃ (τ : Equiv.Perm (Fin m)), g ∈ DoubleCoset.doubleCoset (permutationGL τ) ↑(upperTriangularGroup (Fin m) k) ↑(upperTriangularGroup (Fin m) k)

Bruhat decomposition of GLₘ(k) over any field: every invertible matrix lies in a double coset B τ B of the upper-triangular subgroup represented by a permutation matrix.