OAI/Topology/ArtinGroups/ParabolicIntersections/ParabolicCosetProjection.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Canonical minimal coset representatives and their parabolic components.

  1. theorem OAI.HarmonicArtin.ParabolicIntersections.exists_minimum_rep line 12
  2. def OAI.HarmonicArtin.ParabolicIntersections.parabolicRep line 17
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicRep_min line 20
  4. def OAI.HarmonicArtin.ParabolicIntersections.parabolicComponent line 23
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicComponent_mul_rep line 25
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicComponent_mem line 29
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicRep_eq_of_decomposition line 36
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicRep_of_minimum line 47
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicRep_left_mul line 51
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicComponent_left_mul line 58
  11. def OAI.HarmonicArtin.ParabolicIntersections.parabolicStepRatio line 62
  12. theorem OAI.HarmonicArtin.ParabolicIntersections.parabolicStepRatio_cases line 66

    Source documentation

    The component changes by either no letter or a simple letter of J.

    theorem parabolicStepRatio_cases (w : W) (s : S) :
    parabolicStepRatio cs J w s=1 ∨
      ∃ t : J, parabolicStepRatio cs J w s=cs.simple t := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.parabolicStepRatio

  13. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicStepRatio_one_of_minimum line 93
  14. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicStepRatio_reflection line 104
  15. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicStepRatio_reverse line 120