theorem GoodMaximalBounded.mem_bruhatCell_one_of_mem_B {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (b : G) (hb : b ∈ bp.B) : b ∈ bp.bruhatCell 1

Every element of the Borel subgroup $B$ lies in the Bruhat cell $B \cdot 1 \cdot B$ indexed by the identity.

theorem GoodMaximalBounded.one_mem_parabolicSubgroupW {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S' : Set B_idx) : 1 ∈ bp.parabolicSubgroupW S'

The identity belongs to every parabolic subgroup $W_{S'} \leq W$.

theorem GoodMaximalBounded.B_subset_standardParabolic {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S' : Set B_idx) : ↑bp.B ⊆ bp.standardParabolic S'

The Borel subgroup $B$ is contained in every standard parabolic $P_{S'} = B W_{S'} B$.

theorem GoodMaximalBounded.B_le_standardParabolic_subgroup {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S' : Set B_idx) (H : Subgroup G) (hH : ↑H = bp.standardParabolic S') : bp.B ≤ H

Subgroup-level statement: if $H \leq G$ has underlying set equal to the standard parabolic $P_{S'}$, then $B \leq H$.

theorem GoodMaximalBounded.standardParabolic_is_subgroup {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (S' : Set B_idx) : ∃ (H : Subgroup G), ↑H = bp.standardParabolic S'

Under the Bruhat properties, each standard parabolic $P_{S'}$ is the underlying set of an honest subgroup of $G$.

def GoodMaximalBounded.vertexFixingGenerators {B_idx : Type u_1} (_M : CoxeterMatrix B_idx) (s₀ : B_idx) : Set B_idx

The set of generators fixing the chosen vertex $s_0$: everything in $S \setminus \{s_0\}$.

def GoodMaximalBounded.PermStabilizesSx {B_idx : Type u_1} (M : CoxeterMatrix B_idx) (s₀ : B_idx) (σ : Equiv.Perm B_idx) : Prop

A permutation $\sigma$ of the generator index set stabilises the vertex $s_0$ iff it maps the subset $S \setminus \{s_0\}$ to itself.

def GoodMaximalBounded.liftK₀ {Gt : Type u_1} [Group Gt] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (gbnpair : GeneralizedBNPair Gt M) (K₀ : Subgroup ↑↑gbnpair.G) : Subgroup Gt

Lift a subgroup of $G \leq G^t$ to a subgroup of $G^t$ via the inclusion.

def GoodMaximalBounded.productSetOmegaPrimeK₀ {Gt : Type u_1} [Group Gt] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (gbnpair : GeneralizedBNPair Gt M) (Ω' : Subgroup Gt) (K₀ : Subgroup ↑↑gbnpair.G) : Set Gt

The set product $\Omega' \cdot K_0$ inside $G^t$, where $K_0$ is lifted from $G$ to $G^t$.

def GoodMaximalBounded.BornologyLiftCompatible {Gt : Type u_1} [Group Gt] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (gbnpair : GeneralizedBNPair Gt M) (bornG : CompactSubgroups.GroupBornology ↑↑gbnpair.G) (bornGt : CompactSubgroups.GroupBornology Gt) : Prop

Compatibility condition: the bornology on $G^t$ extends the one on $G$, i.e. bounded subsets of $G$ have bounded image in $G^t$.

structure GoodMaximalBounded.GoodBoundedSetup (Gt : Type u_1) [Group Gt] {B_idx : Type u_2} (M : CoxeterMatrix B_idx) : Type (max u_1 u_2)

The data needed to construct good maximal bounded subgroups of $G^t$: a generalised BN-pair, bornologies on $G$ and $G^t$, a linear-part homomorphism on $W$, existence of a good maximal bounded subgroup $K_0$ in $G$, and bornological compatibility between the two groups.

• gbnpair : GeneralizedBNPair Gt M
• bornG : CompactSubgroups.GroupBornology ↑↑self.gbnpair.G
• bornGt : CompactSubgroups.GroupBornology Gt
• linearPart : M.Group →* M.Group
• K₀_exists : Nonempty (CompactSubgroups.GoodMaximalBounded self.gbnpair.strictBNPair self.bornG self.linearPart)
• bornology_compatible : BornologyLiftCompatible self.gbnpair self.bornG self.bornGt

theorem GoodMaximalBounded.GoodBoundedSetup.omega_prime_exists {Gt : Type u_1} [Group Gt] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (setup : GoodBoundedSetup Gt M) (s₀ : B_idx) : ∃ Ω' ≤ setup.gbnpair.Tt, setup.bornGt.isBounded ↑Ω' ∧ ∀ t ∈ Ω', ∀ (σ : Equiv.Perm B_idx), (∀ (s : B_idx) (n : ↥setup.gbnpair.strictBNPair.N), setup.gbnpair.strictBNPair.π n = M.toCoxeterSystem.simple s → ∃ (n' : ↥setup.gbnpair.strictBNPair.N), setup.gbnpair.strictBNPair.π n' = M.toCoxeterSystem.simple (σ s) ∧ ↑↑n' = t * ↑↑n * t⁻¹) → PermStabilizesSx M s₀ σ

Existence of a bounded subgroup $\Omega' \leq T^t$ whose elements, when conjugating any lift of the simple reflection $s$ to another lift of $\sigma s$, produce a permutation $\sigma$ stabilising $S \setminus \{s_0\}$.

theorem GoodMaximalBounded.GoodBoundedSetup.product_is_subgroup {Gt : Type u_1} [Group Gt] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (setup : GoodBoundedSetup Gt M) (Ω' : Subgroup Gt) (K₀ : Subgroup ↑↑setup.gbnpair.G) : ∃ (H : Subgroup Gt), ↑H = productSetOmegaPrimeK₀ setup.gbnpair Ω' K₀

The product set $\Omega' \cdot K_0$ is the underlying set of an honest subgroup of $G^t$.

theorem GoodMaximalBounded.good_bounded_subgroup_of_Gt_exist {Gt : Type u_1} [Group Gt] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (setup : GoodBoundedSetup Gt M) : ∃ (H : Subgroup Gt), CompactSubgroups.IsBoundedSubgroup setup.bornGt H ∧ ∃ (K₀_data : CompactSubgroups.GoodMaximalBounded setup.gbnpair.strictBNPair setup.bornG setup.linearPart), ∃ Ω' ≤ setup.gbnpair.Tt, CompactSubgroups.IsBoundedSubgroup setup.bornGt Ω' ∧ ↑H = productSetOmegaPrimeK₀ setup.gbnpair Ω' K₀_data.K ∧ ∀ t ∈ Ω', ∀ (σ : Equiv.Perm B_idx), (∀ (s : B_idx) (n : ↥setup.gbnpair.strictBNPair.N), setup.gbnpair.strictBNPair.π n = M.toCoxeterSystem.simple s → ∃ (n' : ↥setup.gbnpair.strictBNPair.N), setup.gbnpair.strictBNPair.π n' = M.toCoxeterSystem.simple (σ s) ∧ ↑↑n' = t * ↑↑n * t⁻¹) → PermStabilizesSx M K₀_data.vertex σ

Existence of good maximal bounded subgroups in $G^t$: every good bounded setup yields a bounded subgroup $H = \Omega' K_0$ of $G^t$ where $K_0 \leq G$ is a good maximal bounded subgroup and $\Omega' \leq T^t$ is a bounded subgroup whose conjugation action stabilises $S \setminus \{s_0\}$.