The two angle axioms hold for any chart-compatible direction assignment

Disproved

EuclideanBuildingDirections.angleAxioms_of_chart_dir

by Shuze Chen · Aug 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

buildingscoxeter-groupsmetric-geometry

Let $X$ be a Euclidean building given by a maximal atlas $\mathcal A$ modelled on the Euclidean Coxeter data $C$ , and let

\mathrm{dir}:X\times X\to\mathbb R^N

be any assignment of a unit vector of the model apartment to an ordered pair of distinct points which is compatible with the charts: for every $c\in\mathcal A$ and $p\neq q$ there is $w$ in the finite Weyl group $W$ with $\mathrm{dir}\bigl(c(p),c(q)\bigr)=w\cdot\frac{q-p}{\|q-p\|}$ . Then $\mathrm{dir}$ satisfies the two angle axioms of a $\Delta_{\mathrm{mod}}$ -direction structure:

EB1. For all $x\neq y$ and $x\neq z$ there is $w\in W$ with

\angle\bigl(\mathrm{dir}(x,y),\ w\cdot\mathrm{dir}(x,z)\bigr)\ \le\ \widetilde\angle_x(y,z),

the Euclidean comparison angle of the triangle $xyz$ .

EB2. For geodesic segments $\gamma_1$ from $x$ to $y$ and $\gamma_2$ from $x$ to $z$ there is $w\in W$ with

\angle_x(\gamma_1,\gamma_2)\ =\ \angle\bigl(\mathrm{dir}(x,y),\ w\cdot\mathrm{dir}(x,z)\bigr),

the Alexandrov angle being computed exactly by one of the finitely many $W$ -angles between the two orbits.

Role. This is the whole geometric content of Kleiner and Leeb's passage from the atlas description of a Euclidean building to the description by $\Delta_{\mathrm{mod}}$ -directions. Constructing the assignment itself is bookkeeping — read the direction of $xy$ in any apartment containing both points, and the compatibility of overlapping charts makes the answer independent of the choice up to $W$ — but the two angle axioms are not: EB1 compares an angle measured in the model apartment with a comparison angle in $X$ , and EB2 asserts the rigidity that the Alexandrov angle between two geodesics, which a priori is only bounded by the comparison angle, actually takes one of finitely many values. EB2 is the axiom that makes a Euclidean building more than a CAT(0) space with a lot of flats, and it is the source of every discreteness statement downstream, the rationality of the order of a harmonic map included.

Formalization note. Since $\Delta_{\mathrm{mod}}$ is the quotient of the unit sphere by $W$ , a direction is recorded by a unit vector representing it and the axioms appear in $W$ -invariant form. The assignment is a hypothesis rather than a construction, so that the elementary half of the passage can be discharged separately.

Preamble

import Definitions.Def_euclidean_building_directions

Formal statement

namespace EuclideanBuildingDirections

open HarmonicBuilding MetricGeometry

theorem angleAxioms_of_chart_dir {N : ℕ} (C : EuclideanCoxeterData N)
    {X : Type*} [MetricSpace X] [CompleteSpace X]
    (E : EuclideanBuildingData N C X)
    (dir : X → X → ModelEuclideanSpace N)
    (hunit : ∀ x y : X, x ≠ y → ‖dir x y‖ = 1)
    (hchart : ∀ c ∈ E.atlas, ∀ p q : ModelEuclideanSpace N, p ≠ q →
      ∃ w : C.weyl,
        dir (c p) (c q) = (w : OrthogonalGroup N) (segmentDirection p q)) :
    (∀ x y z : X, x ≠ y → x ≠ z →
      ∃ w : C.weyl,
        InnerProductGeometry.angle (dir x y) ((w : OrthogonalGroup N) (dir x z))
          ≤ comparisonAngle x y z) ∧
    (∀ x y z : X, ∀ g₁ g₂ : ℝ → X, x ≠ y → x ≠ z →
      IsGeodesicSegment g₁ x y → IsGeodesicSegment g₂ x z →
      ∃ w : C.weyl,
        alexandrovAngle x g₁ g₂
          = InnerProductGeometry.angle (dir x y)
              ((w : OrthogonalGroup N) (dir x z))) := by sorry

end EuclideanBuildingDirections

Source

B. Kleiner and B. Leeb, Rigidity of quasi-isometries for symmetric spaces and Euclidean buildings, Publ. Math. IHES 86 (1997), 115-197, Section 4, axioms EB1 and EB2 and their verification for a building given by an atlas; the equivalence of the two axiomatizations is due to A. Parreau, see Section 2 of L. Kramer, Metric properties of Euclidean buildings, arXiv:1012.2218.

View graph