OAI/Topology/ArtinGroups/ParabolicIntersections/GeneratorPowers.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Infinite cyclic generator subgroups and their intersections with standard parabolics. The retraction argument supplies infinite branching in visual trees.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.exponent_alternating line 12
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.exponent_relators line 23
  3. def OAI.HarmonicArtin.ParabolicIntersections.artinExponent line 29

    Source documentation

    The total exponent homomorphism for the Artin presentation.

    def artinExponent : Artin M →* Multiplicative ℤ :=
…

    Mentions: OAI.HarmonicArtin.Artin

  4. lemma OAI.HarmonicArtin.ParabolicIntersections.artinExponent_generator line 32
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.generator_zpow_eq_one_iff line 36
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicStepLetter_one_outside line 51
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicStepArtin_one_outside line 63
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.generator_power_retraction line 69

    Source documentation

    Every integral power of an outside generator has trivial parabolic read.

    lemma generator_power_retraction (t : S) (ht : t∉J) (n : ℤ) :
    (MulOpposite.unop (parabolicRetractionAction M J (generator M t ^ n))
      (1,1)).2=1 := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.parabolicRetractionAction, OAI.HarmonicArtin.generator

  9. theorem OAI.HarmonicArtin.ParabolicIntersections.generator_zpow_not_mem line 112

    Source documentation

    A nonzero power of an omitted generator never lies in a standard parabolic.

    theorem generator_zpow_not_mem (t : S) (ht : t∉J) (n : ℤ) (hn : n≠0) :
    generator M t ^ n∉artinParabolic M J := by
…

    Mentions: OAI.HarmonicArtin.generator, OAI.HarmonicArtin.artinParabolic