RankReduction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Rank descent restricted to the subgroup of colors avoiding the frame.

theorem OAI.HarmonicArtin.ParabolicIntersections.relativeStabilizers_of_reductions_on line 12
Source documentation
The induction keeps the transported point inside the prescribed orbit. This permits the extra frame color in the relative diagram to remain fixed.
```
theorem relativeStabilizers_of_reductions_on (U : Set S)
    (hred : ∀ Y : Set S, Y ⊆ U → ∀ x : Artin M, x ∈ artinParabolic M U →
      ReductionAt M v Y x)
    (Y : Set S) (hYU : Y ⊆ U) (x : Artin M) (hx : x ∈ artinParabolic M U) :
    ∃ (R : Set S) (c : Artin M), R ⊆ Y ∧ c ∈ artinParabolic M Y ∧
      relativeStabilizer M v Y x = conjugate c⁻¹ (artinParabolic M R) := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.ReductionAt, OAI.HarmonicArtin.ParabolicIntersections.relativeStabilizer