theorem AptFoldingFromRetraction.exists_canonical_retraction {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC : A.IsMaximal C) : ∃ (ρ : V → V), (∀ s ∈ b.faces, Finset.image ρ s ∈ A.faces) ∧ (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → ρ v = v) ∧ (∀ (D : Finset V), b.IsMaximal D → A.IsMaximal (Finset.image ρ D)) ∧ (∀ (D₁ D₂ : Finset V), b.Adjacent D₁ D₂ → Finset.image ρ D₁ = Finset.image ρ D₂ ∨ A.Adjacent (Finset.image ρ D₁) (Finset.image ρ D₂)) ∧ ∀ B ∈ b.apartmentSystem.apartments, C ∈ B.faces → ∀ (v₁ v₂ : V), (∃ s ∈ B.faces, v₁ ∈ s) → (∃ s ∈ B.faces, v₂ ∈ s) → ρ v₁ = ρ v₂ → v₁ = v₂

For an apartment $A$ of a building $b$ and a chamber $C$ maximal in $A$, there exists a canonical retraction $\rho : V \to V$ from the building onto $A$ centered at $C$: it sends faces of $b$ to faces of $A$, fixes vertices of $A$, sends adjacent chambers to equal or adjacent chambers of $A$, and is injective on any apartment containing $C$.

theorem AptFoldingFromRetraction.apt_is_thin {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (F C : Finset V) : A.IsFacet F C → A.IsMaximal C → ∃! D : Finset V, D ≠ C ∧ A.IsFacet F D ∧ A.IsMaximal D

Thinness of apartments: for every facet $F$ of a maximal chamber $C$ in an apartment $A$, there is a unique other maximal chamber $D \ne C$ of $A$ with $F$ as a facet.

theorem AptFoldingFromRetraction.card_eq_of_adjacent {V : Type} [DecidableEq V] {K : SimplicialComplex V} {C D : Finset V} (hadj : K.Adjacent C D) : C.card = D.card

Adjacent chambers have the same cardinality.

theorem AptFoldingFromRetraction.list_chain_preserves {α : Type u_1} {R : α → α → Prop} {f : α → ℕ} (hR : ∀ (a b : α), R a b → f a = f b) (l : List α) (hl : l ≠ []) : List.IsChain R l → f (l.head hl) = f (l.getLast hl)

If a function $f$ is constant along every step of a chain under $R$, then $f$ agrees at the head and last of the chain.

theorem AptFoldingFromRetraction.card_eq_of_gallery {V : Type} [DecidableEq V] {K : SimplicialComplex V} {C D : Finset V} (g : Gallery K) (hconn : g.Connects C D) : C.card = D.card

Chambers connected by a gallery have the same cardinality.

theorem AptFoldingFromRetraction.apt_facet_of_maximal_containing {V : Type} [DecidableEq V] (b : Building V) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) {C D F₀ : Finset V} (hC_max : A.IsMaximal C) (hD_max : A.IsMaximal D) (hF₀_C : A.IsFacet F₀ C) (hF₀_sub_D : F₀ ⊆ D) : A.IsFacet F₀ D

If $F_0$ is a facet of a chamber $C$ in an apartment $A$ and $F_0 \subseteq D$ for another maximal chamber $D$ of $A$, then $F_0$ is also a facet of $D$.

theorem AptFoldingFromRetraction.retraction_fixes_face {V : Type} [DecidableEq V] {A : SimplicialComplex V} {ρ : V → V} (hρ_fix : ∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → ρ v = v) {s : Finset V} (hs : s ∈ A.faces) : Finset.image ρ s = s

A retraction fixing vertices of $A$ acts as the identity on faces of $A$.

theorem AptFoldingFromRetraction.third_chamber_from_thickness {V : Type} [DecidableEq V] {K : ChamberComplex V} (hthick : K.IsThick) {C C' : Finset V} (hadj : K.Adjacent C C') : ∃ (E : Finset V) (F : Finset V), E ≠ C ∧ E ≠ C' ∧ K.IsMaximal E ∧ K.IsFacet F C ∧ K.IsFacet F C' ∧ K.IsFacet F E

Thickness yields a third chamber: given adjacent chambers $C, C'$ sharing facet $F$, there exists $E \notin \{C, C'\}$ also sharing the facet $F$.

theorem AptFoldingFromRetraction.thin_unique_other_chamber {V : Type} [DecidableEq V] {b : Building V} {A : SimplicialComplex V} (hA : A ∈ b.apartmentSystem.apartments) {F C D₁ D₂ : Finset V} (hC_max : A.IsMaximal C) (hF_C : A.IsFacet F C) (hD₁_max : A.IsMaximal D₁) (hD₁_ne : D₁ ≠ C) (hF_D₁ : A.IsFacet F D₁) (hD₂_max : A.IsMaximal D₂) (hD₂_ne : D₂ ≠ C) (hF_D₂ : A.IsFacet F D₂) : D₁ = D₂

Uniqueness in thinness: two chambers both opposite to $C$ across the facet $F$ in an apartment must coincide.

theorem AptFoldingFromRetraction.apt_chamber_with_facet_is_C_or_C' {V : Type} [DecidableEq V] {b : Building V} {A : SimplicialComplex V} (hA : A ∈ b.apartmentSystem.apartments) {C C' D F₀ : Finset V} (hC_max : A.IsMaximal C) (hC'_max : A.IsMaximal C') (hD_max : A.IsMaximal D) (hne : C ≠ C') (hF₀_C : A.IsFacet F₀ C) (hF₀_C' : A.IsFacet F₀ C') (hF₀_sub_D : F₀ ⊆ D) : D = C ∨ D = C'

In a thin apartment, a maximal chamber containing a facet $F_0$ of two given chambers $C, C'$ must be one of $C$ or $C'$.