ParabolicCore.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The normal core of every proper parabolic in irreducible type is trivial. The arbitrary-intersection theorem also supplies a finite list of conjugates realizing this core. These are the algebraic inputs to the tree argument.

lemma OAI.HarmonicArtin.ParabolicIntersections.normalCore_eq_sInf_conjugates line 14
theorem OAI.HarmonicArtin.ParabolicIntersections.normal_parabolic line 26
Source documentation
The conjugate form of CMMW Lemma 3.3.
```
theorem normal_parabolic (hIrred : IsIrreducible M)
    (P : Subgroup (Artin M)) (hP : IsParabolic M P) (hn : P.Normal) :
    P=⊥ ∨ P=⊤ := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.parabolic_normalCore_eq_bot line 41
Source documentation
No nontrivial normal subgroup obtained as a parabolic can lie in a proper parabolic of an irreducible Artin group.
```
theorem parabolic_normalCore_eq_bot (hIrred : IsIrreducible M)
    (P : Subgroup (Artin M)) (hP : IsParabolic M P) (hproper : P≠⊤) :
    P.normalCore=⊥ := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.finite_conjugates_inf_bot line 55
Source documentation
A bounded finite family of conjugates has trivial intersection. This is used to find a finite subtree with trivial pointwise stabilizer.
```
theorem finite_conjugates_inf_bot (hIrred : IsIrreducible M)
    (P : Subgroup (Artin M)) (hP : IsParabolic M P) (hproper : P≠⊤) :
    ∃ F : Finset (Subgroup (Artin M)),
      (∀ Q∈F, ∃ g : Artin M, Q=conjugate g P) ∧ F.card≤Nat.card S ∧
        sInf (↑F : Set (Subgroup (Artin M)))=⊥ := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic