A simplicial map from $K$ to $L$: a vertex function sending faces of $K$ to faces of $L$.
- toFun : V → V
Instances For
A is a subcomplex of K iff every face of A is a face of K.
Instances For
An apartment system on a chamber complex $K$: a collection of "apartments" subject to the axioms (B1)–(B3) of buildings: every two chambers lie in a common apartment, common-chamber apartments admit a fixing simplicial isomorphism, gallery-convexity inside apartments, plus the Coxeter-complex structure on each apartment.
- apartments : Set (SimplicialComplex V)
- nonempty_apartments : ∃ (A : SimplicialComplex V), A ∈ self.apartments
- sub (A : SimplicialComplex V) : A ∈ self.apartments → IsSubcomplex A K.toSimplicialComplex
- iso_exists (A : SimplicialComplex V) : A ∈ self.apartments → ∀ A' ∈ self.apartments, ∀ x ∈ A.faces, x ∈ A'.faces → ∀ (C : Finset V), A.IsMaximal C → C ∈ A'.faces → ∃ (φ : SimplicialMap A A'), (∀ v ∈ x, φ.toFun v = v) ∧ ∀ v ∈ C, φ.toFun v = v
- maximal_in_apt_is_maximal (A : SimplicialComplex V) : A ∈ self.apartments → ∀ (C : Finset V), A.IsMaximal C → K.IsMaximal C
- gallery_convex (A : SimplicialComplex V) : A ∈ self.apartments → ∀ (C D : Finset V), C ∈ A.faces → K.IsMaximal C → D ∈ A.faces → K.IsMaximal D → ∀ (g : Gallery K.toSimplicialComplex), g.Connects C D → g.length = galleryDist K.toSimplicialComplex C D → ∀ E ∈ g.chambers, E ∈ A.faces
- building_maximal_in_apt_is_apt_maximal (A : SimplicialComplex V) : A ∈ self.apartments → ∀ C ∈ A.faces, K.IsMaximal C → A.IsMaximal C
- apt_nonempty (A : SimplicialComplex V) : A ∈ self.apartments → ∃ (s : Finset V), s ∈ A.faces
- iso_bijective (A : SimplicialComplex V) : A ∈ self.apartments → ∀ A' ∈ self.apartments, ∀ C ∈ A.faces, C ∈ A'.faces → A.IsMaximal C → ∃ (φ : V → V), Function.Bijective φ ∧ ∀ (s : Finset V), s ∈ A.faces ↔ Finset.image φ s ∈ A'.faces
- apt_is_coxeter (A : SimplicialComplex V) : A ∈ self.apartments → ∃ (B_idx : Type) (M : CoxeterMatrix B_idx) (cc : ChamberComplex V), cc.toSimplicialComplex = A ∧ ∃ (φ : Finset V → M.Group), (∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) ∧ (∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) ∧ (∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) ∧ cc.IsThin
Instances For
Uniqueness of label transport on an apartment: two strictly monotone labellings agree under a unique bijection of label sets determined by their values on any maximal chamber $C_0$.
Canonical retraction onto an apartment $B$ at a maximal chamber $C_0$: a chamber-level map $\rho$ sending every chamber of $K$ into $B$ and acting as the identity on chambers of $B$.
A retraction $\rho$ onto an apartment preserves gallery distance from the center chamber $C$: $d(C, \rho D) = d(C, D)$.
If $\psi_0$ is a gallery-distance preserving map from $Y_0$ into the building, then composing with the retraction $\rho$ recovers the original chamber: $\rho(\psi_0 E) = E$ for $E \in Y_0$.
Combining the previous two: a gallery-distance preserving map $\psi_0$ preserves the distance from the center $C$, i.e. $d(C, \psi_0 E) = d(C, E)$ for $E \in Y_0$.
One-step extension of a gallery isometry: given a chamber $C'$ adjacent to the domain $Y_0$, one can extend $\psi_0$ to $C'$ while preserving all gallery distances.
In a finite chain whose head satisfies $P$ and last does not, there is an adjacent pair where $P$ flips.
Gallery boundary: a proper non-empty subset $Y_0$ of the maximal chambers of $A$ has a boundary chamber $C' \notin Y_0$ adjacent to some chamber of $Y_0$.
The image of a gallery-distance preserving map into the apartment $A$ is maximal in $A$.
The image $\varphi C$ is a maximal chamber of the ambient building $K$.
Gallery distance from a non-maximal chamber to any other chamber is $0$.
Two distinct maximal chambers have strictly positive gallery distance.
When $\varphi$ is constant on its domain $S_1$, every element of $S_1$ is itself maximal in $K$.
A chamber $C$ in the source of a gallery-distance preserving map is maximal in $K$.
A gallery-distance preserving map $\varphi : S_1 \to A.\mathrm{faces}$ maps to apartment-maximal chambers and its source consists of building-maximal chambers.
A gallery-distance preserving map $\varphi$ is injective: $\varphi C = \varphi D$ implies $C = D$.
Seed graph $G_0$ for the gallery-isometry extension: a functional relation on chamber pairs $(C, D)$ encoding an initial fragment of a gallery isometry into the apartment $A$.
Using Zorn's lemma, a gallery-distance preserving map from a subset $S_1$ into $A$ extends to a gallery-distance preserving map $\psi$ defined on all maximal chambers of $A$ with image in $K$.
Uniqueness lemma: two gallery-distance preserving maps from $A$ into $K$ that agree on a single chamber $C_0$ agree on every maximal chamber of $A$.
The composition $\rho \circ \psi$ of a retraction $\rho$ onto $B$ with a gallery-isometry $\psi$ is again a gallery isometry into $K$.
If $\psi C_0 \in B$ and $\rho$ retracts onto $B$, then $\rho \circ \psi = \psi$ on every maximal chamber $D$ of $A$.
If a gallery isometry $\psi$ sends one chamber $C_0$ into apartment $B$, then it sends every maximal chamber of $A$ into $B$.
The image of a gallery isometry $\psi$ defined on all of an apartment $A$ is contained in some apartment $B$ of the system.
A subset $S_1$ that lies in the image of a full-apartment gallery isometry is contained in some apartment $B$.
Strong isometry extension via galleries: a gallery-distance preserving map from $S_1$ into $S_2$, where $S_2$ lies in some apartment, has its source $S_1$ also contained in an apartment.
A building on vertex set $V$: a thick chamber complex equipped with an apartment system.
- apartmentSystem : ApartmentSystem self.toChamberComplex
- thick : self.IsThick