(In)dependence of the axioms of \(\Lambda\)-trees. (English) Zbl 07845443
Summary: A \(\Lambda\)-tree is a \(\Lambda\)-metric space satisfying three axioms (1), (2), and (3). We give a characterization of those ordered abelian groups \(\Lambda\) for which axioms (1) and (2) imply axiom (3). As a special case, it follows that for the important class of ordered abelian groups \(\Lambda\) that satisfy \(\Lambda =2\Lambda\), (3) follows from (1) and (2). For some ordered abelian groups \(\Lambda\), we show that axiom (2) is independent of axioms (1) and (3) and ask whether this holds for all ordered abelian groups. Part of this work has been formalized in the proof assistant Lean.
MSC:
| 06F15 | Ordered groups |
| 06F20 | Ordered abelian groups, Riesz groups, ordered linear spaces |
| 05C05 | Trees |
| 51M30 | Line geometries and their generalizations |
| 20F60 | Ordered groups (group-theoretic aspects) |
References:
| [1] | R. Alperin and H. Bass, Length functions of group actions on Λ-trees, in: Combinatorial Group Theory and Topology, S. M. Gersten and J. R. Stallings, (Ed.), Annals of Mathematical Studies, vol. 111, Princeton University Press, Princeton, NJ,1987, p. 265-378. · Zbl 0978.20500 |
| [2] | R. Appenzeller, Λ-metric-space - Lean project, 2023, https://github.com/Strichcoder/lambda-metric-space. |
| [3] | C. Bennett. Affine Λ-buildings, Ph.D.-thesis. University of Chicago, 1990. |
| [4] | C. Bennett, Affine Lambda-buildings I, Proc. London Math. Soc. 68 (1994), no. 3, 541-576. · Zbl 0834.20026 |
| [5] | K. Buzzard, J. Commelin, and P. Massot, Formalising perfectiod spaces, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020. |
| [6] | C. Bennett, P. Schwer, and K. Struyve, On axiomatic definitions of non-discrete affine buildings, Adv. Geom. 14 (2014), no. 3, 381-412. · Zbl 1408.51009 |
| [7] | G. W. Brumfiel, The tree of a non-Archimedean hyperbolic plane, Contemporary Mathematics, vol. 74, 1988. · Zbl 0657.51013 |
| [8] | I. M. Chiswell, Introduction to Λ-trees, World Scientific Publishing Co. Inc., River Edge, NJ, 2001, ISBN 981-02-4386-3. · Zbl 1004.20014 |
| [9] | L. M. de Moura, S. Kong, J. Avigad, F. van Doorn, J. von Raumer, The Lean Theorem Prover (System Description), Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, 2015, p. 378-388. · Zbl 1465.68279 |
| [10] | The mathlib Community. The Lean mathematical library, 2019. arXiv:1910.09336. |
| [11] | J. W. Morgan and P. B. Shalen. Valuations, trees, and degenerations of hyperbolic structures. I, Ann. Math. (2) 120 (1984), no. 3, 401-476. · Zbl 0583.57005 |
| [12] | A. Parreau, Immeubles affines: construction par les normes, in: Crystallographic Groups and Their Generalizations: Workshop, Katholicke Universiteit Leuven Campus Kortrijk, Belgium, May 26-28, 1999, vol. 262, American Mathematical Soc., 2000, p. 263. · Zbl 1060.20027 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
