OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeUpperComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Strict upper-neighbor comparisons for the relative height.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeHeight_eq_of_blocks line 12
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeHeight_eq_of_new_invisible line 20
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeUpper_inactive_le line 49
  4. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeUpper_descending_has_active line 100

    Source documentation

    Every descending upper neighbor adds an active color.

    theorem relativeUpper_descending_has_active {P R : Deligne M} (h : P < R)
    (he : relativeHeight M f U cutoff R < relativeHeight M f U cutoff P) :
    ∃ i ∈ R.val.1, i ∉ P.val.1 ∧ relativeColorActive M f U cutoff P i := by
…

    Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.ParabolicIntersections.relativeHeight, OAI.HarmonicArtin.ParabolicIntersections.relativeColorActive

  5. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeUpper_active_descending line 109

    Source documentation

    Closing a nonempty set of active colors strictly decreases the height.

    theorem relativeUpper_active_descending {P R : Deligne M} (h : P < R)
    (ha : ∀ i ∈ R.val.1, i ∉ P.val.1 → relativeColorActive M f U cutoff P i) :
    relativeHeight M f U cutoff R < relativeHeight M f U cutoff P := by
…

    Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.ParabolicIntersections.relativeColorActive, OAI.HarmonicArtin.ParabolicIntersections.relativeHeight