The Borel subgroup of GL₂

The Borel subgroup B of GL₂ is the Fin 2 specialization of TauCeti.upperTriangularGroup, the subgroup of invertible upper-triangular matrices. It is the standard minimal parabolic: over a finite field it is the subgroup from which the principal series Ind_B^{GL₂}(α ⊗ β) is induced, and its index q + 1 is the dimension of that induced representation.

Everything except the two counting results is proved over an arbitrary commutative ring, where the subgroup already makes sense: upper-triangular matrices are closed under multiplication, and the inverse of an invertible one is again upper triangular by Matrix.blockTriangular_inv_of_blockTriangular. The constructor TauCeti.GL2Borel.mk, which does not mention the subgroup, needs only a ring. Two facts organize the subgroup:

• the two diagonal entries of an element of B are units, and reading them off is a group homomorphism TauCeti.GL2Borel.diag : B →* Rˣ × Rˣ, the diagonal projection; it is split by the split torus T, the diagonal matrices TauCeti.GL2Borel.torusHom : Rˣ × Rˣ →* B, which is a section of it, and it is by composing with TauCeti.GL2Borel.diag that a pair of characters α, β of Rˣ inflates to a character of B;
• the kernel of the diagonal projection is the unipotent radical U, the image of TauCeti.GL2Borel.unipotentHom, and every element of B factors as a torus element times a unipotent one (TauCeti.GL2Borel.eq_torusHom_mul_unipotentHom) — the decomposition B = T U. Coordinatewise this is the bijection B ≃ (Rˣ × Rˣ) × R (TauCeti.GL2Borel.equivProd), the upper-right entry being the free coordinate.

Over a finite field with q elements these give |B| = q (q - 1)² and hence [GL₂(𝔽_q) : B] = q + 1, the number of points of the projective line.

Main definitions

• TauCeti.GL2Borel R: the upper-triangular subgroup of GL (Fin 2) R.
• TauCeti.GL2Borel.mk: the element of GL (Fin 2) R with prescribed diagonal units and upper-right entry; it lies in TauCeti.GL2Borel R.
• TauCeti.GL2Borel.diag: the two diagonal entries of an element of the Borel subgroup, as a homomorphism to Rˣ × Rˣ, and TauCeti.GL2Borel.torusHom, the split torus, its homomorphic section.
• TauCeti.GL2Borel.unipotentHom: the unipotent radical, Matrix.GeneralLinearGroup.upperRightHom seen as an additive character valued in the Borel subgroup.
• TauCeti.GL2Borel.equivProd: the bijection B ≃ (Rˣ × Rˣ) × R.

Main results

• TauCeti.GL2Borel.mem_iff_exists_mk: an element of GL₂ is upper triangular exactly when it is !![a, b; 0, d] for units a, d.
• TauCeti.GL2Borel.mem_ker_diag_iff: the kernel of TauCeti.GL2Borel.diag is the unipotent radical, the image of TauCeti.GL2Borel.unipotentHom.
• TauCeti.GL2Borel.eq_torusHom_mul_unipotentHom: the decomposition B = T U.
• TauCeti.GL2Borel.det_diag: the determinant of an element of B is the product of its two diagonal entries.
• TauCeti.GL2Borel.exists_det_sub_algebraMap_eq_zero: a matrix with an upper-triangular conjugate has an eigenvalue in the base ring.
• TauCeti.GL2Borel.card_eq: |B| = q (q - 1)² over a finite field with q elements.
• TauCeti.GL2Borel.index_eq: [GL₂(𝔽_q) : B] = q + 1.

Implementation notes

The name follows the GL2 prefix that TauCetiRoadmap/RepresentationTheory/CharacterTheory/README.md uses for this family of objects (GL2Borel, GL2PrincipalSeries, GL2Steinberg, GL2NonSplitTorus), rather than being placed in the Matrix.GeneralLinearGroup namespace; the statements are the roadmap's, with [Field F] [Fintype F] weakened to [CommRing R] wherever the result does not count.

The subgroup is the Fin 2 specialization of TauCeti.upperTriangularGroup. Its public membership lemma is nevertheless stated as the concrete condition g 1 0 = 0, because that is what the coordinate proofs below use; TauCeti.blockTriangular_id_iff identifies this condition with the general upper-triangular predicate.

References

This supplies the Borel subgroup of Layer 9 ("the representation theory of GL₂(𝔽_q)") of TauCetiRoadmap/RepresentationTheory/CharacterTheory/README.md, whose GL2Borel is the subgroup defined here, together with the index q + 1 that its principal-series dimension count needs. See also W. Fulton and J. Harris, Representation Theory: A First Course, GTM 129, §5.2.

@[simp]

theorem TauCeti.blockTriangular_id_iff {R : Type u} [Zero R] {M : Matrix (Fin 2) (Fin 2) R} : M.BlockTriangular id ↔ M 1 0 = 0

In size 2, block triangularity for id : Fin 2 → Fin 2 is the single vanishing condition on the lower-left entry.

def TauCeti.GL2Borel.mk {R : Type u} [Ring R] (a d : Rˣ) (b : R) : GL (Fin 2) R

The invertible upper-triangular matrix !![a, b; 0, d] with prescribed diagonal units a, d and prescribed upper-right entry b.

Equations

• TauCeti.GL2Borel.mk a d b = { val := !![↑a, b; 0, ↑d], inv := !![↑a⁻¹, -(↑a⁻¹ * b * ↑d⁻¹); 0, ↑d⁻¹], val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem TauCeti.GL2Borel.coe_mk {R : Type u} [Ring R] (a d : Rˣ) (b : R) : ↑(mk a d b) = !![↑a, b; 0, ↑d]

@[reducible, inline]

abbrev TauCeti.GL2Borel (R : Type u) [CommRing R] : Subgroup (GL (Fin 2) R)

The Borel subgroup of GL₂, obtained by specializing the general upper-triangular subgroup to Fin 2.

Equations

• TauCeti.GL2Borel R = TauCeti.upperTriangularGroup (Fin 2) R

theorem TauCeti.GL2Borel.mem_iff {R : Type u} [CommRing R] {g : GL (Fin 2) R} : g ∈ GL2Borel R ↔ ↑g 1 0 = 0

@[simp]

theorem TauCeti.GL2Borel.apply_one_zero {R : Type u} [CommRing R] (g : ↥(GL2Borel R)) : ↑↑g 1 0 = 0

The lower-left entry of an element of the Borel subgroup vanishes.

theorem TauCeti.GL2Borel.upperRightHom_mem (R : Type u) [CommRing R] (b : R) : Matrix.GeneralLinearGroup.upperRightHom b ∈ GL2Borel R

The unipotent radical sits inside the Borel subgroup: Matrix.GeneralLinearGroup.upperRightHom sends b to !![1, b; 0, 1].

theorem TauCeti.GL2Borel.scalar_mem (R : Type u) [CommRing R] (u : Rˣ) : (Matrix.GeneralLinearGroup.scalar (Fin 2)) u ∈ GL2Borel R

The scalar matrices sit inside the Borel subgroup.

theorem TauCeti.GL2Borel.mk_mem {R : Type u} [CommRing R] (a d : Rˣ) (b : R) : mk a d b ∈ GL2Borel R

def TauCeti.GL2Borel.diag {R : Type u} [CommRing R] : ↥(GL2Borel R) →* Rˣ × Rˣ

The diagonal projection: the general diagonal projection specialized to Fin 2, with its two coordinates packaged as a pair of units.

Equations

• TauCeti.GL2Borel.diag = (MonoidHom.mk' (fun (t : Fin 2 → Rˣ) => (t 0, t 1)) ⋯).comp TauCeti.UpperTriangularGroup.diag

theorem TauCeti.GL2Borel.diag_eq {R : Type u} [CommRing R] (g : ↥(GL2Borel R)) : diag g = (UpperTriangularGroup.diag g 0, UpperTriangularGroup.diag g 1)

The pair-valued diagonal projection is the two-coordinate packaging of the general diagonal projection.

@[simp]

theorem TauCeti.GL2Borel.diag_fst_val {R : Type u} [CommRing R] (g : ↥(GL2Borel R)) : ↑(diag g).1 = ↑↑g 0 0

@[simp]

theorem TauCeti.GL2Borel.diag_snd_val {R : Type u} [CommRing R] (g : ↥(GL2Borel R)) : ↑(diag g).2 = ↑↑g 1 1

@[simp]

theorem TauCeti.GL2Borel.diag_mk {R : Type u} [CommRing R] (a d : Rˣ) (b : R) : diag ⟨mk a d b, ⋯⟩ = (a, d)

@[simp]

theorem TauCeti.GL2Borel.det_diag {R : Type u} [CommRing R] (g : ↥(GL2Borel R)) : Matrix.GeneralLinearGroup.det ↑g = (diag g).1 * (diag g).2

The determinant of an element of the Borel subgroup is the product of the two torus coordinates.

def TauCeti.GL2Borel.torusHom {R : Type u} [CommRing R] : Rˣ × Rˣ →* ↥(GL2Borel R)

The split torus T, as a homomorphic section of TauCeti.GL2Borel.diag: the diagonal matrix !![a, 0; 0, d]. Its existence is what upgrades the bijection TauCeti.GL2Borel.equivProd to a genuine splitting B = T U.

Equations

• TauCeti.GL2Borel.torusHom = TauCeti.UpperTriangularGroup.diagonalHom.comp (MonoidHom.mk' (fun (p : Rˣ × Rˣ) => ![p.1, p.2]) ⋯)

@[simp]

theorem TauCeti.GL2Borel.coe_torusHom {R : Type u} [CommRing R] (p : Rˣ × Rˣ) : ↑(torusHom p) = mk p.1 p.2 0

@[simp]

theorem TauCeti.GL2Borel.diag_torusHom {R : Type u} [CommRing R] (p : Rˣ × Rˣ) : diag (torusHom p) = p

theorem TauCeti.GL2Borel.diag_surjective {R : Type u} [CommRing R] : Function.Surjective ⇑diag

The diagonal projection is surjective: the diagonal matrix !![a, 0; 0, d] realizes (a, d).

def TauCeti.GL2Borel.unipotentHom {R : Type u} [CommRing R] : AddChar R ↥(GL2Borel R)

The unipotent radical U, as an additive character valued in the Borel subgroup: b is sent to !![1, b; 0, 1]. It is Matrix.GeneralLinearGroup.upperRightHom with its codomain restricted to B.

Equations

• TauCeti.GL2Borel.unipotentHom = { toFun := fun (b : R) => ⟨Matrix.GeneralLinearGroup.upperRightHom b, ⋯⟩, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }

@[simp]

theorem TauCeti.GL2Borel.coe_unipotentHom {R : Type u} [CommRing R] (b : R) : ↑(unipotentHom b) = Matrix.GeneralLinearGroup.upperRightHom b

@[simp]

theorem TauCeti.GL2Borel.diag_unipotentHom {R : Type u} [CommRing R] (b : R) : diag (unipotentHom b) = 1

The unipotent radical is diagonally trivial: both diagonal entries of !![1, b; 0, 1] are 1.

theorem TauCeti.GL2Borel.mem_ker_diag_iff {R : Type u} [CommRing R] (g : ↥(GL2Borel R)) : g ∈ diag.ker ↔ ∃ (b : R), g = unipotentHom b

The kernel of the diagonal projection is the unipotent radical: the elements of the Borel subgroup with both diagonal entries 1, that is, the image of TauCeti.GL2Borel.unipotentHom.

theorem TauCeti.GL2Borel.eq_torusHom_mul_unipotentHom {R : Type u} [CommRing R] (g : ↥(GL2Borel R)) : g = torusHom (diag g) * unipotentHom (↑(diag g).1⁻¹ * ↑↑g 0 1)

The Borel subgroup is T U: every element of B is the diagonal matrix carrying its two torus coordinates times the unipotent matrix carrying the remaining upper-right coordinate.

def TauCeti.GL2Borel.equivProd {R : Type u} [CommRing R] : ↥(GL2Borel R) ≃ (Rˣ × Rˣ) × R

Coordinates on the Borel subgroup: an element of B is exactly a pair of diagonal units together with a free upper-right entry. This is the set-level form of the decomposition TauCeti.GL2Borel.eq_torusHom_mul_unipotentHom into the split torus and the unipotent radical; it is what the cardinality count below runs on.

Equations

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

@[simp]

theorem TauCeti.GL2Borel.equivProd_apply {R : Type u} [CommRing R] (g : ↥(GL2Borel R)) : equivProd g = (diag g, ↑↑g 0 1)

@[simp]

theorem TauCeti.GL2Borel.equivProd_symm_apply {R : Type u} [CommRing R] (p : (Rˣ × Rˣ) × R) : equivProd.symm p = ⟨mk p.1.1 p.1.2 p.2, ⋯⟩

theorem TauCeti.GL2Borel.mem_iff_exists_mk {R : Type u} [CommRing R] {g : GL (Fin 2) R} : g ∈ GL2Borel R ↔ ∃ (a : Rˣ) (d : Rˣ) (b : R), g = mk a d b

Normal form: an element of GL₂ is upper triangular exactly when it is !![a, b; 0, d] for two units a, d and a scalar b.

theorem TauCeti.GL2Borel.exists_det_sub_algebraMap_eq_zero {R : Type u} [CommRing R] {u g : GL (Fin 2) R} (h : g * u * g⁻¹ ∈ GL2Borel R) : ∃ (a : R), (↑u - (algebraMap R (Matrix (Fin 2) (Fin 2) R)) a).det = 0

If some conjugate of u : GL (Fin 2) R is upper triangular then u has an eigenvalue in the base ring: writing a for the upper-left entry of that conjugate, det (u - a) = 0. This is the eigenvalue that an element of the non-split torus has to be shown not to have.

theorem TauCeti.GL2Borel.ne_top (R : Type u) [CommRing R] [Nontrivial R] : GL2Borel R ≠ ⊤

The Borel subgroup is proper: the swap !![0, 1; 1, 0] is invertible but not upper triangular.

theorem TauCeti.GL2Borel.card_eq (F : Type u) [Field F] [Fintype F] : Nat.card ↥(GL2Borel F) = Fintype.card F * (Fintype.card F - 1) ^ 2

The order of the Borel subgroup of GL₂(𝔽_q) is q (q - 1)²: two diagonal units and one free upper-right entry.

theorem TauCeti.GL2Borel.index_eq (F : Type u) [Field F] [Fintype F] : (GL2Borel F).index = Fintype.card F + 1

The index of the Borel subgroup of GL₂(𝔽_q) is q + 1, the number of points of the projective line — hence the dimension of the principal series induced from B.