OAI/Topology/ArtinGroups/ParabolicIntersections/VisualTree.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The Bass--Serre tree and stabilizers of an actual visual Artin splitting.

  1. abbrev OAI.HarmonicArtin.ParabolicIntersections.VisualVertex line 12
  2. abbrev OAI.HarmonicArtin.ParabolicIntersections.visualGraph line 13
  3. abbrev OAI.HarmonicArtin.ParabolicIntersections.visualAction line 15
  4. def OAI.HarmonicArtin.ParabolicIntersections.visualVertex line 19
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_smul_vertex line 26
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_factor_comap line 32
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.conjugate_comap_hom line 47
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_vertex_stabilizer line 53
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.visualGraph_isTree line 62
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_vertex_exists line 67
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_vertex_isParabolic line 76
  12. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_vertex_adj line 82
  13. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_adj_representatives line 86
  14. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_adj_stabilizers_generate line 95

    Source documentation

    The stabilizers of the endpoints of every edge generate the whole group.

    lemma visual_adj_stabilizers_generate {u v : VisualVertex M Y Z}
    (h : (visualGraph M Y Z).Adj u v) :
    MulAction.stabilizer (Artin M) u ⊔ MulAction.stabilizer (Artin M) v=⊤ := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.VisualVertex, OAI.HarmonicArtin.ParabolicIntersections.visualGraph, OAI.HarmonicArtin.Artin