The upper-triangular subgroup of SL₂

The standard Borel subgroup of SL₂(R) consists of the determinant-one upper-triangular matrices. Over a field, its two Bruhat cells are represented by the identity and by ModularGroup.S = !![0, -1; 1, 0]. Thus the Borel together with ModularGroup.S generates SL₂, and no larger solvable subgroup can contain it whenever the field has a nonzero element whose square is not one. In particular, this holds over every infinite field.

The maximal-solvability theorem is the abstract-group input for proving that the upper-triangular closed subgroup scheme of SL₂ is a Borel subgroup. The field hypothesis is used only to rule out solvability of SL₂; the Bruhat decomposition itself holds over every field. Entrywise mapping makes the construction functorial in the coefficient ring.

Main declarations

• TauCeti.SL2Borel: the upper-triangular subgroup of SL₂.
• TauCeti.SL2Borel.map: entrywise mapping along a ring homomorphism.
• TauCeti.SL2Borel.mem_doubleCoset_modularGroup_S_iff: the big cell of the rank-one Bruhat decomposition is detected by the lower-left entry.
• TauCeti.SL2Borel.closure_insert_modularGroup_S_eq_top: the Borel and the Weyl element generate SL₂.
• TauCeti.SL2Borel.le_of_isSolvable: a solvable subgroup containing the Borel is contained in it when the field contains a nonzero element whose square is not one.

References

• J. E. Humphreys, Linear Algebraic Groups, §28.3.
• R. Steinberg, Lectures on Chevalley Groups, §3.

def TauCeti.SL2Borel (R : Type u) [CommRing R] : Subgroup (Matrix.SpecialLinearGroup (Fin 2) R)

The standard upper-triangular subgroup of SL₂(R), obtained by pulling the upper-triangular subgroup of GL₂(R) back along the canonical inclusion.

Equations

• TauCeti.SL2Borel R = Subgroup.comap Matrix.SpecialLinearGroup.toGL (TauCeti.GL2Borel R)

@[simp]

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

An element of SL₂(R) belongs to the standard Borel exactly when its lower-left entry vanishes.

@[simp]

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

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

def TauCeti.SL2Borel.mk {R : Type u} [CommRing R] (a : Rˣ) (b : R) : ↥(SL2Borel R)

The upper-triangular determinant-one matrix with diagonal entries a, a⁻¹ and upper-right entry b.

Equations

• TauCeti.SL2Borel.mk a b = ⟨⟨!![↑a, b; 0, ↑a⁻¹], ⋯⟩, ⋯⟩

@[simp]

theorem TauCeti.SL2Borel.coe_mk {R : Type u} [CommRing R] (a : Rˣ) (b : R) : ↑↑(mk a b) = !![↑a, b; 0, ↑a⁻¹]

The matrix underlying mk a b.

def TauCeti.SL2Borel.map {R : Type u} [CommRing R] {S : Type v} [CommRing S] (phi : R →+* S) : ↥(SL2Borel R) →* ↥(SL2Borel S)

Apply a ring homomorphism entrywise to an upper-triangular determinant-one matrix.

Equations

• TauCeti.SL2Borel.map phi = ((Matrix.SpecialLinearGroup.map phi).domRestrict (TauCeti.SL2Borel R)).codRestrict (TauCeti.SL2Borel S) ⋯

@[simp]

theorem TauCeti.SL2Borel.coe_map {R : Type u} [CommRing R] {S : Type v} [CommRing S] (phi : R →+* S) (g : ↥(SL2Borel R)) : ↑((map phi) g) = (Matrix.SpecialLinearGroup.map phi) ↑g

The special-linear matrix underlying an entrywise-mapped Borel element is the entrywise map of its underlying matrix.

theorem TauCeti.SL2Borel.map_apply {R : Type u} [CommRing R] {S : Type v} [CommRing S] (phi : R →+* S) (g : ↥(SL2Borel R)) (i j : Fin 2) : ↑↑((map phi) g) i j = phi (↑↑g i j)

The (i, j) entry of the entrywise map of g is the image under phi of the (i, j) entry of g.

@[simp]

theorem TauCeti.SL2Borel.map_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] (phi : R →+* S) (a : Rˣ) (b : R) : (map phi) (mk a b) = mk ((Units.map ↑phi) a) (phi b)

Entrywise mapping sends a matrix in standard coordinates to the matrix obtained by mapping both parameters.

@[simp]

theorem TauCeti.SL2Borel.map_id {R : Type u} [CommRing R] : map (RingHom.id R) = MonoidHom.id ↥(SL2Borel R)

Entrywise mapping along the identity ring homomorphism is the identity.

@[simp]

theorem TauCeti.SL2Borel.map_comp {R : Type u} [CommRing R] {S : Type u_1} {T : Type u_2} [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) : map (g.comp f) = (map g).comp (map f)

Successive entrywise maps agree with mapping along the composite ring homomorphism.

def TauCeti.SL2Borel.toGL2Borel {R : Type u} [CommRing R] : ↥(SL2Borel R) →* ↥(GL2Borel R)

The canonical inclusion from the SL₂ Borel to the GL₂ Borel.

Equations

• TauCeti.SL2Borel.toGL2Borel = MonoidHom.restrict ⋯

@[simp]

theorem TauCeti.SL2Borel.coe_toGL2Borel {R : Type u} [CommRing R] (g : ↥(SL2Borel R)) : ↑(toGL2Borel g) = Matrix.SpecialLinearGroup.toGL ↑g

The inclusion of the SL₂ Borel into the GL₂ Borel does not change the underlying general linear matrix.

theorem TauCeti.SL2Borel.toGL2Borel_injective {R : Type u} [CommRing R] : Function.Injective ⇑toGL2Borel

The inclusion from the SL₂ Borel to the GL₂ Borel is injective.

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

The upper-left diagonal entry of an SL₂ Borel matrix, bundled as a unit.

Equations

• TauCeti.SL2Borel.diag = { toFun := fun (g : ↥(TauCeti.SL2Borel R)) => (TauCeti.GL2Borel.diag (TauCeti.SL2Borel.toGL2Borel g)).1, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

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

The value of the diagonal parameter is the upper-left matrix entry.

def TauCeti.SL2Borel.upperRight {R : Type u} [CommRing R] (g : ↥(SL2Borel R)) : R

The free upper-right parameter of an SL₂ Borel matrix.

Equations

• TauCeti.SL2Borel.upperRight g = ↑↑g 0 1

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

The upper-right parameter is the upper-right matrix entry.

@[simp]

theorem TauCeti.SL2Borel.diag_mk {R : Type u} [CommRing R] (a : Rˣ) (b : R) : diag (mk a b) = a

The diagonal parameter of a matrix built by mk is its first argument.

@[simp]

theorem TauCeti.SL2Borel.upperRight_mk {R : Type u} [CommRing R] (a : Rˣ) (b : R) : upperRight (mk a b) = b

The upper-right parameter of a matrix built by mk is its second argument.

@[simp]

theorem TauCeti.SL2Borel.mk_diag_upperRight {R : Type u} [CommRing R] (g : ↥(SL2Borel R)) : mk (diag g) (upperRight g) = g

Every SL₂ Borel matrix is recovered from its diagonal and upper-right parameters.

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

An SL₂ Borel matrix is equivalently a diagonal unit and a free upper-right entry.

Equations

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

@[simp]

theorem TauCeti.SL2Borel.equivProd_apply {R : Type u} [CommRing R] (g : ↥(SL2Borel R)) : equivProd g = (diag g, upperRight g)

The product equivalence records the diagonal unit and upper-right entry.

@[simp]

theorem TauCeti.SL2Borel.equivProd_symm_apply {R : Type u} [CommRing R] (p : Rˣ × R) : equivProd.symm p = mk p.1 p.2

The inverse product equivalence constructs the matrix with the given parameters.

instance TauCeti.SL2Borel.instIsSolvable {R : Type u} [CommRing R] : Group.IsSolvable ↥(SL2Borel R)

The upper-triangular subgroup of SL₂(R) is solvable.

theorem TauCeti.SL2Borel.mem_doubleCoset_modularGroup_S_of_notMem {F : Type u} [Field F] {g : Matrix.SpecialLinearGroup (Fin 2) F} (hg : g ∉ SL2Borel F) : g ∈ DoubleCoset.doubleCoset ((Matrix.SpecialLinearGroup.map (Int.castRingHom F)) ModularGroup.S) ↑(SL2Borel F) ↑(SL2Borel F)

An element outside the upper-triangular subgroup of SL₂(F) lies in the big Bruhat cell represented by ModularGroup.S.

theorem TauCeti.SL2Borel.mem_doubleCoset_modularGroup_S_iff {F : Type u} [Field F] {g : Matrix.SpecialLinearGroup (Fin 2) F} : g ∈ DoubleCoset.doubleCoset ((Matrix.SpecialLinearGroup.map (Int.castRingHom F)) ModularGroup.S) ↑(SL2Borel F) ↑(SL2Borel F) ↔ ↑g 1 0 ≠ 0

The lower-left entry detects the big cell. An element of SL₂(F) lies in the double coset of ModularGroup.S by the standard Borel exactly when its lower-left entry is nonzero.

Not a simp lemma: TauCeti.mem_doubleCoset_iff_mk_mem_orbit rewrites double-coset membership to orbit membership, so the left-hand side is not simp-normal.

theorem TauCeti.SL2Borel.closure_insert_modularGroup_S_eq_top {F : Type u} [Field F] : Subgroup.closure (insert ((Matrix.SpecialLinearGroup.map (Int.castRingHom F)) ModularGroup.S) ↑(SL2Borel F)) = ⊤

The upper-triangular subgroup and the Weyl element ModularGroup.S generate SL₂(F).

theorem TauCeti.SL2Borel.le_of_isSolvable {F : Type u} [Field F] (hF : ∃ (a : F), a ≠ 0 ∧ a ^ 2 ≠ 1) (P : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [Group.IsSolvable ↥P] (hBP : SL2Borel F ≤ P) : P ≤ SL2Borel F

Every solvable subgroup of SL₂(F) that contains the standard Borel is contained in it if F has a nonzero element whose square is not one.

theorem TauCeti.SL2Borel.le_of_isSolvable_of_infinite {F : Type u} [Field F] [Infinite F] (P : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [Group.IsSolvable ↥P] (hBP : SL2Borel F ≤ P) : P ≤ SL2Borel F

Every solvable subgroup of SL₂ over an infinite field that contains the standard Borel is contained in it.