A Euclidean building given by its atlas carries a $\Delta_{\mathrm{mod}}$ -direction assignment

Disproved

EuclideanBuildingDirections.exists_directionAssignment

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

buildingscoxeter-groupsmetric-geometry

Let $X$ be a Euclidean building modelled on the Euclidean Coxeter data $C$ in the atlas sense: a complete CAT(0) space with a maximal atlas of apartments in which every segment, ray and line lies, and whose overlaps are governed by the affine Weyl group. Then $X$ carries a $\Delta_{\mathrm{mod}}$ -direction assignment: there is a map

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

sending an ordered pair of distinct points to a unit vector of the model apartment, such that

(EB1, directions) for any three points with $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 comparison angle;
(EB2, angle rigidity) 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;
(compatibility) every chart $c$ of the atlas preserves directions up to $W$ : $\mathrm{dir}\bigl(c(p),c(q)\bigr)=w\cdot\frac{q-p}{\|q-p\|}$ for some $w\in W$ .

Role. The two axiomatizations of a Euclidean building used in this development — the atlas description recorded by EuclideanBuildingData, and the description by $\Delta_{\mathrm{mod}}$ -directions recorded by BuildingWithDirections — describe the same objects. The passage from directions to a maximal atlas is elementary and already available as EuclideanBuildingDirections.exists_euclideanBuildingData; this statement is the other direction, and it is the substantive one, since the direction assignment has to be constructed. It is what lets a result proved for one description be quoted for the other, and in particular it removes the duplication between the tangent-map reduction stated over an atlas and the same reduction stated over a direction structure.

Since $\Delta_{\mathrm{mod}}$ is the quotient of the unit sphere of the model apartment by the finite Weyl group, a direction is recorded here by a unit vector representing it, and the axioms are stated in the equivalent $W$ -invariant form: "the distance in $\Delta_{\mathrm{mod}}$ is at most $c$ " becomes " $\angle(u,wv)\le c$ for some $w\in W$ ", and "lies in the finite set of distances between the two orbits" becomes "equals $\angle(u,wv)$ for some $w\in W$ ".

Formalization note. The direction assignment is produced as a bare function together with its four properties rather than as a bundled structure, so that the structure BuildingWithDirections can be assembled from it together with the atlas data already present; closure of a maximal atlas under precomposition with the affine Weyl group is elementary and is not part of this statement.

Preamble

import Definitions.Def_euclidean_building_directions

Formal statement

namespace EuclideanBuildingDirections

open HarmonicBuilding MetricGeometry

theorem exists_directionAssignment {N : ℕ} (C : EuclideanCoxeterData N)
    {X : Type*} [MetricSpace X] [CompleteSpace X]
    (E : EuclideanBuildingData N C X) :
    ∃ dir : X → X → ModelEuclideanSpace N,
      (∀ x y : X, x ≠ y → ‖dir x y‖ = 1) ∧
      (∀ 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))) ∧
      (∀ c ∈ E.atlas, ∀ p q : ModelEuclideanSpace N, p ≠ q →
        ∃ w : C.weyl,
          dir (c p) (c q) = (w : OrthogonalGroup N) (segmentDirection p q)) := 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 (the axioms EB1 and EB2 for Delta_mod-directions and their equivalence with the atlas description); the equivalence of the Kleiner-Leeb axioms with the classical ones is due to A. Parreau, see Theorem 2.1 and Section 2 of L. Kramer, Metric properties of Euclidean buildings, arXiv:1012.2218.

View graph

A Euclidean building given by its atlas carries a Δmod\Delta_{\mathrm{mod}}Δmod​-direction assignment

A Euclidean building given by its atlas carries a $\Delta_{\mathrm{mod}}$ -direction assignment