Consequences.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Consequences of the inside-parabolic intersection theorem

These are the deductions in the introduction of paper 082-03. The premise InsideIntersectionProperty is a new result of that paper, not a published input and not an established instance. These deductions alone do not constitute a formalization of its main intersection theorem.

def OAI.HarmonicArtin.ParabolicIntersections.InsideIntersectionProperty line 20
Source documentation
The inside-parabolic conclusion of §8. Its proof, for arbitrary Artin matrices, must come from the relative stabilizer argument.
```
def InsideIntersectionProperty : Prop :=
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.inside_conjugate line 26
theorem OAI.HarmonicArtin.ParabolicIntersections.pairwise_of_inside line 40
Source documentation
The exact pairwise statement of Theorem 1.1, deduced from its stronger inside-parabolic form. The hypothesis still needs to be proved.
```
theorem pairwise_of_inside (h : InsideIntersectionProperty M)
    (X Y : Set S) (g a : Artin M) :
    ∃ (Z : Set S) (k : Artin M),
      conjugate g (artinParabolic M X) ⊓ conjugate a (artinParabolic M Y) =
        conjugate k (artinParabolic M Z) := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.InsideIntersectionProperty, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.isParabolic_inf line 49
theorem OAI.HarmonicArtin.ParabolicIntersections.insert_intersection line 56

theorem OAI.HarmonicArtin.ParabolicIntersections.finite_subfamily_aux line 67

Source documentation

The descent uses the displayed type, so no separate theorem asserting that parabolic rank is invariant under conjugation is required.

private theorem finite_subfamily_aux (h : InsideIntersectionProperty M)
    (F : Set (Subgroup (Artin M))) (hF : ∀ P ∈ F, IsParabolic M P) :
    ∀ n : ℕ, ∀ (X : Set S), X.ncard = n → ∀ g : Artin M,
      ∃ F₀ : Finset (Subgroup (Artin M)),
        (↑F₀ : Set (Subgroup (Artin M))) ⊆ F ∧ F₀.card ≤ n ∧
        conjugate g (artinParabolic M X) ⊓ sInf F =
          conjugate g (artinParabolic M X) ⊓ sInf (↑F₀ : Set (Subgroup (Artin M))) ∧
        IsParabolic M (conjugate g (artinParabolic M X) ⊓ sInf F) := by
…

Mentions: OAI.HarmonicArtin.ParabolicIntersections.InsideIntersectionProperty, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic, OAI.HarmonicArtin.artinParabolic

theorem OAI.HarmonicArtin.ParabolicIntersections.arbitrary_intersections_of_inside line 123
Source documentation
The full subfamily bound in Corollary 1.2, including the empty family. This is conditional on the new inside-intersection theorem, explicitly.
```
theorem arbitrary_intersections_of_inside (h : InsideIntersectionProperty M)
    (F : Set (Subgroup (Artin M))) (hF : ∀ P ∈ F, IsParabolic M P) :
    (∃ F₀ : Finset (Subgroup (Artin M)),
      (↑F₀ : Set (Subgroup (Artin M))) ⊆ F ∧ F₀.card ≤ Nat.card S ∧
        sInf F = sInf (↑F₀ : Set (Subgroup (Artin M)))) ∧
    IsParabolic M (sInf F) := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.InsideIntersectionProperty, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.parabolic_closure_of_inside line 136
Source documentation
The unique smallest parabolic containing an arbitrary subset, rather than merely a smallest parabolic containing a finite set.
```
theorem parabolic_closure_of_inside (h : InsideIntersectionProperty M)
    (E : Set (Artin M)) :
    ∃! P : Subgroup (Artin M), IsParabolic M P ∧ E ⊆ P ∧
      ∀ Q : Subgroup (Artin M), IsParabolic M Q → E ⊆ Q → P ≤ Q := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.InsideIntersectionProperty, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic