theorem CellDisjoint.simple_inv_eq {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (cs : CoxeterSystem M M.Group) (s : B_idx) : (cs.simple s)⁻¹ = cs.simple s

Simple reflections are involutions: $s^{-1} = s$.

theorem CellDisjoint.simple_ne_one {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (cs : CoxeterSystem M M.Group) (s : B_idx) : cs.simple s ≠ 1

Simple reflections have length one, hence are nontrivial: $s \neq 1$.

theorem CellDisjoint.eq_one_of_mem_B_and_bruhatCell {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {g : G} {w : M.Group} (hg_B : g ∈ bp.B) (hg_w : g ∈ bp.bruhatCell w) : w = 1

If $g \in B \cap C(w)$ then $w = 1$. The unique cell containing $B$-elements is $C(1)$.

theorem CellDisjoint.bruhatCell_one_sub_B' {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {g : G} (hg : g ∈ bp.bruhatCell 1) : g ∈ bp.B

The identity Bruhat cell coincides with $B$: $C(1) \subseteq B$.

theorem CellDisjoint.mul_simple_simple_self {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (cs : CoxeterSystem M M.Group) (w : M.Group) (s : B_idx) : w * cs.simple s * cs.simple s = w

Double simple cancellation: $w \cdot s \cdot s = w$ for any simple reflection $s$.

theorem CellDisjoint.cell_decomp {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {w : M.Group} {g : G} (hg : g ∈ bp.bruhatCell w) (s : B_idx) (_hlen : M.toCoxeterSystem.length (w * M.toCoxeterSystem.simple s) < M.toCoxeterSystem.length w) : ∃ a ∈ bp.bruhatCell (w * M.toCoxeterSystem.simple s), ∃ b ∈ bp.bruhatCell (M.toCoxeterSystem.simple s), g = a * b

Cell decomposition: when $\ell(ws) < \ell(w)$, every $g \in C(w)$ factors as $g = a \cdot b$ with $a \in C(ws)$ and $b \in C(s)$.

theorem CellDisjoint.inv_mem_bruhatCell_simple {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {b : G} {s : B_idx} (hb : b ∈ bp.bruhatCell (M.toCoxeterSystem.simple s)) : b⁻¹ ∈ bp.bruhatCell (M.toCoxeterSystem.simple s)

$C(s)$ is closed under inversion since $s^{-1} = s$: $b \in C(s) \Rightarrow b^{-1} \in C(s)$.

theorem CellDisjoint.mem_setMul_of_mem_cells {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {w : M.Group} {s : B_idx} {x y : G} (hx : x ∈ bp.bruhatCell w) (hy : y ∈ bp.bruhatCell (M.toCoxeterSystem.simple s)) : x * y ∈ setMul (bp.bruhatCell w) (bp.bruhatCell (M.toCoxeterSystem.simple s))

Trivial packaging: $xy \in C(w) \cdot C(s)$ when $x \in C(w)$ and $y \in C(s)$.

theorem CellDisjoint.cell_disjoint_from_bnpair {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (w w' : M.Group) (h : (bp.bruhatCell w ∩ bp.bruhatCell w').Nonempty) : w = w'

Bruhat cell disjointness: distinct Bruhat cells are disjoint, i.e. $C(w) \cap C(w') \neq \emptyset \Rightarrow w = w'$. Together with cell_cover_from_bnpair, this yields $G = \bigsqcup_{w \in W} BwB$.