OAI/Topology/ArtinGroups/ParabolicIntersections/FoldingPositive.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Positive-monoid folding and its action on simple elements. These are proved from the Coxeter word theorem and the established folding geometry.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.folded_word_product line 18
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.folded_positive_relations line 29
  3. def OAI.HarmonicArtin.ParabolicIntersections.foldedPositiveHom line 43
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.foldedPositiveHom_generator line 47
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.foldedPositiveHom_word line 51
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.foldedPositiveHom_simpleLift line 58
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.folded_simple_atom_iff line 73

    Source documentation

    A left atom divides the folded simple element precisely when its original color divides the original simple element.

    theorem folded_simple_atom_iff (w : (R).Group) (α : Y × FusionLabel m) :
    PositivePrefix N (positiveGenerator N α)
      (foldedPositiveHom M Y hY (positiveSimpleLift R w)) ↔
    PositivePrefix R (positiveGenerator R α.1) (positiveSimpleLift R w) := by
…

    Mentions: OAI.HarmonicArtin.FusionLabel, OAI.HarmonicArtin.PositivePrefix, OAI.HarmonicArtin.positiveGenerator, OAI.HarmonicArtin.ParabolicIntersections.foldedPositiveHom, OAI.HarmonicArtin.positiveSimpleLift