Bruhat order #

This file defines the Bruhat order.

Main definitions #

Coxeter.le : The Bruhat order
Coxeter.w₀ : The longest element

Main statements #

References #

[BB05] A. Björner and F. Brenti, Combinatorics of Coxeter Groups

source

inductive Coxeter.le {W : Type u_1} [CoxeterGroup W] :

W → W → Prop

rfl {W : Type u_1} [CoxeterGroup W] (u : W) : le u u
step {W : Type u_1} [CoxeterGroup W] (u v w : W) (h1 : le u v) (h2 : CoxeterGroup.cs.IsReflection (w * v⁻¹)) (h3 : CoxeterGroup.cs.length v < CoxeterGroup.cs.length w) : le u w

Instances For

source

@[implicit_reducible]

instance Coxeter.instLE_coxeter {W : Type u_1} [CoxeterGroup W] :

LE W

Equations

Coxeter.instLE_coxeter = { le := Coxeter.le }

source

theorem Coxeter.length_le_of_le {W : Type u_1} [CoxeterGroup W] {u w : W} (h : u ≤ w) :

CoxeterGroup.cs.length u ≤ CoxeterGroup.cs.length w

source

theorem Coxeter.eq_of_le_of_length_ge {W : Type u_1} [CoxeterGroup W] {u w : W} (h : u ≤ w) (h2 : CoxeterGroup.cs.length u ≥ CoxeterGroup.cs.length w) :

u = w

source

theorem Coxeter.eq_of_le_of_length_eq {W : Type u_1} [CoxeterGroup W] {u w : W} (h : u ≤ w) (h2 : CoxeterGroup.cs.length u = CoxeterGroup.cs.length w) :

u = w

source

def Coxeter.lt {W : Type u_1} [CoxeterGroup W] (u w : W) :

Prop

Equations

Coxeter.lt u w = (u ≤ w ∧ u ≠ w)

Instances For

source

@[implicit_reducible]

instance Coxeter.instLT_coxeter {W : Type u_1} [CoxeterGroup W] :

LT W

Equations

Coxeter.instLT_coxeter = { lt := Coxeter.lt }

source

theorem Coxeter.lt_iff_le_and_length_lt {W : Type u_1} [CoxeterGroup W] (u w : W) :

u < w ↔ u ≤ w ∧ CoxeterGroup.cs.length u < CoxeterGroup.cs.length w

source

@[implicit_reducible]

instance Coxeter.instPartialOrder_coxeter {W : Type u_1} [CoxeterGroup W] :

PartialOrder W

Equations

Coxeter.instPartialOrder_coxeter = { toLE := Coxeter.instLE_coxeter, toLT := Coxeter.instLT_coxeter, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

source

theorem Coxeter.monotone_length {W : Type u_1} [CoxeterGroup W] :

Monotone CoxeterGroup.cs.length

source

theorem Coxeter.strictMono_length {W : Type u_1} [CoxeterGroup W] :

StrictMono CoxeterGroup.cs.length

source

theorem Coxeter.reflection_mul_lt_self_iff {W : Type u_1} [CoxeterGroup W] {t : W} (ht : CoxeterGroup.cs.IsReflection t) (w : W) :

t * w < w ↔ CoxeterGroup.cs.IsLeftInversion w t

source

theorem Coxeter.lt_reflection_mul_self_iff {W : Type u_1} [CoxeterGroup W] {t : W} (ht : CoxeterGroup.cs.IsReflection t) (w : W) :

w < t * w ↔ ¬CoxeterGroup.cs.IsLeftInversion w t

source

theorem Coxeter.mul_reflection_lt_self_iff {W : Type u_1} [CoxeterGroup W] {t : W} (ht : CoxeterGroup.cs.IsReflection t) (w : W) :

w * t < w ↔ CoxeterGroup.cs.IsRightInversion w t

source

theorem Coxeter.lt_self_mul_reflection_iff {W : Type u_1} [CoxeterGroup W] {t : W} (ht : CoxeterGroup.cs.IsReflection t) (w : W) :

w < w * t ↔ ¬CoxeterGroup.cs.IsRightInversion w t

source

theorem Coxeter.simple_mul_lt_self_iff {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (w : W) :

CoxeterGroup.cs.simple i * w < w ↔ CoxeterGroup.cs.IsLeftDescent w i

source

theorem Coxeter.lt_simple_mul_self_iff {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (w : W) :

w < CoxeterGroup.cs.simple i * w ↔ ¬CoxeterGroup.cs.IsLeftDescent w i

source

theorem Coxeter.mul_simple_lt_self_iff {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (w : W) :

w * CoxeterGroup.cs.simple i < w ↔ CoxeterGroup.cs.IsRightDescent w i

source

theorem Coxeter.lt_self_mul_simple_iff {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (w : W) :

w < w * CoxeterGroup.cs.simple i ↔ ¬CoxeterGroup.cs.IsRightDescent w i

source

theorem Coxeter.reflection_mul_lt_or_gt_self {W : Type u_1} [CoxeterGroup W] (w : W) {t : W} (ht : CoxeterGroup.cs.IsReflection t) :

t * w < w ∨ t * w > w

source

theorem Coxeter.mul_reflection_lt_or_gt_self {W : Type u_1} [CoxeterGroup W] (w : W) {t : W} (ht : CoxeterGroup.cs.IsReflection t) :

w * t < w ∨ w * t > w

source

@[implicit_reducible]

instance Coxeter.instOrderBot_coxeter {W : Type u_1} [CoxeterGroup W] :

OrderBot W

Equations

Coxeter.instOrderBot_coxeter = { bot := 1, bot_le := ⋯ }

source

theorem Coxeter.reduced_subword_extend {W : Type u_1} [CoxeterGroup W] {u w : W} (ω : ReducedWord w) (h1 : u ≠ w) (h2 : ∃ (μ : ReducedWord u), (↑μ).Sublist ↑ω) :

∃ v > u, CoxeterGroup.cs.length v = CoxeterGroup.cs.length u + 1 ∧ ∃ (ν : ReducedWord v), (↑ν).Sublist ↑ω

Bjorner--Brenti Lemma 2.2.1

source

theorem Coxeter.exists_reduced_subword_of_le {W : Type u_1} [CoxeterGroup W] {u w : W} (ω : ReducedWord w) (h : u ≤ w) :

∃ (μ : ReducedWord u), (↑μ).Sublist ↑ω

source

theorem Coxeter.le_of_reduced_subword {W : Type u_1} [CoxeterGroup W] {u w : W} (μ : ReducedWord u) (ω : ReducedWord w) (h : (↑μ).Sublist ↑ω) :

u ≤ w

source

theorem Coxeter.subword_property {W : Type u_1} [CoxeterGroup W] (u : W) {w : W} (ω : ReducedWord w) :

u ≤ w ↔ ∃ (μ : ReducedWord u), (↑μ).Sublist ↑ω

Bjorner--Brenti Theorem 2.2.2

source

theorem Coxeter.subword_property' {W : Type u_1} [CoxeterGroup W] {u w : W} :

u ≤ w ↔ ∃ (μ : ReducedWord u) (ω : ReducedWord w), (↑μ).Sublist ↑ω

Bjorner--Brenti Corollary 2.2.3 (i) iff (iii)

source

theorem Coxeter.finite_Icc {W : Type u_1} [CoxeterGroup W] (u w : W) :

Finite ↑(Set.Icc u w)

source

@[implicit_reducible]

noncomputable instance Coxeter.instLocallyFiniteOrder_coxeter {W : Type u_1} [CoxeterGroup W] :

LocallyFiniteOrder W

Equations

Coxeter.instLocallyFiniteOrder_coxeter = LocallyFiniteOrder.ofFiniteIcc ⋯

source

theorem Coxeter.card_Icc_le {W : Type u_1} [CoxeterGroup W] (u w : W) :

(Finset.Icc u w).card ≤ 2 ^ CoxeterGroup.cs.length w

Bjorner--Brenti Corollary 2.2.4

source

theorem Coxeter.monotone_inv {W : Type u_1} [CoxeterGroup W] :

Monotone Inv.inv

Bjorner--Brenti Corollary 2.2.5

source

theorem Coxeter.strictMono_inv {W : Type u_1} [CoxeterGroup W] :

StrictMono Inv.inv

source

theorem Coxeter.length_cover {W : Type u_1} [CoxeterGroup W] {u w : W} (h : u ⋖ w) :

CoxeterGroup.cs.length u + 1 = CoxeterGroup.cs.length w

source

@[implicit_reducible]

noncomputable instance Coxeter.instGradeMinOrderNat_coxeter {W : Type u_1} [CoxeterGroup W] :

GradeMinOrder ℕ W

Equations

Coxeter.instGradeMinOrderNat_coxeter = { grade := Coxeter.CoxeterGroup.cs.length, grade_strictMono := ⋯, covBy_grade := ⋯, isMin_grade := ⋯ }

source

instance Coxeter.instIsStronglyAtomic_coxeter {W : Type u_1} [CoxeterGroup W] :

IsStronglyAtomic W

source

theorem Coxeter.covBy_iff {W : Type u_1} [CoxeterGroup W] {u w : W} :

u ⋖ w ↔ u ≤ w ∧ CoxeterGroup.cs.length u + 1 = CoxeterGroup.cs.length w

Bjorner--Brenti Theorem 2.2.6

source

theorem Coxeter.simple_mul_covBy_self_iff {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (w : W) :

CoxeterGroup.cs.simple i * w ⋖ w ↔ CoxeterGroup.cs.IsLeftDescent w i

source

theorem Coxeter.covBy_simple_mul_self_iff {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (w : W) :

w ⋖ CoxeterGroup.cs.simple i * w ↔ ¬CoxeterGroup.cs.IsLeftDescent w i

source

theorem Coxeter.mul_simple_covBy_self_iff {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (w : W) :

w * CoxeterGroup.cs.simple i ⋖ w ↔ CoxeterGroup.cs.IsRightDescent w i

source

theorem Coxeter.covBy_self_mul_simple_iff {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (w : W) :

w ⋖ w * CoxeterGroup.cs.simple i ↔ ¬CoxeterGroup.cs.IsRightDescent w i

source

theorem Coxeter.lifting_property {W : Type u_1} [CoxeterGroup W] {u w : W} {i : CoxeterGroup.B W} (h1 : u ≤ w) (h2 : CoxeterGroup.cs.IsLeftDescent w i) (h3 : ¬CoxeterGroup.cs.IsLeftDescent u i) :

u ≤ CoxeterGroup.cs.simple i * w ∧ CoxeterGroup.cs.simple i * u ≤ w

Bjorner--Brenti Proposition 2.2.7

source

theorem Coxeter.local_configuration {W : Type u_1} [CoxeterGroup W] {i : CoxeterGroup.B W} {t w : W} (h : CoxeterGroup.cs.simple i ≠ t) (h2 : w ⋖ CoxeterGroup.cs.simple i * w) (h3 : w ⋖ t * w) :

CoxeterGroup.cs.simple i * w ⋖ CoxeterGroup.cs.simple i * t * w ∧ t * w ⋖ CoxeterGroup.cs.simple i * t * w

Bjorner--Brenti Corollary 2.2.8 (i)

source

theorem Coxeter.local_configuration₂ {W : Type u_1} [CoxeterGroup W] {i i' : CoxeterGroup.B W} {w : W} (h : w ⋖ CoxeterGroup.cs.simple i * w) (h2 : w ⋖ w * CoxeterGroup.cs.simple i') :

CoxeterGroup.cs.simple i * w ⋖ CoxeterGroup.cs.simple i * w * CoxeterGroup.cs.simple i' ∧ w * CoxeterGroup.cs.simple i' ⋖ CoxeterGroup.cs.simple i * w * CoxeterGroup.cs.simple i' ∨ w = CoxeterGroup.cs.simple i * w * CoxeterGroup.cs.simple i'

Bjorner--Brenti Corollary 2.2.8 (ii)

source

instance Coxeter.instIsDirectedOrder_coxeter {W : Type u_1} [CoxeterGroup W] :

IsDirectedOrder W

Bjorner--Brenti Proposition 2.2.9

Bruhat order on finite Coxeter groups #

source

theorem Coxeter.isTop_iff_all_isLeftDescent {W : Type u_1} [CoxeterGroup W] {x : W} :

(∀ (i : CoxeterGroup.B W), CoxeterGroup.cs.IsLeftDescent x i) ↔ IsTop x

source

theorem Coxeter.finite_of_orderTop {W : Type u_1} [CoxeterGroup W] [OrderTop W] :

Finite W

source

theorem Coxeter.finite_of_exists_all_isLeftDescent {W : Type u_1} [CoxeterGroup W] (h : ∃ (x : W), ∀ (i : CoxeterGroup.B W), CoxeterGroup.cs.IsLeftDescent x i) :

Finite W

Bjorner--Brenti Proposition 2.3.1 (ii)

source

@[implicit_reducible]

noncomputable instance Coxeter.instOrderTop_coxeter_1 {W : Type u_1} [CoxeterGroup W] [Finite W] :

OrderTop W

Bjorner--Brenti Proposition 2.3.1 (i)

Equations

Coxeter.instOrderTop_coxeter_1 = inferInstance

source

noncomputable def Coxeter.w₀ {W : Type u_1} [CoxeterGroup W] [Finite W] :

Equations

Coxeter.w₀ = ⊤

Instances For

source

theorem Coxeter.all_isLeftDescent_iff {W : Type u_1} [CoxeterGroup W] [Finite W] (x : W) :

(∀ (i : CoxeterGroup.B W), CoxeterGroup.cs.IsLeftDescent x i) ↔ x = w₀

Bjorner--Brenti Proposition 2.3.1 (ii) continued

source

theorem Coxeter.length_le_length_w₀ {W : Type u_1} [CoxeterGroup W] [Finite W] (x : W) :

CoxeterGroup.cs.length x ≤ CoxeterGroup.cs.length w₀

source

theorem Coxeter.eq_w₀_of_length_ge {W : Type u_1} [CoxeterGroup W] [Finite W] {x : W} (h : CoxeterGroup.cs.length x ≥ CoxeterGroup.cs.length w₀) :

x = w₀

source

theorem Coxeter.eq_w₀_of_length_eq {W : Type u_1} [CoxeterGroup W] [Finite W] {x : W} (h : CoxeterGroup.cs.length x = CoxeterGroup.cs.length w₀) :

x = w₀

source

@[simp]

theorem Coxeter.inv_w₀ {W : Type u_1} [CoxeterGroup W] [Finite W] :

w₀ ⁻¹ = w₀

source

@[simp]

theorem Coxeter.w₀_mul_self {W : Type u_1} [CoxeterGroup W] [Finite W] :

w₀ * w₀ = 1

source

@[simp]

theorem Coxeter.w₀_sq {W : Type u_1} [CoxeterGroup W] [Finite W] :

w₀ ^ 2 = 1

Bjorner--Brenti Proposition 2.3.2 (i)

source

theorem Coxeter.length_mul_w₀ {W : Type u_1} [CoxeterGroup W] [Finite W] (w : W) :

CoxeterGroup.cs.length (w * w₀) = CoxeterGroup.cs.length w₀ - CoxeterGroup.cs.length w

Bjorner--Brenti Proposition 2.3.2 (ii)

source

theorem Coxeter.isLeftInversion_mul_w₀_iff {W : Type u_1} [CoxeterGroup W] [Finite W] {t : W} (ht : CoxeterGroup.cs.IsReflection t) (w : W) :

CoxeterGroup.cs.IsLeftInversion (w * w₀) t ↔ ¬CoxeterGroup.cs.IsLeftInversion w t

Bjorner--Brenti Proposition 2.3.2 (iii)

source

theorem Coxeter.isLeftInversion_w₀_iff {W : Type u_1} [CoxeterGroup W] [Finite W] (t : W) :

CoxeterGroup.cs.IsLeftInversion w₀ t ↔ CoxeterGroup.cs.IsReflection t

source

instance Coxeter.instFiniteReflectionSet {W : Type u_1} [CoxeterGroup W] [Finite W] :

Finite (ReflectionSet W)

source

theorem Coxeter.length_w₀_eq_card_reflectionSet {W : Type u_1} [CoxeterGroup W] [Finite W] :

CoxeterGroup.cs.length w₀ = Nat.card (ReflectionSet W)

Bjorner--Brenti Proposition 2.3.2 (iv)

source

theorem Coxeter.length_w₀_mul {W : Type u_1} [CoxeterGroup W] [Finite W] (w : W) :

CoxeterGroup.cs.length (w₀ * w) = CoxeterGroup.cs.length w₀ - CoxeterGroup.cs.length w

Bjorner--Brenti Corollary 2.3.3 (i)

source

theorem Coxeter.length_conj_w₀ {W : Type u_1} [CoxeterGroup W] [Finite W] (w : W) :

CoxeterGroup.cs.length ((MulAut.conj w₀) w) = CoxeterGroup.cs.length w

Bjorner--Brenti Corollary 2.3.3 (ii)

source

theorem Coxeter.antitone_mul_w₀ {W : Type u_1} [CoxeterGroup W] [Finite W] :

Antitone ⇑(Equiv.mulRight w₀)

Bjorner--Brenti Proposition 2.3.4 (i)

source

theorem Coxeter.strictAnti_mul_w₀ {W : Type u_1} [CoxeterGroup W] [Finite W] :

StrictAnti ⇑(Equiv.mulRight w₀)

source

theorem Coxeter.antitone_w₀_mul {W : Type u_1} [CoxeterGroup W] [Finite W] :

Antitone ⇑(Equiv.mulLeft w₀)

source

theorem Coxeter.strictAnti_w₀_mul {W : Type u_1} [CoxeterGroup W] [Finite W] :

StrictAnti ⇑(Equiv.mulLeft w₀)

source

theorem Coxeter.monotone_conj_w₀ {W : Type u_1} [CoxeterGroup W] [Finite W] :

Monotone ⇑(MulAut.conj w₀)

Bjorner--Brenti Proposition 2.3.4 (ii)

source

theorem Coxeter.strictMono_conj_w₀ {W : Type u_1} [CoxeterGroup W] [Finite W] :

StrictMono ⇑(MulAut.conj w₀)

Documentation

Coxeter.Bruhat

Bruhat order #

Main definitions #

Main statements #

References #

Bruhat order on finite Coxeter groups #