Standard parabolic subgroups of a Tits system

For a subset J of the simple reflections of a Tits system (B, N), the standard parabolic P_J is generated by B and the simple Bruhat cells indexed by J. Its Bruhat decomposition consists exactly of the cells B w B with w in the subgroup W_J generated by J in the Weyl group. In particular, its intersection with N is the inverse image of W_J under N → W. These statements connect parabolic subgroups of a BN-pair to Weyl-group combinatorics.

The indexing set has type Set T.simple, so every selected generator is a simple reflection. No finiteness, field, or algebraic-group hypothesis is needed. The empty set gives B, and the set of all simple reflections gives the ambient group; consequently B is the ambient group exactly when there are no simple reflections (TauCeti.TitsSystem.subgroupB_eq_top_iff). This file does not classify all subgroups containing B or identify these abstract subgroups with subgroup schemes.

The Bruhat cells and their uniqueness are those of TauCeti.GroupTheory.TitsSystem.Bruhat.Basic and Bruhat.Uniqueness.

References

• J. E. Humphreys, Linear Algebraic Groups (1975), Section 29.
• T. A. Springer, Linear Algebraic Groups, second edition (1998), Section 8.3.

noncomputable def TauCeti.TitsSystem.standardParabolic {G : Type u} [Group G] (T : TitsSystem G) (J : Set ↑T.simple) : Subgroup G

The standard parabolic subgroup generated by B and the simple Bruhat cells selected by J. Equivalently, one can adjoin any normalizer representative of each selected reflection.

theorem TauCeti.TitsSystem.standardParabolic_def {G : Type u} [Group G] (T : TitsSystem G) (J : Set ↑T.simple) : T.standardParabolic J = Subgroup.closure (↑T.subgroupB ∪ ⋃ s ∈ J, T.bruhatCell ↑s)

The standard parabolic is the subgroup closure of B and its selected simple cells.

theorem TauCeti.TitsSystem.subgroupB_le_standardParabolic {G : Type u} [Group G] (T : TitsSystem G) (J : Set ↑T.simple) : T.subgroupB ≤ T.standardParabolic J

Every standard parabolic contains B.

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

A selected simple Bruhat cell lies in the standard parabolic.

theorem TauCeti.TitsSystem.standardParabolic_le_iff {G : Type u} [Group G] (T : TitsSystem G) (J : Set ↑T.simple) (P : Subgroup G) : T.standardParabolic J ≤ P ↔ T.subgroupB ≤ P ∧ ∀ s ∈ J, T.bruhatCell ↑s ⊆ ↑P

A standard parabolic is the least subgroup containing B and the selected simple cells.

theorem TauCeti.TitsSystem.standardParabolic_monotone {G : Type u} [Group G] (T : TitsSystem G) : Monotone T.standardParabolic

Enlarging the selected set of simple reflections enlarges the standard parabolic.

theorem TauCeti.TitsSystem.bruhatCell_subset_standardParabolic_of_mem_closure {G : Type u} [Group G] (T : TitsSystem G) {J : Set ↑T.simple} {w : T.WeylGroup} (hw : w ∈ Subgroup.closure (Subtype.val '' J)) : T.bruhatCell w ⊆ ↑(T.standardParabolic J)

Every cell indexed by the Weyl subgroup generated by J lies in P_J.

theorem TauCeti.TitsSystem.mem_standardParabolic_iff {G : Type u} [Group G] (T : TitsSystem G) {J : Set ↑T.simple} {g : G} : g ∈ T.standardParabolic J ↔ ∃ w ∈ Subgroup.closure (Subtype.val '' J), g ∈ T.bruhatCell w

The Bruhat decomposition of a standard parabolic: an element lies in P_J exactly when its Bruhat cell is indexed by the Weyl subgroup generated by J.

theorem TauCeti.TitsSystem.coe_standardParabolic {G : Type u} [Group G] (T : TitsSystem G) (J : Set ↑T.simple) : ↑(T.standardParabolic J) = ⋃ w ∈ Subgroup.closure (Subtype.val '' J), T.bruhatCell w

The standard parabolic is the union of the cells indexed by its Weyl subgroup. The cells are pairwise disjoint by disjoint_bruhatCell_iff.

theorem TauCeti.TitsSystem.mem_standardParabolic_iff_of_mem_bruhatCell {G : Type u} [Group G] (T : TitsSystem G) {J : Set ↑T.simple} {g : G} {w : T.WeylGroup} (hg : g ∈ T.bruhatCell w) : g ∈ T.standardParabolic J ↔ w ∈ Subgroup.closure (Subtype.val '' J)

On any given Bruhat cell, parabolic membership is exactly membership of its Weyl index in the subgroup generated by the selected simple reflections.

@[simp]

theorem TauCeti.TitsSystem.coe_mem_standardParabolic_iff {G : Type u} [Group G] (T : TitsSystem G) (J : Set ↑T.simple) (n : ↥T.subgroupN) : ↑n ∈ T.standardParabolic J ↔ ↑n ∈ Subgroup.closure (Subtype.val '' J)

An element of N belongs to P_J exactly when its Weyl class belongs to W_J. Thus P_J ∩ N is the inverse image of W_J under N → W.

@[simp]

theorem TauCeti.TitsSystem.standardParabolic_empty {G : Type u} [Group G] (T : TitsSystem G) : T.standardParabolic ∅ = T.subgroupB

The standard parabolic for the empty set of simple reflections is B.

@[simp]

theorem TauCeti.TitsSystem.standardParabolic_univ {G : Type u} [Group G] (T : TitsSystem G) : T.standardParabolic Set.univ = ⊤

Selecting every simple reflection gives the whole ambient group.

theorem TauCeti.TitsSystem.subgroupB_eq_top_iff {G : Type u} [Group G] (T : TitsSystem G) : T.subgroupB = ⊤ ↔ T.simple = ∅

The subgroup B is the whole group exactly when there are no simple reflections.