RelativePoset.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The connected poset of actual spherical cosets inside a fixed standard coset.

abbrev OAI.HarmonicArtin.ParabolicIntersections.RelativeVertex line 11
def OAI.HarmonicArtin.ParabolicIntersections.relativeAdjacent line 14
abbrev OAI.HarmonicArtin.ParabolicIntersections.RelativePath line 17
def OAI.HarmonicArtin.ParabolicIntersections.relativeVertex line 20
def OAI.HarmonicArtin.ParabolicIntersections.relativeElement line 24
lemma OAI.HarmonicArtin.ParabolicIntersections.relativeElement_le line 28
lemma OAI.HarmonicArtin.ParabolicIntersections.relativePath_symm line 36
lemma OAI.HarmonicArtin.ParabolicIntersections.relative_generator_step line 43
lemma OAI.HarmonicArtin.ParabolicIntersections.relative_element_connected line 66
Source documentation
Left multiplication by a word in the ambient standard subgroup gives an explicit comparability path through rank-one cosets.
```
lemma relative_element_connected (Y : Set S) (x g : Artin M)
    (hg : g ∈ artinParabolic M Y) :
    RelativePath M (relativeElement M Y x x (rightCoset_self M Y x))
      (relativeElement M Y x (g*x) (by
        change (g*x)*x⁻¹ ∈ artinParabolic M Y
        simpa only [_root_.mul_assoc, mul_inv_cancel, _root_.mul_one] using hg)) := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.RelativePath, OAI.HarmonicArtin.ParabolicIntersections.relativeElement, OAI.HarmonicArtin.rightCoset_self
theorem OAI.HarmonicArtin.ParabolicIntersections.relative_poset_connected line 95
Source documentation
The relative spherical-coset poset is connected, without assuming that its ambient type is spherical.
```
theorem relative_poset_connected (Y : Set S) (x : Artin M)
    (P R : RelativeVertex M Y x) : RelativePath M P R := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.RelativeVertex, OAI.HarmonicArtin.ParabolicIntersections.RelativePath