FixedFactor.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removing an invisible factor

The nonspherical branch of §8 of paper 082-03 splits off a standard factor fixing the entire family. This module proves that step for the actual subgroup lattice and group action. Pairwise label 2 is the precise commutation hypothesis; no product decomposition is assumed.

theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_eq_of_commute line 21
Source documentation
A subgroup centralized pointwise by an element is invariant under its conjugation.
```
theorem conjugate_eq_of_commute (P : Subgroup G) (g : G)
    (hc : ∀ a ∈ P, Commute a g) : conjugate g P = P := by
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.relativeStabilizer_fixed_factor line 48
Source documentation
A fixed commuting standard factor splits off from the simultaneous stabilizer. Surjectivity of the multiplication map suffices.
```
theorem relativeStabilizer_fixed_factor (K T : Set S) (x : Artin M)
    (hc : ∀ k ∈ K, ∀ t ∈ T, M k t = 2)
    (hfix : ∀ k ∈ artinParabolic M K, k • (x • v) = x • v) :
    relativeStabilizer M v (K ∪ T) x =
      artinParabolic M K ⊔ relativeStabilizer M v T x := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.relativeStabilizer
theorem OAI.HarmonicArtin.ParabolicIntersections.standard_factor_normalized line 76
Source documentation
The fixed factor is normalized by the complementary standard factor, as required by the rank induction.
```
theorem standard_factor_normalized (K T : Set S)
    (hc : ∀ k ∈ K, ∀ t ∈ T, M k t = 2)
    (t : Artin M) (ht : t ∈ artinParabolic M T) :
    conjugate t (artinParabolic M K) = artinParabolic M K :=
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic