How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Finite groups acting on trees have a global fixed vertex after subdivision
Statement
Let a finite group act on a simplicial tree . Then the induced action on the barycentric subdivision fixes a vertex.
Facts & Assumptions
Given: A finite group acting on a simplicial tree .
Barycentric subdivision preserves the tree and removes edge inversions. (Barycentric subdivision removes edge inversions while preserving the tree)
The path metric on a simplicial tree is geodesic and integer-valued. (The path metric on a simplicial tree is geodesic and integer-valued)
Proof
Replace by its barycentric subdivision using [L1]. Choose a vertex of . Because is finite, the orbit is finite, and the union of the geodesics joining pairs of orbit vertices is therefore a finite -invariant subtree .
Let be the diameter of , choose vertices with , and let be the midpoint of the unique geodesic from to . In a finite tree every diameter geodesic has the same midpoint: if two diameters had different midpoints, the unique path joining those midpoints would extend one of them past length , contradicting maximality. So depends only on , not on the chosen diameter.
Any automorphism of sends diameter geodesics to diameter geodesics, so it fixes the intrinsic midpoint from step 2.1. If is even, is a vertex of and is fixed. If is odd, is the midpoint of a unique geometric edge of , so every element of preserves that edge setwise. The action on is without inversions by [L1], hence no element can swap the two endpoints; both endpoints are fixed. In either case the induced action on fixes a vertex.
Depends on
Used by
Dependency tree · two levels
6 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Jean-Pierre Serre, Trees (standard reference, not scraped)