CoxeterProjectionSupport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Parabolic projection preserves any standard subgroup containing its input.

lemma OAI.HarmonicArtin.ParabolicIntersections.component_one line 11
lemma OAI.HarmonicArtin.ParabolicIntersections.rep_mem_of_component_mem line 18
lemma OAI.HarmonicArtin.ParabolicIntersections.component_step_mem line 26
theorem OAI.HarmonicArtin.ParabolicIntersections.component_mem_of_mem line 46
Source documentation
The parabolic component of an element of W_C is again in W_C.
```
theorem component_mem_of_mem (X C : Set S) (w : W) (hw : w∈parabolic cs C) :
    parabolicComponent cs X w∈parabolic cs C := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.parabolicComponent
theorem OAI.HarmonicArtin.ParabolicIntersections.rep_mem_of_mem line 61
Source documentation
The canonical minimal representative also stays in W_C.
```
theorem rep_mem_of_mem (X C : Set S) (w : W) (hw : w∈parabolic cs C) :
    parabolicRep cs X w∈parabolic cs C :=
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.parabolicRep

theorem OAI.HarmonicArtin.ParabolicIntersections.minimum_not_product line 66

Source documentation

A minimal left representative outside W_C cannot lie in W_X W_C.

theorem minimum_not_product (X C : Set S) (w : W) (hmin : IsParabolicMinimum cs X w)
    (hw : w∉parabolic cs C) (a b : W) (ha : a∈parabolic cs X) (hb : b∈parabolic cs C) :
    w≠a*b := by
…