OAI/Topology/ArtinGroups/ParabolicIntersections/VisualAmalgam.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The actual amalgamated-product presentation of a visual splitting. The factors and edge group are the standard subgroups of the given Artin group, and the inverse homomorphism is constructed from its braid relators.

  1. def OAI.HarmonicArtin.ParabolicIntersections.visualSide line 16
  2. def OAI.HarmonicArtin.ParabolicIntersections.visualEdgeInclusion line 20
  3. abbrev OAI.HarmonicArtin.ParabolicIntersections.VisualAmalgam line 24
  4. def OAI.HarmonicArtin.ParabolicIntersections.visualToArtin line 26
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.visualSplit_cover line 30
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.visualSplit_finite_edge line 35
  7. def OAI.HarmonicArtin.ParabolicIntersections.visualGenerator line 51
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.visualGenerator_eq line 58
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.visualWord line 73
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_relators line 85
  11. def OAI.HarmonicArtin.ParabolicIntersections.visualFromArtin line 108
  12. lemma OAI.HarmonicArtin.ParabolicIntersections.visualFromArtin_generator line 111
  13. lemma OAI.HarmonicArtin.ParabolicIntersections.visualToArtin_generator line 115
  14. lemma OAI.HarmonicArtin.ParabolicIntersections.visualToArtin_from line 120
  15. lemma OAI.HarmonicArtin.ParabolicIntersections.visualFromArtin_factor line 130
  16. lemma OAI.HarmonicArtin.ParabolicIntersections.visualFromArtin_to line 151
  17. def OAI.HarmonicArtin.ParabolicIntersections.visualArtinEquiv line 163

    Source documentation

    The visual splitting is an isomorphism with the genuine injective amalgamated free product of the two standard subgroups.

    noncomputable def visualArtinEquiv (hsplit : IsVisualSplit M Y Z) :
    Artin M ≃* VisualAmalgam M Y Z where
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsVisualSplit, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.VisualAmalgam