OAI/Topology/ArtinGroups/ParabolicIntersections/StandardEmbedding.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Injectivity of every finite-rank standard Artin parabolic.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.component_of_parabolic line 15
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicStepLetter_standard line 25
  3. def OAI.HarmonicArtin.ParabolicIntersections.parabolicState line 44
  4. theorem OAI.HarmonicArtin.ParabolicIntersections.parabolicRetractionAction_standard line 48

    Source documentation

    On the standard parabolic, the gallery action is its right regular action.

    theorem parabolicRetractionAction_standard (g a : Artin R) :
    MulOpposite.unop (parabolicRetractionAction M J (restrictedArtinHom M J g))
      (parabolicState M J a)=parabolicState M J (a*g) := by
…

    Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.parabolicRetractionAction, OAI.HarmonicArtin.restrictedArtinHom, OAI.HarmonicArtin.ParabolicIntersections.parabolicState

  5. theorem OAI.HarmonicArtin.ParabolicIntersections.standardArtinEmbedding line 82

    Source documentation

    Van der Lek's standard-parabolic injectivity theorem in finite rank, proved from the Coxeter retraction and the Artin braid presentation.

    theorem standardArtinEmbedding : Function.Injective (restrictedArtinHom M J) := by
…

    Mentions: OAI.HarmonicArtin.restrictedArtinHom