OAI/Topology/ArtinGroups/ParabolicIntersections/TreeFixedPaths.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Fixed paths and branching for group actions on simplicial trees.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.stabilizer_smul line 13
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.pairStabilizer_smul line 20
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.fixes_path line 26

    Source documentation

    An element fixing the endpoints of a tree path fixes each vertex of it.

    theorem fixes_path (hT : T.IsAcyclic) (hA : PreservesAdj (G := G) T)
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PreservesAdj

  4. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.fixes_path_support line 41
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.pairStabilizer_le_at_path line 48

    Source documentation

    Endpoint stabilizers also fix all intermediate vertices.

    lemma pairStabilizer_le_at_path (hT : T.IsAcyclic) (hA : PreservesAdj (G := G) T)
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PreservesAdj