Classification of subgroups containing the Borel subgroup of a BN-pair

For a Tits system (B, N), the standard parabolics give an order isomorphism from subsets of the simple reflections to subgroups containing B. The inverse selects those simple Bruhat cells contained in the subgroup. This is an abstract group-theoretic classification; no identification with parabolic subgroup schemes is asserted.

The key step is that if a subgroup containing B contains B w B, it also contains the simple cells in a reduced expression of w. Length-decreasing Bruhat multiplication extracts the first simple cell, and induction extracts the rest. The exchange condition shows that no additional simple cell appears in a standard parabolic.

Main declarations

• TauCeti.TitsSystem.standardParabolic_eq_of_subgroupB_le: every subgroup containing B is the standard parabolic selected by its simple cells.
• TauCeti.TitsSystem.standardParabolic_le_standardParabolic_iff: the parametrization preserves and reflects inclusion.
• TauCeti.TitsSystem.standardParabolicOrderIso: the classification as an order isomorphism.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter IV, §2, no. 5.
• J. E. Humphreys, Linear Algebraic Groups (1975), Section 29.

The proof uses the Bruhat multiplication and exchange APIs in TauCeti.GroupTheory.TitsSystem.Bruhat.Exchange and the standard parabolic decomposition in TauCeti.GroupTheory.TitsSystem.Parabolic.Basic.

theorem TauCeti.TitsSystem.bruhatCell_subset_of_mem {G : Type u} [Group G] (T : TitsSystem G) {P : Subgroup G} (hB : T.subgroupB ≤ P) {w : T.WeylGroup} {g : G} (hg : g ∈ T.bruhatCell w) (hP : g ∈ P) : T.bruhatCell w ⊆ ↑P

A subgroup containing B contains the whole Bruhat cell of each of its elements.

theorem TauCeti.TitsSystem.bruhatCell_subset_of_wordLength_lt {G : Type u} [Group G] (T : TitsSystem G) {P : Subgroup G} (hB : T.subgroupB ≤ P) {s w : T.WeylGroup} (hs : s ∈ T.simple) (hw : T.bruhatCell w ⊆ ↑P) (hlt : T.simpleGenerators.wordLength (s * w) < T.simpleGenerators.wordLength w) : T.bruhatCell s ⊆ ↑P ∧ T.bruhatCell (s * w) ⊆ ↑P

If a simple reflection shortens a cell contained in a subgroup containing B, both the simple cell and the shortened cell lie in that subgroup.

theorem TauCeti.TitsSystem.bruhatCell_subset_of_mem_reduced_word {G : Type u} [Group G] (T : TitsSystem G) {P : Subgroup G} (hB : T.subgroupB ≤ P) {l : List T.WeylGroup} (hl : ∀ s ∈ l, s ∈ T.simple) (hlen : l.length = T.simpleGenerators.wordLength l.prod) (hP : T.bruhatCell l.prod ⊆ ↑P) (s : T.WeylGroup) : s ∈ l → T.bruhatCell s ⊆ ↑P

The Bruhat cell of every letter of a reduced word lies in a subgroup containing B if the cell of that word lies in the subgroup.

theorem TauCeti.TitsSystem.standardParabolic_eq_of_subgroupB_le {G : Type u} [Group G] (T : TitsSystem G) {P : Subgroup G} (hB : T.subgroupB ≤ P) : T.standardParabolic {s : ↑T.simple | T.bruhatCell ↑s ⊆ ↑P} = P

Every subgroup containing B is the standard parabolic generated by the simple cells it contains.

@[simp]

theorem TauCeti.TitsSystem.bruhatCell_subset_standardParabolic_iff {G : Type u} [Group G] (T : TitsSystem G) (J : Set ↑T.simple) (s : ↑T.simple) : T.bruhatCell ↑s ⊆ ↑(T.standardParabolic J) ↔ s ∈ J

A standard parabolic contains a simple cell exactly when that reflection was selected.

@[simp]

theorem TauCeti.TitsSystem.standardParabolic_le_standardParabolic_iff {G : Type u} [Group G] (T : TitsSystem G) (J K : Set ↑T.simple) : T.standardParabolic J ≤ T.standardParabolic K ↔ J ⊆ K

Inclusion of standard parabolics is exactly inclusion of their sets of simple reflections.

noncomputable def TauCeti.TitsSystem.standardParabolicOrderIso {G : Type u} [Group G] (T : TitsSystem G) : Set ↑T.simple ≃o ↑(Set.Ici T.subgroupB)

Standard parabolics classify subgroups containing B, with their inclusion order.

@[simp]

theorem TauCeti.TitsSystem.standardParabolicOrderIso_apply {G : Type u} [Group G] (T : TitsSystem G) (J : Set ↑T.simple) : ↑(T.standardParabolicOrderIso J) = T.standardParabolic J

The classification sends a selection to its standard parabolic.

@[simp]

theorem TauCeti.TitsSystem.mem_standardParabolicOrderIso_symm_apply {G : Type u} [Group G] (T : TitsSystem G) (P : ↑(Set.Ici T.subgroupB)) (s : ↑T.simple) : s ∈ T.standardParabolicOrderIso.symm P ↔ T.bruhatCell ↑s ⊆ ↑↑P

The inverse classification selects precisely the simple cells in the subgroup.