The Bruhat decomposition of GL₂ #
The Bruhat decomposition of GL₂ says that the Borel subgroup B of invertible upper
triangular matrices has exactly two double cosets in GL₂: the group GL₂ is the disjoint union
of B itself and the big cell B w B, where w = !![0, 1; 1, 0] is the Weyl element. In the
Weyl-group language this is GL₂ = ⨆_{σ ∈ S₂} B σ B, the rank-one case of the general
decomposition.
Everything is cut out by a single matrix entry. The lower-left entry of b₁ w b₂, for
b₁ = !![a₁, c₁; 0, d₁] and b₂ = !![a₂, c₂; 0, d₂], is d₁ a₂, a product of two units; and
conversely, for an invertible g = !![a, b; c, d] whose lower-left entry c is a unit, the
column operation v = !![1, -d; 0, c] clears the lower-right entry of g and swapping the two
columns of g v then makes it upper triangular, so that
g = (g v w) * w * v⁻¹
exhibits g in the big cell. So membership in the big cell is exactly invertibility of the
lower-left entry
(TauCeti.GL2Borel.mem_doubleCoset_weyl_iff), while membership in B is exactly its vanishing
(TauCeti.GL2Borel.mem_iff). Over a commutative ring those two conditions need not exhaust GL₂,
so the decomposition itself is stated over a field, where a scalar is either zero or a unit; the
cell description and the factorization hold over any commutative ring.
The counting form TauCeti.GL2Borel.card_doubleCosetQuotient_eq_two is what the Mackey
irreducibility criterion TauCeti.simple_indFDRep_iff_doubleCoset consumes: the criterion
quantifies over B \ GL₂ / B and, with this file in hand, collapses to the single Mackey term at
the Weyl element.
Main definitions #
TauCeti.GL2WeylElement: the Weyl element!![0, 1; 1, 0]ofGL₂, the nontrivial permutation matrix.
Main results #
TauCeti.GL2Borel.mem_doubleCoset_weyl_iff: an element ofGL₂lies in the big cellB w Bexactly when its lower-left entry is a unit, andTauCeti.GL2Borel.doubleCoset_one_eq: the other cell, the identity double coset, isBitself.TauCeti.GL2Borel.union_doubleCoset_weyl_eq_univandTauCeti.GL2Borel.disjoint_doubleCoset_weyl: the Bruhat decomposition,GL₂ = B ⊔ B w Bover a field.TauCeti.GL2Borel.doubleCosetMk_eq_one_or_eq_weylandTauCeti.GL2Borel.doubleCosetMk_eq_weyl_of_ne_one: every double coset ofBis the identity one or the Weyl one, so a double coset other than the identity one is the Weyl one.TauCeti.GL2Borel.card_doubleCosetQuotient_eq_two:Bhas exactly two double cosets inGL₂.TauCeti.GL2Borel.closure_insert_gl2WeylElement_eq_top: the Borel subgroup and the Weyl element generateGL₂.TauCeti.GL2Borel.le_of_isSolvable: every solvable subgroup containing the Borel subgroup equals it when the field contains a nonzero element whose square is not one.TauCeti.GL2Borel.ncard_doubleCoset_weyl: the big cell ofGL₂(𝔽_q)hasq² (q - 1)²elements.
Implementation notes #
The big cell is spelled as Mathlib's DoubleCoset.doubleCoset (GL2WeylElement F) B B rather than
as a new definition for B * {w} * B: the two are definitionally the same set, and using
Mathlib's spelling is what lets the results be read directly as statements about
DoubleCoset.Quotient, which is the form the Mackey criterion asks for.
The GL2 prefix on TauCeti.GL2WeylElement follows the naming that
TauCetiRoadmap/RepresentationTheory/CharacterTheory/README.md uses for this family of objects
(GL2Borel, GL2PrincipalSeries, GL2Steinberg, GL2NonSplitTorus), and matches
TauCeti.GL2Borel in the file this one builds on.
References #
This supplies the double-coset decomposition B \ GL₂ / B that the principal-series milestone of
Layer 9 ("the representation theory of GL₂(𝔽_q)") of
TauCetiRoadmap/RepresentationTheory/CharacterTheory/README.md needs: its target
simple_GL2PrincipalSeries_iff, the irreducibility of Ind_B^{GL₂}(α ⊗ β) for α ≠ β, is read
off the Mackey criterion, whose double-coset sum this decomposition evaluates. It is the rank-one
case of the Bruhat decomposition named in Layer 8 of
TauCetiRoadmap/RepresentationTheory/LieGroups/README.md; the general statement is J. E.
Humphreys, Linear Algebraic Groups, GTM 21, §28.3, whose Theorem is
G = ⨆_{σ ∈ W} B σ B with B σ B = B τ B only for σ = τ. See also W. Fulton and J. Harris,
Representation Theory: A First Course, GTM 129, §5.2, and J.-P. Serre, Linear Representations
of Finite Groups, GTM 42, §7.3.
The Weyl element of GL₂: the permutation matrix !![0, 1; 1, 0] swapping the two basis
vectors. It is an involution, and together with the Borel subgroup it generates GL₂; its double
coset is the big cell of the Bruhat decomposition.
Equations
- TauCeti.GL2WeylElement R = { val := !![0, 1; 1, 0], inv := !![0, 1; 1, 0], val_inv := ⋯, inv_val := ⋯ }
Instances For
The underlying matrix of the Weyl element.
The Weyl element is an involution.
The Weyl element is not upper triangular: its lower-left entry is 1.
The big cell, entrywise. Multiplying the Weyl element by upper-triangular matrices on both
sides produces the matrix !![c₁ a₂, c₁ c₂ + a₁ d₂; d₁ a₂, d₁ c₂]; the lower-left entry d₁ a₂ is
the product of two units, which is the whole content of the Bruhat decomposition.
The lower-left entry detects the big cell. An element of GL₂ lies in the double coset
B w B exactly when its lower-left entry is invertible — the condition complementary, over a
field, to the vanishing that defines B.
Not a simp lemma: TauCeti.mem_doubleCoset_iff_mk_mem_orbit is simp and rewrites any
double-coset membership into an orbit membership, so this left-hand side is not simp-normal.
The Weyl double coset, in the quotient: an element of GL₂ has the same double coset as
the Weyl element exactly when it lies in the big cell. This is
TauCeti.doubleCosetMk_eq_mk_iff_mem at the Weyl element.
The identity double coset of the Borel subgroup is the Borel subgroup. This is
TauCeti.doubleCoset_one_self for H = B.
The Weyl double coset is not the identity one: the Weyl element is not upper triangular.
The Bruhat decomposition of GL₂, covering half: every invertible 2 × 2 matrix over a
field is upper triangular or lies in the big cell B w B, according as its lower-left entry
vanishes or not.
The Bruhat decomposition of GL₂, disjointness half: the Borel subgroup and the big cell
B w B are disjoint, the lower-left entry vanishing on the first and invertible on the second.
Bruhat, in the quotient. Every double coset of the Borel subgroup in GL₂ is either the
identity one or the one of the Weyl element.
The form the Mackey criterion consumes: a double coset of the Borel subgroup other than the identity one is the Weyl one.
The Bruhat decomposition, counted: the Borel subgroup of GL₂ over a field has exactly two
double cosets, indexed by the Weyl group S₂ of GL₂. This is the input to the Mackey
irreducibility criterion for the principal series.
The Borel subgroup and the Weyl element generate GL₂. Every element of GL₂ is upper
triangular or a product b₁ w b₂ of two upper-triangular matrices with the Weyl element, which is
the generation axiom of the (B, N)-pair of GL₂.
Every solvable subgroup of GL₂(F) that contains the upper-triangular subgroup is contained
in it if F has a nonzero element whose square is not one.
Every solvable subgroup of GL₂ over an infinite field that contains the upper-triangular
subgroup is contained in it.
The size of the big cell of GL₂(𝔽_q) is q² (q - 1)²: what is left of the group after
the Borel subgroup, whose order is q (q - 1)². Equivalently |B w B| = |B|²/|T| for the split
torus T, the two double cosets accounting for q (q - 1)² (q + 1) = |GL₂(𝔽_q)|.