Tits systems of rank one

A Tits system of rank one has a single simple reflection s, and its Bruhat decomposition reads G = B ∪ B s B. Conversely, this two-cell decomposition already supplies the generation and multiplication axioms of a Tits system. This file records that construction.

Let B and N be subgroups of G, with B ∩ N normal in N, and let n ∈ N be an element such that

• every element of N lies in B or in n B, so the Weyl group N / (B ∩ N) is generated by the class of n;
• n² ∈ B, and n B n⁻¹ ≠ B;
• every element of G lies in B or in the double coset B n B.

Then TauCeti.TitsSystem.ofRankOne is a Tits system with B, N and the single simple reflection n (B ∩ N). Its Coxeter system is irreducible, having only one generator, which is the irreducibility hypothesis of Tits's simplicity theorem TauCeti.TitsSystem.le_normalCore_or_eq_top_of_normal. Applying that theorem additionally requires G to be perfect and a solvable subgroup normalized by B whose conjugates generate G.

These are the Tits systems of the finite groups of Lie rank one, such as SL₂(q), the unitary groups SU₃(q), the Suzuki groups and the Ree groups ²G₂(q), where B is the stabilizer of a point in a doubly transitive action and n exchanges that point with a second one. The subgroup N may be taken as small as the cyclic group generated by n.

Main definitions and results

• TauCeti.TitsSystem.ofRankOne: the Tits system defined by a two-cell Bruhat decomposition.
• TauCeti.TitsSystem.ofRankOne_simple: its only simple reflection is the class of n.
• TauCeti.TitsSystem.isIrreducible_ofRankOne: it is irreducible.

References

• J. E. Humphreys, Linear Algebraic Groups (1975), Section 29.1.

def TauCeti.TitsSystem.ofRankOne {G : Type u} [Group G] (B N : Subgroup G) [(B.subgroupOf N).Normal] (n : ↥N) (hn : ↑n * ↑n ∈ B) (hN : ∀ x ∈ N, x ∈ B ∨ (↑n)⁻¹ * x ∈ B) (hconj : ∃ b ∈ B, ↑n * b * (↑n)⁻¹ ∉ B) (hbruhat : ∀ (g : G), g ∈ B ∨ g ∈ DoubleCoset.doubleCoset ↑n ↑B ↑B) : TitsSystem G

The Tits system of a two-cell Bruhat decomposition. If B ∩ N is normal in N, every element of N lies in B or in n B, n² ∈ B, n B n⁻¹ ≠ B, and every element of G lies in B or in B n B, then B and N form a Tits system whose only simple reflection is the class of n.

@[simp]

theorem TauCeti.TitsSystem.ofRankOne_subgroupB {G : Type u} [Group G] {B N : Subgroup G} [(B.subgroupOf N).Normal] {n : ↥N} {hn : ↑n * ↑n ∈ B} {hN : ∀ x ∈ N, x ∈ B ∨ (↑n)⁻¹ * x ∈ B} {hconj : ∃ b ∈ B, ↑n * b * (↑n)⁻¹ ∉ B} {hbruhat : ∀ (g : G), g ∈ B ∨ g ∈ DoubleCoset.doubleCoset ↑n ↑B ↑B} : (ofRankOne B N n hn hN hconj hbruhat).subgroupB = B

The subgroup B of the Tits system of a two-cell decomposition is B.

@[simp]

theorem TauCeti.TitsSystem.ofRankOne_subgroupN {G : Type u} [Group G] {B N : Subgroup G} [(B.subgroupOf N).Normal] {n : ↥N} {hn : ↑n * ↑n ∈ B} {hN : ∀ x ∈ N, x ∈ B ∨ (↑n)⁻¹ * x ∈ B} {hconj : ∃ b ∈ B, ↑n * b * (↑n)⁻¹ ∉ B} {hbruhat : ∀ (g : G), g ∈ B ∨ g ∈ DoubleCoset.doubleCoset ↑n ↑B ↑B} : (ofRankOne B N n hn hN hconj hbruhat).subgroupN = N

The subgroup N of the Tits system of a two-cell decomposition is N.

@[simp]

theorem TauCeti.TitsSystem.ofRankOne_simple {G : Type u} [Group G] {B N : Subgroup G} [(B.subgroupOf N).Normal] {n : ↥N} {hn : ↑n * ↑n ∈ B} {hN : ∀ x ∈ N, x ∈ B ∨ (↑n)⁻¹ * x ∈ B} {hconj : ∃ b ∈ B, ↑n * b * (↑n)⁻¹ ∉ B} {hbruhat : ∀ (g : G), g ∈ B ∨ g ∈ DoubleCoset.doubleCoset ↑n ↑B ↑B} : (ofRankOne B N n hn hN hconj hbruhat).simple = {↑⟨↑n, ⋯⟩}

The only simple reflection of the Tits system of a two-cell decomposition is the class of n.

theorem TauCeti.TitsSystem.isIrreducible_ofRankOne {G : Type u} [Group G] {B N : Subgroup G} [(B.subgroupOf N).Normal] {n : ↥N} {hn : ↑n * ↑n ∈ B} {hN : ∀ x ∈ N, x ∈ B ∨ (↑n)⁻¹ * x ∈ B} {hconj : ∃ b ∈ B, ↑n * b * (↑n)⁻¹ ∉ B} {hbruhat : ∀ (g : G), g ∈ B ∨ g ∈ DoubleCoset.doubleCoset ↑n ↑B ↑B} : (ofRankOne B N n hn hN hconj hbruhat).IsIrreducible

A Tits system of rank one is irreducible.