OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeTranslation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Right translation of the relative coset poset by a transported stabilizer.

  1. def OAI.HarmonicArtin.ParabolicIntersections.deligneRightTranslate line 12
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.deligneRightTranslate_type line 16
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.mem_deligneRightTranslate line 20
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.deligneRightTranslate_mono line 28
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.deligneRightTranslate_inv line 35
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedFamily_transport_fixed line 43
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_translate_fixed line 51
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeHeight_congr line 65
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeHeight_translate_fixed line 86

    Source documentation

    A transported stabilizer preserves the complete relative height, including every sign-mask coordinate.

    lemma relativeHeight_translate_fixed (f : S) (U : Set (S ⊕ Unit)) (cutoff : ℤ)
    (x a : Artin M) (ha : pointedFamily M f (a*x) = pointedFamily M f x) (P : Deligne M) :
    relativeHeight M f U cutoff (deligneRightTranslate M P (x⁻¹*a*x)) =
      relativeHeight M f U cutoff P :=
…

    Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.pointedFamily, OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.ParabolicIntersections.relativeHeight, OAI.HarmonicArtin.ParabolicIntersections.deligneRightTranslate

  10. lemma OAI.HarmonicArtin.ParabolicIntersections.deligneRightTranslate_relative line 93
  11. def OAI.HarmonicArtin.ParabolicIntersections.relativeTranslate line 107