StabilizerDescent.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The rank induction in §8 of paper 082-03

The finite-rank induction is proved here for an actual group action. ReductionAt records the three alternatives that the paper obtains from its new relative-height arguments. It is deliberately not called a published input: constructing these alternatives for the categorical action is still required before this module implies the main theorem.

def OAI.HarmonicArtin.ParabolicIntersections.relativeStabilizer line 22
Source documentation
Stabilizer of the transported family, restricted to a standard subgroup. For a family of homotopy classes, take V to be the product of the classes.
```
def relativeStabilizer (Y : Set S) (x : Artin M) : Subgroup (Artin M) :=
…
```
Mentions: OAI.HarmonicArtin.Artin
theorem OAI.HarmonicArtin.ParabolicIntersections.mem_relativeStabilizer line 25
theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_stabilizer line 29
theorem OAI.HarmonicArtin.ParabolicIntersections.relativeStabilizer_conjugation line 39
Source documentation
Lemma 8.1: a containing smaller parabolic removes the ambient intersection after conjugation.
```
theorem relativeStabilizer_conjugation (Y D : Set S) (b x : Artin M)
    (hD : D ⊆ Y) (hb : b ∈ artinParabolic M Y)
    (hcontain : relativeStabilizer M v Y x ≤ conjugate b⁻¹ (artinParabolic M D)) :
    conjugate b (relativeStabilizer M v Y x) = relativeStabilizer M v D (b * x) := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.relativeStabilizer

inductive OAI.HarmonicArtin.ParabolicIntersections.ReductionAt line 58

Source documentation

The alternatives furnished by the spherical positive-height reduction and the nonspherical harmonic-minimum reduction. The split case expresses the invisible direct factor, including its normalization property.

inductive ReductionAt (Y : Set S) (x : Artin M) : Prop
  | fixed : relativeStabilizer M v Y x = artinParabolic M Y → ReductionAt Y x
  | smaller (D : Set S) (b : Artin M) :
      D ⊂ Y → b ∈ artinParabolic M Y →
      relativeStabilizer M v Y x ≤ conjugate b⁻¹ (artinParabolic M D) → ReductionAt Y x
  | split (T K : Set S) :
      T ⊂ Y → K ⊆ Y →
      (∀ c ∈ artinParabolic M T, conjugate c (artinParabolic M K) = artinParabolic M K) →
      relativeStabilizer M v Y x = artinParabolic M K ⊔ relativeStabilizer M v T x →
      ReductionAt Y x

variable [Finite S]

Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.relativeStabilizer, OAI.HarmonicArtin.artinParabolic

theorem OAI.HarmonicArtin.ParabolicIntersections.relativeStabilizers_of_reductions line 73
Source documentation
Theorem 8.2's rank induction. The genuinely new local alternatives are an explicit premise, so this is not advertised as the completed theorem.
```
theorem relativeStabilizers_of_reductions
    (hred : ∀ (Y : Set S) (x : Artin M), ReductionAt M v Y x)
    (Y : Set S) (x : Artin M) :
    ∃ (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.ParabolicIntersections.ReductionAt, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.relativeStabilizer
theorem OAI.HarmonicArtin.ParabolicIntersections.inside_at_of_action_reductions line 105
Source documentation
Once the relative categorical action has its initial stabilizer and local reductions, its stabilizer induction gives the inside intersection. Neither of those new categorical assertions is installed as an axiom.
```
theorem inside_at_of_action_reductions (X Y : Set S) (g : Artin M)
    (hinit : MulAction.stabilizer (Artin M) v = artinParabolic M X)
    (hred : ∀ (D : Set S) (x : Artin M), ReductionAt M v D x) :
    ∃ (R : Set S) (c : Artin M), R ⊆ Y ∧ c ∈ artinParabolic M Y ∧
      artinParabolic M Y ⊓ conjugate g (artinParabolic M X) =
        conjugate c (artinParabolic M R) := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.ReductionAt