CosetContainment.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Confining paths of parabolic cosets

This is the coset argument in Proposition 6.9 of paper 082-03. A path whose types stay in one set cannot escape its standard coset. The proof uses actual subgroup cosets, including upward as well as downward edges.

theorem OAI.HarmonicArtin.ParabolicIntersections.rightCoset_subset_of_point line 20
Source documentation
A smaller-type coset through a point of a larger-type coset is contained in that larger coset.
```
theorem rightCoset_subset_of_point {T D : Set S} (hTD : T ⊆ D)
    {w z : Artin M} (hw : w ∈ rightCoset M D z) :
    rightCoset M T w ⊆ rightCoset M D z := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.rightCoset
theorem OAI.HarmonicArtin.ParabolicIntersections.deligne_coset_eq_at_point line 31
Source documentation
A represented parabolic coset can be recentered at each of its points.
```
theorem deligne_coset_eq_at_point (P : Deligne M) (w : Artin M) (hw : w ∈ P.val.2) :
    P.val.2 = rightCoset M P.val.1 w := by
…
```
Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.rightCoset
theorem OAI.HarmonicArtin.ParabolicIntersections.deligne_upper_contained line 43
Source documentation
Upward comparability preserves containment when the larger type is still contained in the specified standard type.
```
theorem deligne_upper_contained {P R : Deligne M} (hPR : P ≤ R)
    (D : Set S) (z : Artin M) (hR : R.val.1 ⊆ D)
    (hP : P.val.2 ⊆ rightCoset M D z) : R.val.2 ⊆ rightCoset M D z := by
…
```
Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.rightCoset
theorem OAI.HarmonicArtin.ParabolicIntersections.deligne_path_contained line 58
Source documentation
Every coset on a finite comparability path with types in D stays inside the starting D-coset. This is the path confinement used at a minimum of the relative height.
```
theorem deligne_path_contained (D : Set S) (z : Artin M) {P R : Deligne M}
    (hP : P.val.2 ⊆ rightCoset M D z)
    (path : Relation.ReflTransGen
      (fun A B : Deligne M => A.val.1 ⊆ D ∧ B.val.1 ⊆ D ∧ (A ≤ B ∨ B ≤ A)) P R) :
    R.val.2 ⊆ rightCoset M D z := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.rightCoset

theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_membership_of_coset_path line 72

Source documentation

If a confined path reaches the translate of its starting coset by r, then r belongs to the corresponding conjugate standard subgroup.

theorem conjugate_membership_of_coset_path (D : Set S) (z r : Artin M)
    {P R : Deligne M} (hP : z ∈ P.val.2) (hPT : P.val.1 ⊆ D)
    (hR : z * r ∈ R.val.2)
    (path : Relation.ReflTransGen
      (fun A B : Deligne M => A.val.1 ⊆ D ∧ B.val.1 ⊆ D ∧ (A ≤ B ∨ B ≤ A)) P R) :
    r ∈ conjugate z⁻¹ (artinParabolic M D) := by
…

Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.artinParabolic