theorem AptIsCoxeterProof.thickness_hyp {V : Type} [DecidableEq V] : ThicknessImpliesAptStructureHyp V

Assembled discharge of the hypothesis ThicknessImpliesAptStructureHyp, asserting that thickness of a chamber complex induces sufficient apartment structure (via foldings).

theorem AptIsCoxeterProof.apt_is_coxeter_from_foldings' {V : Type} [DecidableEq V] (K : ChamberComplex V) (hThick : K.IsThick) (pre : PreApartmentData K) (tits_thm : TitsTheoremHyp 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

Each apartment of a thick chamber complex, equipped with sufficient foldings, carries a Coxeter complex structure with an injective surjective labeling map $\varphi$ to a Coxeter group preserving adjacency.

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

Promote PreApartmentData to a full ApartmentSystem, given thickness and the Tits theorem hypothesis.

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

The apartments of pre.toApartmentSystem' are exactly pre.apartments.