OAI/Topology/ArtinGroups/ParabolicIntersections/TreeSegmentOccurrences.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite translates of a segment inside a finite path

This is the finite-pattern input for constructing an acylindrical graph from a tree action. The segment is in the actual tree and its pointwise stabilizer is trivial; its occurrences are group elements, not formal labels.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.pair_orbit_injective line 15
  2. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.segmentOccurrences line 30

    Source documentation

    Group translates whose two endpoints occur in a specified finite path.

    def segmentOccurrences (u v : V) (T : SimpleGraph V) {x y : V} (p : T.Walk x y) : Set G :=
…
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.segmentOccurrences_finite line 33
  4. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.ContainsSegment line 43

    Source documentation

    A path contains a translate of the fixed segment. In a tree the endpoint condition also puts the entire translated segment in the path.

    def ContainsSegment (u v : V) (T : SimpleGraph V) {x y : V} (p : T.Walk x y) : Prop :=
…
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.segmentOccurrences_reverse line 47
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.segmentOccurrences_subpath line 52
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.smul_mem_mapped_support line 58
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.segmentOccurrences_map line 75