structure AptIsCoxeterProof.PreApartmentData {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) : Type u_1

A bundle of structural properties an apartment system must satisfy in order to apply the Tits theorem and conclude that apartments are Coxeter complexes. Captures simplicial isomorphism existence, gallery convexity, thinness, and bijectivity of intertwining maps.

• apartments : Set (SimplicialComplex V)
• nonempty_apartments : ∃ (A : SimplicialComplex V), A ∈ self.apartments
• sub (A : SimplicialComplex V) : A ∈ self.apartments → IsSubcomplex A K.toSimplicialComplex
• contains_pair (C D : Finset V) : K.IsMaximal C → K.IsMaximal D → ∃ A ∈ self.apartments, C ∈ A.faces ∧ D ∈ A.faces
• 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_thin_cc (A : SimplicialComplex V) : A ∈ self.apartments → ∃ (cc : ChamberComplex V), cc.toSimplicialComplex = A ∧ cc.IsThin
• apt_automorphism (A : SimplicialComplex V) : A ∈ self.apartments → ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → ∃ (φ : V → V), Function.Bijective φ ∧ (∀ (s : Finset V), s ∈ A.faces ↔ Finset.image φ s ∈ A.faces) ∧ Finset.image φ D = C

theorem AptIsCoxeterProof.PreApartmentData.apt_unique_labelling {V : Type u_2} [DecidableEq V] {K : ChamberComplex V} (pre : PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) (L₁ L₂ : Type) [DecidableEq L₁] [DecidableEq L₂] (lab₁ : Finset V → Finset L₁) (lab₂ : Finset V → Finset L₂) (hlab₁ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₁ s ⊂ lab₁ t) (hlab₂ : ∀ (s t : Finset V), s ∈ A.faces → t ∈ A.faces → s ⊂ t → lab₂ s ⊂ lab₂ t) (C₀ : Finset V) (hC₀ : A.IsMaximal C₀) : (∃ (f : L₁ → L₂), Function.Bijective f ∧ lab₂ C₀ = Finset.image f (lab₁ C₀)) ∧ ∀ (f : L₁ → L₂), Function.Bijective f → lab₂ C₀ = Finset.image f (lab₁ C₀) → ∀ s ∈ A.faces, lab₂ s = Finset.image f (lab₁ s)

Uniqueness of labellings on an apartment: any two strict-mono labellings agree up to a unique bijection of label sets determined by the value on a fixed chamber $C_0$.

theorem AptIsCoxeterProof.coxeter_cayley_no_triangle {B : Type u_2} (M : CoxeterMatrix B) (w₁ w₂ w₃ : M.Group) (h₁₂ : CoxeterComplex.ChamberAdjacent M w₁ w₂) (h₂₃ : CoxeterComplex.ChamberAdjacent M w₂ w₃) (h₁₃ : CoxeterComplex.ChamberAdjacent M w₁ w₃) : False

In the Cayley graph of a Coxeter group, three elements pairwise adjacent in the chamber sense cannot exist (the graph contains no triangles).

def AptIsCoxeterProof.HasSufficientFoldings {V : Type u_1} [DecidableEq V] (cc : ChamberComplex V) : Prop

A chamber complex $cc$ has sufficient foldings if every pair of adjacent chambers $C, C'$ admits a pair of foldings whose images contain the corresponding chamber.

def AptIsCoxeterProof.TitsTheoremHyp (V : Type u_2) [DecidableEq V] : Prop

Hypothesis statement of Tits' theorem: every thin chamber complex with sufficient foldings is isomorphic to a Coxeter complex.

def AptIsCoxeterProof.ThicknessImpliesAptStructureHyp (V : Type u_2) [DecidableEq V] : Prop

Hypothesis statement: in a thick chamber complex, every apartment carries a thin chamber structure with sufficient foldings.

theorem AptIsCoxeterProof.apt_is_coxeter_from_foldings {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (hThick : K.IsThick) (pre : PreApartmentData K) (tits_thm : TitsTheoremHyp V) (thickness_implies_apt : ThicknessImpliesAptStructureHyp V) (A : SimplicialComplex V) (hA : A ∈ pre.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

Main conditional theorem: assuming the Tits theorem and the thickness-implies-apartment-structure hypothesis, every apartment $A$ of a thick building $K$ is a Coxeter complex with an injective, surjective, adjacency-preserving labelling by a Coxeter group $M.\mathrm{Group}$.

def AptIsCoxeterProof.PreApartmentData.toApartmentSystem {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (pre : PreApartmentData K) (hThick : K.IsThick) (tits_thm : TitsTheoremHyp V) (thickness_implies_apt : ThicknessImpliesAptStructureHyp V) : ApartmentSystem K

Promote a PreApartmentData to a full ApartmentSystem, using the conditional foldings construction to supply the apartments-are-Coxeter component.

theorem AptIsCoxeterProof.PreApartmentData.toApartmentSystem_apartments {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (pre : PreApartmentData K) (hThick : K.IsThick) (tits_thm : TitsTheoremHyp V) (thickness_implies_apt : ThicknessImpliesAptStructureHyp V) : (pre.toApartmentSystem hThick tits_thm thickness_implies_apt).apartments = pre.apartments

The promoted apartment system has the same underlying set of apartments.