OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeDiagram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The relative diagram in §2.1 of paper 082-03

Adjoin the color f, with label 2 to the chosen standard type X and label 3 to its complement. The existing fusion construction subsequently adjoins the universal auxiliary color o. The map on Artin presentations is constructed directly; no parabolic embedding theorem is assumed here.

  1. def OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix line 20
  2. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix_original line 46
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix_frame line 49
  4. theorem OAI.HarmonicArtin.ParabolicIntersections.alternating_lift_inclusion line 54
  5. theorem OAI.HarmonicArtin.ParabolicIntersections.relative_relators line 63
  6. def OAI.HarmonicArtin.ParabolicIntersections.relativeArtinHom line 81

    Source documentation

    The canonical homomorphism into the Artin group of the relative diagram.

    noncomputable def relativeArtinHom : Artin M →* Artin (relativeMatrix M X) :=
…

    Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix

  7. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeArtinHom_generator line 84
  8. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeArtinHom_parabolic line 91

    Source documentation

    Standard parabolics map onto the corresponding standard parabolics of the extended diagram. Injectivity is not needed for this identity.

    theorem relativeArtinHom_parabolic (Y : Set S) :
    (artinParabolic M Y).map (relativeArtinHom M X) =
      artinParabolic (relativeMatrix M X) (Sum.inl '' Y) := by
…

    Mentions: OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.relativeArtinHom, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix