Tits systems

A Tits system, or BN-pair, in a group G consists of two subgroups B and N and a set of simple reflections in W = N / (B ∩ N). The subgroups generate G, the intersection B ∩ N is normal in N, the simple reflections generate W and are involutions, and the double cosets satisfy the Tits multiplication and nondegeneracy axioms.

Main definitions

• TauCeti.TitsSystem: a Tits system with its simple reflections in the Weyl quotient.
• TauCeti.TitsSystem.intersection: the subgroup B ∩ N, regarded as a subgroup of N.
• TauCeti.TitsSystem.WeylGroup: the quotient N / (B ∩ N).
• TauCeti.TitsSystem.simple: the simple reflections in the Weyl group.
• TauCeti.TitsSystem.simple_mul_simple_self, TauCeti.TitsSystem.inv_simple and TauCeti.TitsSystem.simple_ne_one: the simple reflections are nontrivial involutions.

References

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

structure TauCeti.TitsSystem (G : Type u_1) [Group G] : Type u_1

A Tits system (or BN-pair) in G.

The field mul_doubleCoset_subset is the usual axiom B s B w B ⊆ B (s w) B ∪ B w B. Its representative is supplied existentially so the structure records only the representation-independent simple set in N / (B ∩ N).

• subgroupB : Subgroup G

  The subgroup conventionally denoted B.

• subgroupN : Subgroup G

  The subgroup conventionally denoted N.

• closure_subgroupB_union_subgroupN : Subgroup.closure (↑self.subgroupB ∪ ↑self.subgroupN) = ⊤

  The subgroups B and N generate the ambient group.

• intersection_normal : (self.subgroupB.subgroupOf self.subgroupN).Normal

  The intersection B ∩ N, regarded inside N, is normal.

• simple : Set (↥self.subgroupN ⧸ self.subgroupB.subgroupOf self.subgroupN)

  The simple reflections in the Weyl quotient N / (B ∩ N).

• closure_simple : let x := ⋯; Subgroup.closure self.simple = ⊤

  The simple reflections generate the Weyl quotient.

• exists_simpleRep_mul_self_mem (s : ↥self.subgroupN ⧸ self.subgroupB.subgroupOf self.subgroupN) (hs : s ∈ self.simple) : ∃ (r : ↥self.subgroupN), ↑r = s ∧ r * r ∈ self.subgroupB.subgroupOf self.subgroupN

  Every simple reflection has a representative whose square lies in B ∩ N.

• mul_doubleCoset_subset (s : ↥self.subgroupN ⧸ self.subgroupB.subgroupOf self.subgroupN) (hs : s ∈ self.simple) : ∃ (r : ↥self.subgroupN), ↑r = s ∧ ∀ (w : ↥self.subgroupN), DoubleCoset.doubleCoset ↑r ↑self.subgroupB ↑self.subgroupB * DoubleCoset.doubleCoset ↑w ↑self.subgroupB ↑self.subgroupB ⊆ DoubleCoset.doubleCoset ↑(r * w) ↑self.subgroupB ↑self.subgroupB ∪ DoubleCoset.doubleCoset ↑w ↑self.subgroupB ↑self.subgroupB

  Multiplying a Bruhat cell on the left by a simple cell produces at most the adjacent cell and the original cell.

• exists_conj_not_mem (s : ↥self.subgroupN ⧸ self.subgroupB.subgroupOf self.subgroupN) (hs : s ∈ self.simple) : ∃ (r : ↥self.subgroupN), ↑r = s ∧ ∃ (b : ↥self.subgroupB), ↑r * ↑b * (↑r)⁻¹ ∉ self.subgroupB

  No simple reflection conjugates B into B.

theorem TauCeti.TitsSystem.ext {G : Type u_1} {inst✝ : Group G} {x y : TitsSystem G} (subgroupB : x.subgroupB = y.subgroupB) (subgroupN : x.subgroupN = y.subgroupN) (simple : x.simple ≍ y.simple) : x = y

theorem TauCeti.TitsSystem.ext_iff {G : Type u_1} {inst✝ : Group G} {x y : TitsSystem G} : x = y ↔ x.subgroupB = y.subgroupB ∧ x.subgroupN = y.subgroupN ∧ x.simple ≍ y.simple

@[reducible, inline]

abbrev TauCeti.TitsSystem.intersection {G : Type u_1} [Group G] (T : TitsSystem G) : Subgroup ↥T.subgroupN

The intersection B ∩ N, regarded as a subgroup of N.

theorem TauCeti.TitsSystem.mem_intersection {G : Type u_1} [Group G] (T : TitsSystem G) (n : ↥T.subgroupN) : n ∈ T.intersection ↔ ↑n ∈ T.subgroupB

Membership in the intersection means membership in B after forgetting the N subtype.

instance TauCeti.TitsSystem.intersectionNormal {G : Type u_1} [Group G] (T : TitsSystem G) : T.intersection.Normal

@[reducible, inline]

abbrev TauCeti.TitsSystem.WeylGroup {G : Type u_1} [Group G] (T : TitsSystem G) : Type u_1

The Weyl group W = N / (B ∩ N) of a Tits system.

@[simp]

theorem TauCeti.TitsSystem.simple_mul_simple_self {G : Type u_1} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) : s * s = 1

Every simple reflection has square one.

@[simp]

theorem TauCeti.TitsSystem.inv_simple {G : Type u_1} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) : s⁻¹ = s

A simple reflection is its own inverse.

@[simp]

theorem TauCeti.TitsSystem.simple_mul_simple_cancel_left {G : Type u_1} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) (w : T.WeylGroup) : s * (s * w) = w

Multiplying twice by a simple reflection on the left is the identity.

@[simp]

theorem TauCeti.TitsSystem.simple_mul_simple_cancel_right {G : Type u_1} [Group G] (T : TitsSystem G) (w : T.WeylGroup) {s : T.WeylGroup} (hs : s ∈ T.simple) : w * s * s = w

Multiplying twice by a simple reflection on the right is the identity.

theorem TauCeti.TitsSystem.simple_ne_one {G : Type u_1} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) : s ≠ 1

A simple reflection is not the identity.