section ‹Buildings› text ‹ In this section we collect the axioms for a (thick) building in a locale, and prove that apartments in a building are uniformly Coxeter. › theory Building imports Coxeter begin subsection ‹Apartment systems› text ‹ First we describe and explore the basic structure of apartment systems. An apartment system is a collection of isomorphic thin chamber subcomplexes with certain intersection properties. › subsubsection ‹Locale and basic facts› locale ChamberComplexWithApartmentSystem = ChamberComplex X for X :: "'a set set" + fixes 𝒜 :: "'a set set set" assumes subcomplexes : "A∈𝒜 ⟹ ChamberSubcomplex A" and thincomplexes : "A∈𝒜 ⟹ ThinChamberComplex A" and no_trivial_apartments: "{}∉𝒜" and containtwo : "chamber C ⟹ chamber D ⟹ ∃A∈𝒜. C∈A ∧ D∈A" and intersecttwo : "⟦ A∈𝒜; A'∈𝒜; x∈A∩A'; C∈A∩A'; chamber C ⟧ ⟹ ∃f. ChamberComplexIsomorphism A A' f ∧ fixespointwise f x ∧ fixespointwise f C" begin lemmas complexes = ChamberSubcomplexD_complex [OF subcomplexes] lemmas apartment_simplices = ChamberSubcomplexD_sub [OF subcomplexes] lemmas chamber_in_apartment = chamber_in_subcomplex [OF subcomplexes] lemmas apartment_chamber = subcomplex_chamber [OF subcomplexes] lemmas gallery_in_apartment = gallery_in_subcomplex [OF subcomplexes] lemmas apartment_gallery = subcomplex_gallery [OF subcomplexes] lemmas min_gallery_in_apartment = min_gallery_in_subcomplex [OF subcomplexes] lemmas apartment_simplex_in_max = ChamberComplex.simplex_in_max [OF complexes] lemmas apartment_faces = ChamberComplex.faces [OF complexes] lemmas apartment_chamber_system_def = ChamberComplex.chamber_system_def [OF complexes] lemmas apartment_chamberD_simplex = ChamberComplex.chamberD_simplex [OF complexes] lemmas apartment_chamber_distance_def = ChamberComplex.chamber_distance_def [OF complexes] lemmas apartment_galleryD_chamber = ChamberComplex.galleryD_chamber [OF complexes] lemmas apartment_gallery_least_length = ChamberComplex.gallery_least_length [OF complexes] lemmas apartment_min_galleryD_gallery = ChamberComplex.min_galleryD_gallery [OF complexes] lemmas apartment_min_gallery_pgallery = ChamberComplex.min_gallery_pgallery [OF complexes] lemmas apartment_trivial_morphism = ChamberComplex.trivial_morphism [OF complexes] lemmas apartment_chamber_system_simplices = ChamberComplex.chamber_system_simplices [OF complexes] lemmas apartment_min_gallery_least_length = ChamberComplex.min_gallery_least_length [OF complexes] lemmas apartment_vertex_set_int = ChamberComplex.vertex_set_int[OF complexes complexes] lemmas apartment_standard_uniqueness_pgallery_betw = ThinChamberComplex.standard_uniqueness_pgallery_betw[OF thincomplexes] lemmas apartment_standard_uniqueness = ThinChamberComplex.standard_uniqueness[OF thincomplexes] lemmas apartment_standard_uniqueness_isomorphs = ThinChamberComplex.standard_uniqueness_isomorphs[OF thincomplexes] abbreviation "supapartment C D ≡ (SOME A. A∈𝒜 ∧ C∈A ∧ D∈A)" lemma supapartmentD: assumes CD: "chamber C" "chamber D" defines A : "A ≡ supapartment C D" shows "A∈𝒜" "C∈A" "D∈A" proof- from CD have 1: "∃A. A∈𝒜 ∧ C∈A ∧ D∈A" using containtwo by fast from A show "A∈𝒜" "C∈A" "D∈A" using someI_ex[OF 1] by auto qed lemma iso_fixespointwise_chamber_in_int_apartments: assumes apartments: "A ∈ 𝒜" "A' ∈ 𝒜" and chamber : "chamber C" "C∈A∩A'" and iso : "ChamberComplexIsomorphism A A' f" "fixespointwise f C" shows "fixespointwise f (⋃(A∩A'))" proof (rule fixespointwiseI) fix v assume "v ∈ ⋃(A ∩ A')" from this obtain x where x: "x ∈ A∩A'" "v ∈ x" by fast from apartments x(1) chamber intersecttwo[of A A'] obtain g where g: "ChamberComplexIsomorphism A A' g" "fixespointwise g x" "fixespointwise g C" by force from assms g(1,3) have "fun_eq_on f g (⋃A)" using chamber_in_apartment by (auto intro: apartment_standard_uniqueness_isomorphs fixespointwise2_imp_eq_on ) with x g(2) show "f v = id v" using fixespointwiseD fun_eq_onD by force qed lemma strong_intersecttwo: "⟦ A∈𝒜; A'∈𝒜; chamber C; C ∈ A∩A' ⟧ ⟹ ∃f. ChamberComplexIsomorphism A A' f ∧ fixespointwise f (⋃(A∩A'))" using intersecttwo[of A A'] iso_fixespointwise_chamber_in_int_apartments[of A A' C] by force end (* context ChamberComplexWithApartmentSystem *) subsubsection ‹Isomorphisms between apartments› text ‹ By standard uniqueness, the isomorphism between overlapping apartments guaranteed by the axiom ‹intersecttwo› is unique. › context ChamberComplexWithApartmentSystem begin lemma ex1_apartment_iso: assumes "A∈𝒜" "A'∈𝒜" "chamber C" "C∈A∩A'" shows "∃!f. ChamberComplexIsomorphism A A' f ∧ fixespointwise f (⋃(A∩A')) ∧ fixespointwise f (-⋃A)" ― ‹The third clause in the conjunction is to facilitate uniqueness.› proof (rule ex_ex1I) from assms obtain f where f: "ChamberComplexIsomorphism A A' f" "fixespointwise f (⋃(A∩A'))" using strong_intersecttwo by fast define f' where "f' = restrict1 f (⋃A)" from f(1) f'_def have "ChamberComplexIsomorphism A A' f'" by (fastforce intro: ChamberComplexIsomorphism.iso_cong fun_eq_onI) moreover from f(2) f'_def have "fixespointwise f' (⋃(A∩A'))" using fun_eq_onI[of "⋃(A∩A')" f' f] by (fastforce intro: fixespointwise_cong) moreover from f'_def have "fixespointwise f' (-⋃A)" by (auto intro: fixespointwiseI) ultimately show "∃f. ChamberComplexIsomorphism A A' f ∧ fixespointwise f (⋃(A∩A')) ∧ fixespointwise f (-⋃A)" by fast next fix f g assume "ChamberComplexIsomorphism A A' f ∧ fixespointwise f (⋃(A ∩ A')) ∧ fixespointwise f (-⋃A)" "ChamberComplexIsomorphism A A' g ∧ fixespointwise g (⋃(A ∩ A')) ∧ fixespointwise g (-⋃A)" with assms show "f=g" using chamber_in_apartment fixespointwise2_imp_eq_on[of f C g] fun_eq_on_cong fixespointwise_subset[of f "⋃(A∩A')" C] fixespointwise_subset[of g "⋃(A∩A')" C] apartment_standard_uniqueness_isomorphs by (blast intro: fun_eq_on_set_and_comp_imp_eq) qed definition the_apartment_iso :: "'a set set ⇒ 'a set set ⇒ ('a⇒'a)" where "the_apartment_iso A A' ≡ (THE f. ChamberComplexIsomorphism A A' f ∧ fixespointwise f (⋃(A∩A')) ∧ fixespointwise f (-⋃A))" lemma the_apartment_isoD: assumes "A∈𝒜" "A'∈𝒜" "chamber C" "C∈A∩A'" defines "f ≡ the_apartment_iso A A'" shows "ChamberComplexIsomorphism A A' f" "fixespointwise f (⋃(A∩A'))" "fixespointwise f (-⋃A)" using assms theI'[OF ex1_apartment_iso] unfolding the_apartment_iso_def by auto lemmas the_apartment_iso_apartment_chamber_map = ChamberComplexIsomorphism.chamber_map [OF the_apartment_isoD(1)] lemmas the_apartment_iso_apartment_simplex_map = ChamberComplexIsomorphism.simplex_map [OF the_apartment_isoD(1)] lemma the_apartment_iso_chamber_map: "⟦ A∈𝒜; B∈𝒜; chamber C; C∈A∩B; chamber D; D∈A ⟧ ⟹ chamber (the_apartment_iso A B ` D)" using chamber_in_apartment[of A] apartment_chamber the_apartment_iso_apartment_chamber_map by auto lemma the_apartment_iso_comp: assumes apartments: "A∈𝒜" "A'∈𝒜" "A''∈𝒜" and chamber : "chamber C" "C∈A∩A'∩A''" defines "f ≡ the_apartment_iso A A'" and "g ≡ the_apartment_iso A' A''" and "h ≡ the_apartment_iso A A''" defines "gf ≡ restrict1 (g∘f) (⋃A)" shows "h = gf" proof ( rule fun_eq_on_set_and_comp_imp_eq, rule apartment_standard_uniqueness_isomorphs, rule apartments(3) ) from gf_def have gf_cong1: "fun_eq_on gf (g∘f) (⋃A)" by (fastforce intro: fun_eq_onI) from gf_def have gf_cong2: "fixespointwise gf (-⋃A)" by (auto intro: fixespointwiseI) from apartments(1,3) chamber h_def show "ChamberComplexIsomorphism A A'' h" using the_apartment_isoD(1) by fast from apartments chamber f_def g_def show "ChamberComplexIsomorphism A A'' gf" using ChamberComplexIsomorphism.iso_cong[OF _ gf_cong1] ChamberComplexIsomorphism.iso_comp the_apartment_isoD(1) by blast from apartments(1) chamber show "ChamberComplex.chamber A C" using chamber_in_apartment by fast show "fun_eq_on h gf C" proof (rule fixespointwise2_imp_eq_on) from assms(1,3) chamber h_def show "fixespointwise h C" using fixespointwise_subset the_apartment_isoD(2) by blast have "fun_eq_on gf (g∘f) (⋃(A∩A'∩A''))" using fun_eq_on_subset[OF gf_cong1, of "⋃(A∩A'∩A'')"] by fast moreover from f_def g_def apartments chamber have "fixespointwise (g∘f) (⋃(A∩A'∩A''))" using fixespointwise_comp[of f "⋃(A∩A'∩A'')" g] fixespointwise_subset[ OF the_apartment_isoD(2), of _ _ C "⋃(A∩A'∩A'')" ] by auto ultimately have "fixespointwise gf (⋃(A∩A'∩A''))" using fixespointwise_cong[of gf "g∘f"] by fast with chamber(2) show "fixespointwise gf C" using fixespointwise_subset by auto qed from h_def apartments(1,3) chamber show "fun_eq_on h gf (- ⋃A)" using the_apartment_isoD(3) gf_cong2 by (auto intro: fun_eq_on_cong) qed lemma the_apartment_iso_int_im: assumes "A∈𝒜" "A'∈𝒜" "chamber C" "C∈A∩A'" "x∈A∩A'" defines "f ≡ the_apartment_iso A A'" shows "f`x = x" using assms the_apartment_isoD(2) fixespointwise_im[of f "⋃(A∩A')" x] by fast end (* context ChamberComplexWithApartmentSystem *) subsubsection ‹Retractions onto apartments› text ‹ Since the isomorphism between overlapping apartments is the identity on their intersection, starting with a fixed chamber in a fixed apartment, we can construct a retraction onto that apartment as follows. Given a vertex in the complex, that vertex is contained a chamber, and that chamber lies in a common apartment with the fixed chamber. We then apply to the vertex the apartment isomorphism from that common apartment to the fixed apartment. It turns out that the image of the vertex does not depend on the containing chamber and apartment chosen, and so since the isomorphisms between apartments used are unique, such a retraction onto an apartment is canonical. › context ChamberComplexWithApartmentSystem begin definition canonical_retraction :: "'a set set ⇒ 'a set ⇒ ('a⇒'a)" where "canonical_retraction A C = restrict1 (λv. the_apartment_iso (supapartment (supchamber v) C) A v) (⋃X)" lemma canonical_retraction_retraction: assumes "A∈𝒜" "chamber C" "C∈A" "v∈⋃A" shows "canonical_retraction A C v = v" proof- define D where "D = supchamber v" define B where "B = supapartment D C" from D_def assms(1,4) have D_facts: "chamber D" "v∈D" using apartment_simplices supchamberD[of v] by auto from B_def assms(2) have B_facts: "B∈𝒜" "D∈B" "C∈B" using D_facts(1) supapartmentD[of D C] by auto from assms(1,4) have "v∈⋃(B∩A)" using D_facts(2) B_facts(1,2) apartment_vertex_set_int by fast with assms(1-3) D_def B_def show ?thesis using canonical_retraction_def B_facts(1,3) fixespointwiseD[of _ "⋃(B∩A)" v] the_apartment_isoD(2)[of B A C] by simp qed lemma canonical_retraction_simplex_retraction1: "⟦ A∈𝒜; chamber C; C∈A; a∈A ⟧ ⟹ fixespointwise (canonical_retraction A C) a" using canonical_retraction_retraction by (force intro: fixespointwiseI) lemma canonical_retraction_simplex_retraction2: "⟦ A∈𝒜; chamber C; C∈A; a∈A ⟧ ⟹ canonical_retraction A C ` a = a" using canonical_retraction_simplex_retraction1 fixespointwise_im[of _ a a] by simp lemma canonical_retraction_uniform: assumes apartments: "A∈𝒜" "B∈𝒜" and chambers : "chamber C" "C∈A∩B" shows "fun_eq_on (canonical_retraction A C) (the_apartment_iso B A) (⋃B)" proof (rule fun_eq_onI) fix v assume v: "v∈⋃B" define D' B' g f h where "D' = supchamber v" and "B' = supapartment D' C" and "g = the_apartment_iso B' A" and "f = the_apartment_iso B B'" and "h = the_apartment_iso B A" from D'_def v apartments(2) have D'_facts: "chamber D'" "v∈D'" using apartment_simplices supchamberD[of v] by auto from B'_def chambers(1) have B'_facts: "B'∈𝒜" "D'∈B'" "C∈B'" using D'_facts(1) supapartmentD[of D' C] by auto from f_def apartments(2) chambers have "fixespointwise f (⋃(B ∩ B'))" using B'_facts(1,3) the_apartment_isoD(2)[of B B' C] by fast moreover from v apartments(2) have "v∈⋃(B∩B')" using D'_facts(2) B'_facts(1,2) apartment_vertex_set_int by fast ultimately show "canonical_retraction A C v = h v" using D'_def B'_def g_def f_def h_def v apartments chambers fixespointwiseD[of f "⋃(B∩B')" v] canonical_retraction_def apartment_simplices[of B] B'_facts(1,3) the_apartment_iso_comp[of B B' A C] by auto qed lemma canonical_retraction_uniform_im: "⟦ A∈𝒜; B∈𝒜; chamber C; C∈A∩B; x∈B ⟧ ⟹ canonical_retraction A C ` x = the_apartment_iso B A ` x" using canonical_retraction_uniform fun_eq_on_im[of _ _ _ x] by fast lemma canonical_retraction_simplex_im: assumes "A∈𝒜" "chamber C" "C∈A" shows "canonical_retraction A C ⊢ X = A" proof (rule seteqI) fix y assume "y ∈ canonical_retraction A C ⊢ X" from this obtain x where x: "x∈X" "y = canonical_retraction A C ` x" by fast from x(1) obtain D where D: "chamber D" "x⊆D" using simplex_in_max by fast from assms(2) D(1) obtain B where "B∈𝒜" "D∈B" "C∈B" using containtwo by fast with assms D(2) x(2) show "y∈A" using the_apartment_isoD(1)[of B A] ChamberComplexIsomorphism.surj_simplex_map canonical_retraction_uniform_im apartment_faces[of B D x] by fastforce next fix a assume "a∈A" with assms show "a ∈ canonical_retraction A C ⊢ X" using canonical_retraction_simplex_retraction2[of A C a, THEN sym] apartment_simplices by fast qed lemma canonical_retraction_vertex_im: "⟦ A∈𝒜; chamber C; C∈A ⟧ ⟹ canonical_retraction A C ` ⋃X = ⋃A" using singleton_simplex ChamberComplex.singleton_simplex complexes canonical_retraction_simplex_im[of A C] by blast lemma canonical_retraction: assumes "A∈𝒜" "chamber C" "C∈A" shows "ChamberComplexRetraction X (canonical_retraction A C)" proof fix D assume "chamber D" with assms show "chamber (canonical_retraction A C ` D)" "card (canonical_retraction A C ` D) = card D" using containtwo[of C D] canonical_retraction_uniform_im the_apartment_iso_chamber_map chamber_in_apartment ChamberComplexIsomorphism.dim_map[OF the_apartment_isoD(1)] by auto next fix v from assms show "v∈⋃X ⟹ canonical_retraction A C (canonical_retraction A C v) = canonical_retraction A C v" using canonical_retraction_retraction canonical_retraction_vertex_im by fast qed (simp add: canonical_retraction_def) lemma canonical_retraction_comp_endomorphism: "⟦ A∈𝒜; B∈𝒜; chamber C; chamber D; C∈A; D∈B ⟧ ⟹ ChamberComplexEndomorphism X (canonical_retraction A C ∘ canonical_retraction B D)" using canonical_retraction[of A C] canonical_retraction[of B D] ChamberComplexRetraction.axioms(1) ChamberComplexEndomorphism.endo_comp by fast lemma canonical_retraction_comp_simplex_im_subset: "⟦ A∈𝒜; B∈𝒜; chamber C; chamber D; C∈A; D∈B ⟧ ⟹ (canonical_retraction A C ∘ canonical_retraction B D) ⊢ X ⊆ A" using canonical_retraction[of B D] ChamberComplexRetraction.simplex_map canonical_retraction_simplex_im[of A C] by (force simp add: image_comp[THEN sym]) lemma canonical_retraction_comp_apartment_endomorphism: "⟦ A∈𝒜; B∈𝒜; chamber C; chamber D; C∈A; D∈B ⟧ ⟹ ChamberComplexEndomorphism A (restrict1 (canonical_retraction A C ∘ canonical_retraction B D) (⋃A))" using ChamberComplexEndomorphism.restrict_endo[of X _ A] canonical_retraction_comp_endomorphism[of A B C D] subcomplexes[of A] canonical_retraction_comp_simplex_im_subset[of A B C D] apartment_simplices[of A] by auto end (* context ChamberComplexWithApartmentSystem *) subsubsection ‹Distances in apartments› text ‹ Here we examine distances between chambers and between a facet and a chamber, especially with respect to canonical retractions onto an apartment. Note that a distance measured within an apartment is equal to the distance measured between the same objects in the wider chamber complex. In other words, the shortest distance between chambers can always be achieved within an apartment. › context ChamberComplexWithApartmentSystem begin lemma apartment_chamber_distance: assumes "A∈𝒜" "chamber C" "chamber D" "C∈A" "D∈A" shows "ChamberComplex.chamber_distance A C D = chamber_distance C D" proof (cases "C=D") case True with assms(1) show ?thesis using apartment_chamber_distance_def chamber_distance_def by simp next case False define Cs Ds f where "Cs = (ARG_MIN length Cs. ChamberComplex.gallery A (C#Cs@[D]))" and "Ds = (ARG_MIN length Ds. gallery (C#Ds@[D]))" and "f = canonical_retraction A C" from assms(2,3) False Ds_def have 1: "gallery (C#Ds@[D])" using gallery_least_length by fast with assms(1,2,4,5) f_def have "gallery (C # f⊨Ds @ [D])" using canonical_retraction ChamberComplexRetraction.gallery_map[of X] canonical_retraction_simplex_retraction2 by fastforce moreover from f_def assms(1,2,4) have "set (f⊨Ds) ⊆ A" using 1 galleryD_chamber chamberD_simplex canonical_retraction_simplex_im[of A C] by auto ultimately have "ChamberComplex.gallery A (C # f⊨Ds @ [D])" using assms(1,4,5) gallery_in_apartment by simp with assms(1) Ds_def False have "ChamberComplex.chamber_distance A C D ≤ chamber_distance C D" using ChamberComplex.chamber_distance_le[OF complexes] chamber_distance_def by force moreover from assms False Cs_def have "chamber_distance C D ≤ ChamberComplex.chamber_distance A C D" using chamber_in_apartment apartment_gallery_least_length subcomplex_gallery[OF subcomplexes] chamber_distance_le apartment_chamber_distance_def by simp ultimately show ?thesis by simp qed lemma apartment_min_gallery: assumes "A∈𝒜" "ChamberComplex.min_gallery A Cs" shows "min_gallery Cs" proof (cases Cs rule: list_cases_Cons_snoc) case Single with assms show ?thesis using apartment_min_galleryD_gallery apartment_gallery galleryD_chamber by fastforce next case (Cons_snoc C Ds D) moreover with assms have "min_gallery (C#Ds@[D])" using apartment_min_galleryD_gallery[of A Cs] apartment_gallery[of A Cs] apartment_galleryD_chamber apartment_chamberD_simplex ChamberComplex.min_gallery_betw_chamber_distance[ OF complexes, of A C Ds D ] galleryD_chamber apartment_chamber_distance min_galleryI_chamber_distance_betw by auto ultimately show ?thesis by fast qed simp lemma apartment_face_distance: assumes "A∈𝒜" "chamber C" "C∈A" "F∈A" shows "ChamberComplex.face_distance A F C = face_distance F C" proof- define D D' where "D = closest_supchamber F C" and "D' = ChamberComplex.closest_supchamber A F C" from assms D'_def have chamber_D': "ChamberComplex.chamber A D'" using chamber_in_apartment ChamberComplex.closest_supchamberD(1) complexes by fast with assms(1,2,4) D_def have chambers: "chamber D" "chamber D'" using closest_supchamberD(1)[of F C] apartment_chamber apartment_simplices by auto from assms(1-3) have 1: "ChamberComplex.chamber_distance A D' C = chamber_distance D' C" using chamber_D' chambers(2) apartment_chamberD_simplex apartment_chamber_distance by fastforce from assms D_def D'_def have F_DD': "F⊆D" "F⊆D'" using apartment_simplices[of A] closest_supchamberD(2) chamber_in_apartment ChamberComplex.closest_supchamberD(2)[OF complexes] by auto from assms(2) obtain B where B: "B∈𝒜" "C∈B" "D∈B" using chambers(1) containtwo by fast moreover from assms B have "the_apartment_iso B A ` F = F" using F_DD'(1) apartment_faces the_apartment_iso_int_im by force moreover have "the_apartment_iso B A ` F ⊆ the_apartment_iso B A ` D" using F_DD'(1) by fast ultimately have "chamber_distance D C ≥ chamber_distance D' C" using assms(1-3) D'_def 1 chambers(1) apartment_chamber_distance[of B] chamber_in_apartment[of B D] chamber_in_apartment[of B C] ChamberComplexIsomorphism.chamber_map[ OF the_apartment_isoD(1), of B A] ChamberComplex.closest_supchamber_closest[ OF complexes, of A "the_apartment_iso B A ` D" F C] ChamberComplexIsomorphism.chamber_distance_map[ OF the_apartment_isoD(1), of B A C] the_apartment_iso_int_im[of B A C C] by force moreover from assms D_def have "chamber_distance D C ≤ chamber_distance D' C" using closest_supchamber_closest chambers(2) F_DD'(2) by simp ultimately show ?thesis using assms(1) D_def D'_def face_distance_def 1 ChamberComplex.face_distance_def[OF complexes] by simp qed lemma apartment_face_distance_eq_chamber_distance_compare_other_chamber: assumes "A∈𝒜" "chamber C" "chamber D" "chamber E" "C∈A" "D∈A" "E∈A" "z⊲C" "z⊲D" "C≠D" "chamber_distance C E ≤ chamber_distance D E" shows "face_distance z E = chamber_distance C E" using assms apartment_chamber_distance apartment_face_distance facetrel_subset[of z C] apartment_faces[of A C z] chamber_in_apartment ThinChamberComplex.face_distance_eq_chamber_distance_compare_other_chamber[ OF thincomplexes, of A C D z E ] by auto lemma canonical_retraction_face_distance_map: assumes "A∈𝒜" "chamber C" "chamber D" "C∈A" "F⊆C" shows "face_distance F (canonical_retraction A C ` D) = face_distance F D" proof- from assms(2,3) obtain B where B: "B∈𝒜" "C∈B" "D∈B" using containtwo by fast with assms show ?thesis using apartment_faces[of A C F] apartment_faces[of B C F] apartment_face_distance chamber_in_apartment the_apartment_iso_int_im the_apartment_iso_chamber_map the_apartment_iso_apartment_simplex_map apartment_face_distance canonical_retraction_uniform_im ChamberComplexIsomorphism.face_distance_map[ OF the_apartment_isoD(1), of B A C D F ] by simp qed end (* context ChamberComplexWithApartmentSystem *) subsubsection ‹Special situation: a triangle of apartments and chambers› text ‹ To facilitate proving that apartments in buildings have sufficient foldings to be Coxeter, we explore the situation of three chambers sharing a common facet, along with three apartments, each of which contains two of the chambers. A folding of one of the apartments is constructed by composing two apartment retractions, and by symmetry we automatically obtain an opposed folding. › locale ChamberComplexApartmentSystemTriangle = ChamberComplexWithApartmentSystem X 𝒜 for X :: "'a set set" and 𝒜 :: "'a set set set" + fixes A B B' :: "'a set set" and C D E z :: "'a set" assumes apartments : "A∈𝒜" "B∈𝒜" "B'∈𝒜" and chambers : "chamber C" "chamber D" "chamber E" and facet : "z⊲C" "z⊲D" "z⊲E" and in_apartments: "C∈A∩B" "D∈A∩B'" "E∈B∩B'" and chambers_ne : "D≠C" "E≠D" "C≠E" begin abbreviation "fold_A ≡ canonical_retraction A D ∘ canonical_retraction B C" abbreviation "res_fold_A ≡ restrict1 fold_A (⋃A)" abbreviation "opp_fold_A ≡ canonical_retraction A C ∘ canonical_retraction B' D" abbreviation "res_opp_fold_A ≡ restrict1 opp_fold_A (⋃A)" lemma rotate: "ChamberComplexApartmentSystemTriangle X 𝒜 B' A B D E C z" using apartments chambers facet in_apartments chambers_ne by unfold_locales auto lemma reflect: "ChamberComplexApartmentSystemTriangle X 𝒜 A B' B D C E z" using apartments chambers facet in_apartments chambers_ne by unfold_locales auto lemma facet_in_chambers: "z⊆C" "z⊆D" "z⊆E" using facet facetrel_subset by auto lemma A_chambers: "ChamberComplex.chamber A C" "ChamberComplex.chamber A D" using apartments(1) chambers(1,2) in_apartments(1,2) chamber_in_apartment by auto lemma res_fold_A_A_chamber_image: "ChamberComplex.chamber A F ⟹ res_fold_A ` F = fold_A ` F" using apartments(1) apartment_chamberD_simplex restrict1_image by fastforce lemma the_apartment_iso_middle_im: "the_apartment_iso A B ` D = E" proof (rule ChamberComplexIsomorphism.thin_image_shared_facet) from apartments(1,2) chambers(1) in_apartments(1) show "ChamberComplexIsomorphism A B (the_apartment_iso A B)" using the_apartment_isoD(1) by fast from apartments(2) chambers(3) in_apartments(3) show "ChamberComplex.chamber B E" "ThinChamberComplex B" using chamber_in_apartment thincomplexes by auto from apartments(1,2) in_apartments(1) have "z ∈ A∩B" using facet_in_chambers(1) apartment_faces by fastforce with apartments(1,2) chambers(1) in_apartments(1) chambers_ne(3) facet(3) show "the_apartment_iso A B ` z ⊲ E" "E ≠ the_apartment_iso A B ` C" using the_apartment_iso_int_im by auto qed ( rule A_chambers(1), rule A_chambers(2), rule facet(1), rule facet(2), rule chambers_ne(1)[THEN not_sym] ) lemma inside_canonical_retraction_chamber_images: "canonical_retraction B C ` C = C" "canonical_retraction B C ` D = E" "canonical_retraction B C ` E = E" using apartments(1,2) chambers(1,2) in_apartments canonical_retraction_simplex_retraction2[of B C C] canonical_retraction_uniform_im the_apartment_iso_middle_im canonical_retraction_simplex_retraction2 by auto lemmas in_canretract_chimages = inside_canonical_retraction_chamber_images lemma outside_canonical_retraction_chamber_images: "canonical_retraction A D ` C = C" "canonical_retraction A D ` D = D" "canonical_retraction A D ` E = C" using ChamberComplexApartmentSystemTriangle.in_canretract_chimages[ OF rotate ] by auto lemma fold_A_chamber_images: "fold_A ` C = C" "fold_A ` D = C" "fold_A ` E = C" using inside_canonical_retraction_chamber_images outside_canonical_retraction_chamber_images image_comp[of "canonical_retraction A D" "canonical_retraction B C" C] image_comp[of "canonical_retraction A D" "canonical_retraction B C" D] image_comp[of "canonical_retraction A D" "canonical_retraction B C" E] by auto lemmas opp_fold_A_chamber_images = ChamberComplexApartmentSystemTriangle.fold_A_chamber_images[OF reflect] lemma res_fold_A_chamber_images: "res_fold_A ` C = C" "res_fold_A ` D = C" using in_apartments(1,2) fold_A_chamber_images(1,2) res_fold_A_A_chamber_image A_chambers(1,2) by auto lemmas res_opp_fold_A_chamber_images = ChamberComplexApartmentSystemTriangle.res_fold_A_chamber_images[OF reflect] lemma fold_A_fixespointwise1: "fixespointwise fold_A C" using apartments(1,2) chambers(1,2) in_apartments(1,2) canonical_retraction_simplex_retraction1 by (auto intro: fixespointwise_comp) lemmas opp_fold_A_fixespointwise2 = ChamberComplexApartmentSystemTriangle.fold_A_fixespointwise1[OF reflect] lemma fold_A_facet_im: "fold_A ` z = z" using facet_in_chambers(1) fixespointwise_im[OF fold_A_fixespointwise1] by simp lemma fold_A_endo_X: "ChamberComplexEndomorphism X fold_A" using apartments(1,2) chambers(1,2) in_apartments(1,2) canonical_retraction_comp_endomorphism by fast lemma res_fold_A_endo_A: "ChamberComplexEndomorphism A res_fold_A" using apartments(1,2) chambers(1,2) in_apartments(1,2) canonical_retraction_comp_apartment_endomorphism by fast lemmas opp_res_fold_A_endo_A = ChamberComplexApartmentSystemTriangle.res_fold_A_endo_A[OF reflect] lemma fold_A_morph_A_A: "ChamberComplexMorphism A A fold_A" using ChamberComplexEndomorphism.axioms(1)[OF res_fold_A_endo_A] ChamberComplexMorphism.cong fun_eq_on_sym[OF fun_eq_on_restrict1] by fast lemmas opp_fold_A_morph_A_A = ChamberComplexApartmentSystemTriangle.fold_A_morph_A_A[OF reflect] lemma res_fold_A_A_im_fold_A_A_im: "res_fold_A ⊢ A = fold_A ⊢ A" using setsetmapim_restrict1[of A A fold_A] by simp lemmas res_opp_fold_A_A_im_opp_fold_A_A_im = ChamberComplexApartmentSystemTriangle.res_fold_A_A_im_fold_A_A_im[ OF reflect ] lemma res_fold_A_𝒞_A_im_fold_A_𝒞_A_im: "res_fold_A ⊢ (ChamberComplex.chamber_system A) = fold_A ⊢ (ChamberComplex.chamber_system A)" using setsetmapim_restrict1[of "(ChamberComplex.chamber_system A)" A] apartments(1) apartment_chamber_system_simplices by blast lemmas res_opp_fold_A_𝒞_A_im_opp_fold_A_𝒞_A_im = ChamberComplexApartmentSystemTriangle.res_fold_A_𝒞_A_im_fold_A_𝒞_A_im[ OF reflect ] lemma chambercomplex_fold_A_im: "ChamberComplex (fold_A ⊢ A)" using ChamberComplexMorphism.chambercomplex_image[OF fold_A_morph_A_A] by simp lemmas chambercomplex_opp_fold_A_im = ChamberComplexApartmentSystemTriangle.chambercomplex_fold_A_im[ OF reflect ] lemma chambersubcomplex_fold_A_im: "ChamberComplex.ChamberSubcomplex A (fold_A ⊢ A)" using ChamberComplexMorphism.chambersubcomplex_image[OF fold_A_morph_A_A] by simp lemmas chambersubcomplex_opp_fold_A_im = ChamberComplexApartmentSystemTriangle.chambersubcomplex_fold_A_im[ OF reflect ] lemma fold_A_facet_distance_map: "chamber F ⟹ face_distance z (fold_A`F) = face_distance z F" using apartments(1,2) chambers in_apartments(1,2) facet_in_chambers(1,2) ChamberComplexRetraction.chamber_map[ OF canonical_retraction, of B C F ] canonical_retraction_face_distance_map[of A D "canonical_retraction B C ` F"] canonical_retraction_face_distance_map by (simp add: image_comp) lemma fold_A_min_gallery_betw_map: assumes "chamber F" "chamber G" "z⊆F" "face_distance z G = chamber_distance F G" "min_gallery (F#Fs@[G])" shows "min_gallery (fold_A⊨(F#Fs@[G]))" using assms fold_A_facet_im fold_A_facet_distance_map ChamberComplexEndomorphism.facedist_chdist_mingal_btwmap[ OF fold_A_endo_X, of F G z ] by force lemma fold_A_chamber_system_image_fixespointwise': defines 𝒞_A : "𝒞_A ≡ ChamberComplex.𝒞 A" defines f𝒞_A: "f𝒞_A ≡ {F∈𝒞_A. face_distance z F = chamber_distance C F}" assumes F : "F∈f𝒞_A" shows "fixespointwise fold_A F" proof- show ?thesis proof (cases "F=C") case True thus ?thesis using fold_A_fixespointwise1 fixespointwise_restrict1 by fast next case False from apartments(1) assms have Achamber_F: "ChamberComplex.chamber A F" using complexes ChamberComplex.chamber_system_def by fast define Fs where "Fs = (ARG_MIN length Fs. ChamberComplex.gallery A (C#Fs@[F]))" show ?thesis proof (rule apartment_standard_uniqueness_pgallery_betw, rule apartments(1)) show "ChamberComplexMorphism A A fold_A" using fold_A_morph_A_A by fast from apartments(1) show "ChamberComplexMorphism A A id" using apartment_trivial_morphism by fast show "fixespointwise fold_A C" using fold_A_fixespointwise1 fixespointwise_restrict1 by fast from apartments(1) False Fs_def show 1: "ChamberComplex.gallery A (C#Fs@[F])" using A_chambers(1) Achamber_F apartment_gallery_least_length by fast from False Fs_def apartments(1) have mingal: "min_gallery (C # Fs @ [F])" using A_chambers(1) Achamber_F apartment_min_gallery apartment_min_gallery_least_length by fast from apartments(1) have set_A: "set (C#Fs@[F]) ⊆ A" using 1 apartment_galleryD_chamber apartment_chamberD_simplex by fast with apartments(1) have "set (fold_A ⊨ (C#Fs@[F])) ⊆ A" using ChamberComplexMorphism.simplex_map[OF fold_A_morph_A_A] by auto with f𝒞_A F show "ChamberComplex.pgallery A (fold_A ⊨ (C#Fs@[F]))" using chambers(1) apartments(1) apartment_chamber Achamber_F facet_in_chambers(1) mingal fold_A_min_gallery_betw_map[of C F] min_gallery_in_apartment apartment_min_gallery_pgallery by auto from apartments(1) False Fs_def show "ChamberComplex.pgallery A (id ⊨ (C#Fs@[F]))" using A_chambers(1) Achamber_F ChamberComplex.pgallery_least_length[OF complexes] by auto qed qed qed lemma fold_A_chamber_system_image: defines 𝒞_A : "𝒞_A ≡ ChamberComplex.𝒞 A" defines f𝒞_A: "f𝒞_A ≡ {F∈𝒞_A. face_distance z F = chamber_distance C F}" shows "fold_A ⊢ 𝒞_A = f𝒞_A" proof (rule seteqI) fix F assume F: "F ∈ fold_A ⊢ 𝒞_A" with 𝒞_A have "F∈𝒞_A" using ChamberComplexMorphism.chamber_system_into[OF fold_A_morph_A_A] by fast moreover have "face_distance z F = chamber_distance C F" proof (cases "F=C") case False have F_ne_C: "F≠C" by fact from F obtain G where G: "G∈𝒞_A" "F = fold_A ` G" by fast with 𝒞_A apartments(1) have G': "chamber G" "G∈A" using apartment_chamber_system_def complexes apartment_chamber apartment_chamberD_simplex by auto show ?thesis proof (cases "chamber_distance C G ≤ chamber_distance D G") case True thus "face_distance z F = chamber_distance C F" using apartments(1) chambers(1,2) in_apartments(1,2) facet(1,2) chambers_ne(1) F_ne_C G(2) G' fold_A_chamber_images(1) facet_in_chambers(1) fold_A_facet_distance_map fold_A_facet_im apartment_face_distance_eq_chamber_distance_compare_other_chamber[ of A C D G z ] ChamberComplexEndomorphism.face_distance_eq_chamber_distance_map[ OF fold_A_endo_X, of C G z ] by auto next case False thus "face_distance z F = chamber_distance C F" using apartments(1) chambers(1,2) in_apartments(1,2) facet(1,2) chambers_ne(1) F_ne_C G(2) G' fold_A_chamber_images(2) facet_in_chambers(2) fold_A_facet_distance_map fold_A_facet_im apartment_face_distance_eq_chamber_distance_compare_other_chamber[ of A D C G z ] ChamberComplexEndomorphism.face_distance_eq_chamber_distance_map[ OF fold_A_endo_X, of D G z ] by auto qed qed (simp add: chambers(1) facet_in_chambers(1) face_distance_eq_0 chamber_distance_def) ultimately show "F∈f𝒞_A" using f𝒞_A by fast next from 𝒞_A f𝒞_A show "⋀F. F∈f𝒞_A ⟹ F∈fold_A ⊢ 𝒞_A" using fold_A_chamber_system_image_fixespointwise' fixespointwise_im by blast qed lemmas opp_fold_A_chamber_system_image = ChamberComplexApartmentSystemTriangle.fold_A_chamber_system_image[ OF reflect ] lemma fold_A_chamber_system_image_fixespointwise: "F ∈ ChamberComplex.𝒞 A ⟹ fixespointwise fold_A (fold_A`F)" using fold_A_chamber_system_image fold_A_chamber_system_image_fixespointwise'[of "fold_A`F"] by auto lemmas fold_A_chsys_imfix = fold_A_chamber_system_image_fixespointwise lemmas opp_fold_A_chamber_system_image_fixespointwise = ChamberComplexApartmentSystemTriangle.fold_A_chsys_imfix[ OF reflect ] lemma chamber_in_fold_A_im: "chamber F ⟹ F ∈ fold_A ⊢ A ⟹ F ∈ fold_A ⊢ ChamberComplex.𝒞 A" using apartments(1) ChamberComplexMorphism.chamber_system_image[OF fold_A_morph_A_A] ChamberComplexMorphism.simplex_map[OF fold_A_morph_A_A] chamber_in_apartment apartment_chamber_system_def by fastforce lemmas chamber_in_opp_fold_A_im = ChamberComplexApartmentSystemTriangle.chamber_in_fold_A_im[OF reflect] lemma simplex_in_fold_A_im_image: assumes "x ∈ fold_A ⊢ A" shows "fold_A ` x = x" proof- from assms apartments(1) obtain C where "C ∈ ChamberComplex.𝒞 A" "x ⊆ fold_A`C" using apartment_simplex_in_max apartment_chamber_system_def by fast thus ?thesis using fold_A_chamber_system_image_fixespointwise fixespointwise_im by blast qed lemma chamber1_notin_rfold_im: "C ∉ opp_fold_A ⊢ A" using chambers(1,2) facet(1,2) chambers_ne(1) facet_in_chambers(1) min_gallery_adj adjacentI[of z] face_distance_eq_0 min_gallery_betw_chamber_distance[of D "[]" C] chamber_in_opp_fold_A_im[of C] opp_fold_A_chamber_system_image by auto lemma fold_A_min_gallery_from1_map: "⟦ chamber F; F ∈ fold_A ⊢ A; min_gallery (C#Fs@[F]) ⟧ ⟹ min_gallery (C # fold_A ⊨ Fs @ [F])" using chambers(1) chamber_in_fold_A_im fold_A_chamber_system_image facet_in_chambers(1) fold_A_min_gallery_betw_map[of C F] fold_A_chamber_images(1) simplex_in_fold_A_im_image by simp lemma fold_A_min_gallery_from2_map: "⟦ chamber F; F ∈ opp_fold_A ⊢ A; min_gallery (D#Fs@[F]) ⟧ ⟹ min_gallery (C # fold_A ⊨ (Fs@[F]))" using chambers(2) facet_in_chambers(2) chamber_in_opp_fold_A_im opp_fold_A_chamber_system_image fold_A_chamber_images(2) fold_A_min_gallery_betw_map[of D F Fs] by simp lemma fold_A_min_gallery_to2_map: assumes "chamber F" "F ∈ opp_fold_A ⊢ A" "min_gallery (F#Fs@[D])" shows "min_gallery (fold_A ⊨ (F#Fs) @ [C])" using assms(1,2) min_gallery_rev[of "C # fold_A ⊨ (rev Fs @ [F])"] min_gallery_rev[OF assms(3)] fold_A_min_gallery_from2_map[of F "rev Fs"] fold_A_chamber_images(2) by (simp add: rev_map[THEN sym]) lemmas opp_fold_A_min_gallery_from1_map = ChamberComplexApartmentSystemTriangle.fold_A_min_gallery_from2_map[ OF reflect ] lemmas opp_fold_A_min_gallery_to1_map = ChamberComplexApartmentSystemTriangle.fold_A_min_gallery_to2_map[ OF reflect ] lemma closer_to_chamber1_not_in_rfold_im_chamber_system: assumes "chamber_distance C F ≤ chamber_distance D F" shows "F ∉ ChamberComplex.𝒞 (opp_fold_A ⊢ A)" proof assume "F ∈ ChamberComplex.𝒞 (opp_fold_A ⊢ A)" hence F: "F ∈ res_opp_fold_A ⊢ ChamberComplex.𝒞 A" using res_opp_fold_A_A_im_opp_fold_A_A_im ChamberComplexEndomorphism.image_chamber_system[ OF opp_res_fold_A_endo_A ] by simp hence F': "F ∈ opp_fold_A ⊢ ChamberComplex.𝒞 A" using res_opp_fold_A_𝒞_A_im_opp_fold_A_𝒞_A_im by simp from apartments(1) have Achamber_F: "ChamberComplex.chamber A F" using F apartment_chamber_system_def[of A] ChamberComplexEndomorphism.chamber_system_image[ OF opp_res_fold_A_endo_A ] by auto from apartments(1) have F_ne_C: "F≠C" using F' apartment_chamber_system_simplices[of A] chamber1_notin_rfold_im by auto have "fixespointwise opp_fold_A C" proof (rule apartment_standard_uniqueness_pgallery_betw, rule apartments(1)) show "ChamberComplexMorphism A A opp_fold_A" using opp_fold_A_morph_A_A by fast from apartments(1) show "ChamberComplexMorphism A A id" using apartment_trivial_morphism by fast show "fixespointwise opp_fold_A F" using F' opp_fold_A_chamber_system_image_fixespointwise by fast define Fs where "Fs = (ARG_MIN length Fs. ChamberComplex.gallery A (F#Fs@[C]))" with apartments(1) have mingal: "ChamberComplex.min_gallery A (F#Fs@[C])" using A_chambers(1) Achamber_F F_ne_C apartment_min_gallery_least_length[of A F C] by fast with apartments(1) show 5: "ChamberComplex.gallery A (F#Fs@[C])" and "ChamberComplex.pgallery A (id ⊨ (F#Fs@[C]))" using apartment_min_galleryD_gallery apartment_min_gallery_pgallery by auto have "min_gallery (opp_fold_A ⊨ (F#Fs) @ [D])" proof (rule opp_fold_A_min_gallery_to1_map) from apartments(1) show "chamber F" using Achamber_F apartment_chamber by fast from assms have "F ∈ fold_A ⊢ ChamberComplex.𝒞 A" using apartments(1) chambers(1,2) in_apartments(1,2) facet(1,2) chambers_ne(1) Achamber_F apartment_chamber apartment_chamberD_simplex apartment_face_distance_eq_chamber_distance_compare_other_chamber apartment_chamber_system_def fold_A_chamber_system_image apartment_chamber_system_simplices by simp with apartments(1) show "F ∈ fold_A ⊢ A" using apartment_chamber_system_simplices[of A] by auto from apartments(1) show "min_gallery (F # Fs @ [C])" using mingal apartment_min_gallery by fast qed hence "min_gallery (opp_fold_A ⊨ (F#Fs@[C]))" using opp_fold_A_chamber_images(2) by simp moreover from apartments(1) have "set (opp_fold_A ⊨ (F#Fs@[C])) ⊆ A" using 5 apartment_galleryD_chamber[of A] apartment_chamberD_simplex[of A] ChamberComplexMorphism.simplex_map[OF opp_fold_A_morph_A_A] by auto ultimately have "ChamberComplex.min_gallery A (opp_fold_A ⊨ (F#Fs@[C]))" using apartments(1) min_gallery_in_apartment by fast with apartments(1) show "ChamberComplex.pgallery A (opp_fold_A ⊨ (F#Fs@[C]))" using apartment_min_gallery_pgallery by fast qed hence "opp_fold_A ` C = C" using fixespointwise_im by fast with chambers_ne(1) show False using opp_fold_A_chamber_images(2) by fast qed lemmas clsrch1_nin_rfold_im_chsys = closer_to_chamber1_not_in_rfold_im_chamber_system lemmas closer_to_chamber2_not_in_fold_im_chamber_system = ChamberComplexApartmentSystemTriangle.clsrch1_nin_rfold_im_chsys[ OF reflect ] lemma fold_A_opp_fold_A_chamber_systems: "ChamberComplex.𝒞 A = (ChamberComplex.𝒞 (fold_A ⊢ A)) ∪ (ChamberComplex.𝒞 (opp_fold_A ⊢ A))" "(ChamberComplex.𝒞 (fold_A ⊢ A)) ∩ (ChamberComplex.𝒞 (opp_fold_A ⊢ A)) = {}" proof (rule seteqI) fix F assume F: "F ∈ ChamberComplex.𝒞 A" with apartments(1) have F': "ChamberComplex.chamber A F" "F∈A" using apartment_chamber_system_def apartment_chamber_system_simplices apartment_chamber by auto from F'(1) apartments(1) have F'': "chamber F" using apartment_chamber by auto show "F ∈ (ChamberComplex.𝒞 (fold_A ⊢ A)) ∪ (ChamberComplex.𝒞 (opp_fold_A ⊢ A))" proof (cases "chamber_distance C F ≤ chamber_distance D F") case True thus ?thesis using apartments(1) chambers(1,2) in_apartments(1,2) facet(1,2) chambers_ne(1) F F'(2) F'' fold_A_chamber_system_image apartment_face_distance_eq_chamber_distance_compare_other_chamber ChamberComplexMorphism.image_chamber_system[OF fold_A_morph_A_A] by simp next case False thus ?thesis using apartments(1) chambers(1,2) in_apartments(1,2) facet(1,2) chambers_ne(1) F F'(2) F'' opp_fold_A_chamber_system_image apartment_face_distance_eq_chamber_distance_compare_other_chamber ChamberComplexMorphism.image_chamber_system[OF opp_fold_A_morph_A_A] by simp qed next fix F assume F: "F ∈ (ChamberComplex.𝒞 (fold_A ⊢ A)) ∪ (ChamberComplex.𝒞 (opp_fold_A ⊢ A))" thus "F ∈ ChamberComplex.𝒞 A" using ChamberComplexMorphism.image_chamber_system_image[ OF fold_A_morph_A_A ] ChamberComplexMorphism.image_chamber_system_image[ OF opp_fold_A_morph_A_A ] by fast next show "(ChamberComplex.𝒞 (fold_A ⊢ A)) ∩ (ChamberComplex.𝒞 (opp_fold_A ⊢ A)) = {}" using closer_to_chamber1_not_in_rfold_im_chamber_system closer_to_chamber2_not_in_fold_im_chamber_system by force qed lemma fold_A_im_min_gallery': assumes "ChamberComplex.min_gallery (fold_A ⊢ A) (C#Cs)" shows "ChamberComplex.min_gallery A (C#Cs)" proof (cases Cs rule: rev_cases) case Nil with apartments(1) show ?thesis using A_chambers(1) ChamberComplex.min_gallery_simps(2)[OF complexes] by simp next case (snoc Fs F) from assms snoc apartments(1) have ch: "∀H∈set (C#Fs@[F]). ChamberComplex.chamber A H" using ChamberComplex.min_galleryD_gallery ChamberComplex.galleryD_chamber chambercomplex_fold_A_im ChamberComplex.subcomplex_chamber[OF complexes] chambersubcomplex_fold_A_im by fastforce with apartments(1) have ch_F: "chamber F" using apartment_chamber by simp have "ChamberComplex.min_gallery A (C#Fs@[F])" proof (rule ChamberComplex.min_galleryI_betw_compare, rule complexes, rule apartments(1)) define Gs where "Gs = (ARG_MIN length Gs. ChamberComplex.gallery A (C#Gs@[F]))" from assms snoc show "C≠F" using ChamberComplex.min_gallery_pgallery ChamberComplex.pgalleryD_distinct chambercomplex_fold_A_im by fastforce with chambers(1) apartments(1) assms snoc Gs_def show 3: "ChamberComplex.min_gallery A (C#Gs@[F])" using ch apartment_min_gallery_least_length by simp from assms snoc apartments(1) show "ChamberComplex.gallery A (C#Fs@[F])" using ch ChamberComplex.min_galleryD_gallery ChamberComplex.galleryD_adj chambercomplex_fold_A_im ChamberComplex.gallery_def[OF complexes] by fastforce show "length Fs = length Gs" proof- from apartments(1) have set_gal: "set (C#Gs@[F]) ⊆ A" using 3 apartment_min_galleryD_gallery apartment_galleryD_chamber apartment_chamberD_simplex by fast from assms snoc have F_in: "F ∈ fold_A ⊢ A" using ChamberComplex.min_galleryD_gallery ChamberComplex.galleryD_chamber ChamberComplex.chamberD_simplex chambercomplex_fold_A_im by fastforce with apartments(1) have "min_gallery (C # fold_A ⊨ Gs @ [F])" using ch_F 3 apartment_min_gallery fold_A_min_gallery_from1_map by fast moreover have "set (fold_A ⊨ (C#Gs@[F])) ⊆ A" using set_gal ChamberComplexMorphism.simplex_map[OF fold_A_morph_A_A] by auto ultimately have "ChamberComplex.min_gallery A (C # fold_A ⊨ Gs @ [F])" using apartments(1) F_in min_gallery_in_apartment fold_A_chamber_images(1) fold_A_chamber_system_image_fixespointwise simplex_in_fold_A_im_image by simp moreover have "set (fold_A ⊨ (C#Gs@[F])) ⊆ fold_A ⊢ A" using set_gal by auto ultimately show ?thesis using assms snoc apartments(1) F_in fold_A_chamber_images(1) simplex_in_fold_A_im_image ChamberComplex.min_gallery_in_subcomplex[ OF complexes, OF _ chambersubcomplex_fold_A_im ] ChamberComplex.min_gallery_betw_uniform_length[ OF chambercomplex_fold_A_im, of C "fold_A ⊨ Gs" F Fs ] by simp qed qed with snoc show ?thesis by fast qed lemma fold_A_im_min_gallery: "ChamberComplex.min_gallery (fold_A ⊢ A) (C#Cs) ⟹ min_gallery (C#Cs)" using apartments(1) fold_A_im_min_gallery' apartment_min_gallery by fast lemma fold_A_comp_fixespointwise: "fixespointwise (fold_A ∘ opp_fold_A) (⋃ (fold_A ⊢ A))" proof (rule apartment_standard_uniqueness, rule apartments(1)) have "fun_eq_on (fold_A ∘ opp_fold_A) (res_fold_A ∘ res_opp_fold_A) (⋃A)" using ChamberComplexEndomorphism.vertex_map[OF opp_res_fold_A_endo_A] fun_eq_onI[of "⋃A" "fold_A ∘ opp_fold_A"] by auto thus "ChamberComplexMorphism (fold_A ⊢ A) A (fold_A ∘ opp_fold_A)" using ChamberComplexEndomorphism.endo_comp[ OF opp_res_fold_A_endo_A res_fold_A_endo_A ] ChamberComplexEndomorphism.axioms(1) ChamberComplexMorphism.cong ChamberComplexMorphism.restrict_domain chambersubcomplex_fold_A_im by fast from apartments(1) show "ChamberComplexMorphism (fold_A ⊢ A) A id" using ChamberComplexMorphism.restrict_domain apartment_trivial_morphism chambersubcomplex_fold_A_im by fast from apartments(1) show "ChamberComplex.chamber (fold_A ⊢ A) C" using A_chambers(1) apartment_chamberD_simplex fold_A_chamber_images(1) ChamberComplex.chamber_in_subcomplex[ OF complexes, OF _ chambersubcomplex_fold_A_im, of C ] by fast show "fixespointwise (fold_A ∘ opp_fold_A) C" proof- from facet(1) obtain v where v: "v∉z" "C = insert v z" using facetrel_def[of z C] by fast have "fixespointwise (fold_A ∘ opp_fold_A) (insert v z)" proof (rule fixespointwise_insert, rule fixespointwise_comp) show "fixespointwise opp_fold_A z" using facet_in_chambers(2) fixespointwise_subset[of opp_fold_A D z] opp_fold_A_fixespointwise2 by fast show "fixespointwise fold_A z" using facet_in_chambers(1) fixespointwise_subset[of fold_A C z] fold_A_fixespointwise1 by fast have "(fold_A ∘ opp_fold_A) ` C = C" using fold_A_chamber_images(2) opp_fold_A_chamber_images(2) by (simp add: image_comp[THEN sym]) with v(2) show "(fold_A ∘ opp_fold_A) ` (insert v z) = insert v z" by simp qed with v(2) show ?thesis by fast qed show "⋀Cs. ChamberComplex.min_gallery (fold_A ⊢ A) (C # Cs) ⟹ ChamberComplex.pgallery A ((fold_A ∘ opp_fold_A) ⊨ (C # Cs))" proof- fix Cs assume Cs: "ChamberComplex.min_gallery (fold_A ⊢ A) (C # Cs)" show "ChamberComplex.pgallery A ((fold_A ∘ opp_fold_A) ⊨ (C # Cs))" proof (cases Cs rule: rev_cases) case Nil with apartments(1) show ?thesis using fold_A_chamber_images(2) opp_fold_A_chamber_images(2) A_chambers(1) ChamberComplex.pgallery_def[OF complexes] by (auto simp add: image_comp[THEN sym]) next case (snoc Fs F) from Cs snoc apartments(1) have F: "F ∈ fold_A ⊢ A" "ChamberComplex.chamber A F" using ChamberComplex.min_galleryD_gallery[ OF chambercomplex_fold_A_im ] ChamberComplex.galleryD_chamber[ OF chambercomplex_fold_A_im, of "C#Fs@[F]" ] ChamberComplex.chamberD_simplex[OF chambercomplex_fold_A_im] ChamberComplex.subcomplex_chamber[ OF complexes, OF _ chambersubcomplex_fold_A_im ] by auto from F(2) apartments(1) have F': "chamber F" using apartment_chamber by fast with F(1) apartments(1) have zF_CF: "face_distance z F = chamber_distance C F" using chamber_in_fold_A_im[of F] fold_A_chamber_system_image by auto have "min_gallery (C # fold_A ⊨ (opp_fold_A ⊨ Fs @ [opp_fold_A ` F]))" proof (rule fold_A_min_gallery_from2_map) from Cs snoc have Cs': "ChamberComplex.gallery (fold_A ⊢ A) (C#Fs@[F])" using ChamberComplex.min_galleryD_gallery chambercomplex_fold_A_im by fastforce with apartments(1) have chF: "ChamberComplex.chamber A F" using ChamberComplex.galleryD_chamber chambercomplex_fold_A_im ChamberComplex.subcomplex_chamber[OF complexes] chambersubcomplex_fold_A_im by fastforce with apartments(1) show "chamber (opp_fold_A ` F)" using ChamberComplexMorphism.chamber_map opp_fold_A_morph_A_A apartment_chamber by fast from apartments(1) show "opp_fold_A ` F ∈ opp_fold_A ⊢ A" using chF ChamberComplex.chamberD_simplex complexes by fast from Cs snoc apartments(1) show "min_gallery (D # opp_fold_A ⊨ Fs @ [opp_fold_A ` F])" using chF Cs' opp_fold_A_min_gallery_from1_map apartment_chamber ChamberComplex.chamberD_simplex ChamberComplex.galleryD_chamber chambercomplex_fold_A_im fold_A_im_min_gallery by fastforce qed with snoc have "min_gallery (fold_A ⊨ (opp_fold_A ⊨ (C#Cs)))" using fold_A_chamber_images(2) opp_fold_A_chamber_images(2) by simp with Cs apartments(1) have "ChamberComplex.min_gallery A (fold_A ⊨ (opp_fold_A ⊨ (C#Cs)))" using ChamberComplex.min_galleryD_gallery[ OF chambercomplex_fold_A_im, of "C#Cs" ] ChamberComplex.galleryD_chamber[ OF chambercomplex_fold_A_im, of "C#Cs" ] ChamberComplex.subcomplex_chamber[ OF complexes, OF _ chambersubcomplex_fold_A_im ] apartment_chamberD_simplex ChamberComplexMorphism.simplex_map[OF opp_fold_A_morph_A_A] ChamberComplexMorphism.simplex_map[OF fold_A_morph_A_A] by (force intro: min_gallery_in_apartment) with apartments(1) have "ChamberComplex.pgallery A (fold_A ⊨ (opp_fold_A ⊨ (C#Cs)))" using apartment_min_gallery_pgallery by fast thus ?thesis using ssubst[ OF setlistmapim_comp, of "λCs. ChamberComplex.pgallery A Cs" ] by fast qed qed from apartments(1) show "⋀Cs. ChamberComplex.min_gallery (fold_A ⊢ A) Cs ⟹ ChamberComplex.pgallery A (id ⊨ Cs)" using chambersubcomplex_fold_A_im ChamberComplex.min_gallery_pgallery[OF chambercomplex_fold_A_im] ChamberComplex.subcomplex_pgallery[OF complexes, of A "fold_A ⊢ A"] by simp qed lemmas opp_fold_A_comp_fixespointwise = ChamberComplexApartmentSystemTriangle.fold_A_comp_fixespointwise[OF reflect] lemma fold_A_fold: "ChamberComplexIsomorphism (opp_fold_A ⊢ A) (fold_A ⊢ A) fold_A" proof (rule ChamberComplexMorphism.isoI_inverse) show "ChamberComplexMorphism (opp_fold_A ⊢ A) (fold_A ⊢ A) fold_A" using ChamberComplexMorphism.restrict_domain ChamberComplexMorphism.restrict_codomain_to_image ChamberComplexMorphism.cong fun_eq_on_sym[OF fun_eq_on_restrict1] ChamberComplexEndomorphism.axioms(1) res_fold_A_endo_A chambersubcomplex_opp_fold_A_im by fast show "ChamberComplexMorphism (fold_A ⊢ A) (opp_fold_A ⊢ A) opp_fold_A" using ChamberComplexMorphism.restrict_domain ChamberComplexMorphism.restrict_codomain_to_image ChamberComplexMorphism.cong fun_eq_on_sym[OF fun_eq_on_restrict1] ChamberComplexEndomorphism.axioms(1) opp_res_fold_A_endo_A chambersubcomplex_fold_A_im by fast qed (rule opp_fold_A_comp_fixespointwise, rule fold_A_comp_fixespointwise) lemma res_fold_A: "ChamberComplexFolding A res_fold_A" proof (rule ChamberComplexFolding.intro) have "ChamberComplexEndomorphism A (res_fold_A)" using res_fold_A_endo_A by fast thus "ChamberComplexRetraction A (res_fold_A)" proof (rule ChamberComplexRetraction.intro, unfold_locales) fix v assume "v∈⋃A" moreover with apartments(1) obtain C where "C ∈ ChamberComplex.𝒞 A" "v∈C" using apartment_simplex_in_max apartment_chamber_system_def by fast ultimately show "res_fold_A (res_fold_A v) = res_fold_A v" using fold_A_chamber_system_image_fixespointwise fixespointwiseD by fastforce qed show "ChamberComplexFolding_axioms A res_fold_A" proof fix F assume F: "ChamberComplex.chamber A F" "F ∈ res_fold_A ⊢ A" from F(2) have F': "F ∈ fold_A ⊢ A" using setsetmapim_restrict1[of A A fold_A] by simp hence "F ∈ fold_A ⊢ (opp_fold_A ⊢ A)" using ChamberComplexIsomorphism.surj_simplex_map[OF fold_A_fold] by simp from this obtain G where G: "G ∈ opp_fold_A ⊢ A" "F = fold_A ` G" by auto with F(1) F' apartments(1) have G': "ChamberComplex.chamber A G" "G ∈ ChamberComplex.𝒞 (opp_fold_A ⊢ A)" using ChamberComplex.chamber_in_subcomplex[OF complexes] chambersubcomplex_fold_A_im ChamberComplexIsomorphism.chamber_preimage[OF fold_A_fold, of G] ChamberComplex.subcomplex_chamber[ OF complexes, OF apartments(1) chambersubcomplex_opp_fold_A_im ] ChamberComplex.chamber_system_def[ OF chambercomplex_opp_fold_A_im ] by auto from apartments(1) G(2) have 1: "⋀H. ChamberComplex.chamber A H ∧ H ∉ fold_A ⊢ A ∧ fold_A ` H = F ⟹ H=G" using G'(2) apartment_chamber_system_def[of A] fold_A_opp_fold_A_chamber_systems(1) chambercomplex_fold_A_im ChamberComplex.chamber_system_def ChamberComplex.chamberD_simplex inj_onD[ OF ChamberComplexIsomorphism.inj_on_chamber_system, OF fold_A_fold ] by blast with apartments(1) have "⋀H. ChamberComplex.chamber A H ∧ H ∉ res_fold_A ⊢ A ∧ res_fold_A ` H = F ⟹ H=G" using 1 res_fold_A_A_chamber_image apartment_chamberD_simplex res_fold_A_A_im_fold_A_A_im by auto moreover from apartments(1) have "G ∉ res_fold_A ⊢ A" using G' ChamberComplex.chamber_system_def[OF chambercomplex_fold_A_im] ChamberComplex.chamber_in_subcomplex[ OF complexes, OF _ chambersubcomplex_fold_A_im ] fold_A_opp_fold_A_chamber_systems(2) res_fold_A_A_im_fold_A_A_im by auto ultimately show "∃!G. ChamberComplex.chamber A G ∧ G ∉ res_fold_A ⊢ A ∧ res_fold_A ` G = F" using G'(1) G(2) res_fold_A_A_chamber_image ex1I[of _ G] by force qed qed lemmas opp_res_fold_A = ChamberComplexApartmentSystemTriangle.res_fold_A[OF reflect] end (* context ChamberComplexApartmentSystemTriangle *) subsection ‹Building locale and basic lemmas› text ‹ Finally, we define a (thick) building to be a thick chamber complex with a system of apartments. › locale Building = ChamberComplexWithApartmentSystem X 𝒜 for X :: "'a set set" and 𝒜 :: "'a set set set" + assumes thick: "ThickChamberComplex X" begin abbreviation "some_third_chamber ≡ ThickChamberComplex.some_third_chamber X" lemmas some_third_chamberD_facet = ThickChamberComplex.some_third_chamberD_facet [OF thick] lemmas some_third_chamberD_ne = ThickChamberComplex.some_third_chamberD_ne [OF thick] lemmas chamber_some_third_chamber = ThickChamberComplex.chamber_some_third_chamber [OF thick] end (* context Building *) subsection ‹Apartments are uniformly Coxeter› text ‹ Using the assumption of thickness, we may use the special situation @{const ChamberComplexApartmentSystemTriangle} to verify that apartments have enough pairs of opposed foldings to ensure that they are isomorphic to a Coxeter complex. Since the apartments are all isomorphic, they are uniformly isomorphic to a single Coxeter complex. › context Building begin lemma apartments_have_many_foldings1: assumes "A∈𝒜" "chamber C" "chamber D" "C∼D" "C≠D" "C∈A" "D∈A" defines "E ≡ some_third_chamber C D (C∩D)" defines "B ≡ supapartment C E" and "B' ≡ supapartment D E" defines "f ≡ restrict1 (canonical_retraction A D ∘ canonical_retraction B C) (⋃A)" and "g ≡ restrict1 (canonical_retraction A C ∘ canonical_retraction B' D) (⋃A)" shows "f`D = C" "ChamberComplexFolding A f" "g`C = D" "ChamberComplexFolding A g" proof- from assms have 1: "ChamberComplexApartmentSystemTriangle X 𝒜 A B B' C D E (C∩D)" using adjacent_int_facet1[of C D] adjacent_int_facet2[of C D] some_third_chamberD_facet chamber_some_third_chamber some_third_chamberD_ne[of C "C∩D" D] supapartmentD by unfold_locales auto from f_def g_def show "ChamberComplexFolding A f" "ChamberComplexFolding A g" "f`D = C" "g`C = D" using ChamberComplexApartmentSystemTriangle.res_fold_A [OF 1] ChamberComplexApartmentSystemTriangle.opp_res_fold_A[OF 1] ChamberComplexApartmentSystemTriangle.res_fold_A_chamber_images(2)[ OF 1 ] ChamberComplexApartmentSystemTriangle.res_opp_fold_A_chamber_images(2)[ OF 1 ] by auto qed lemma apartments_have_many_foldings2: assumes "A∈𝒜" "chamber C" "chamber D" "C∼D" "C≠D" "C∈A" "D∈A" defines "E ≡ some_third_chamber C D (C∩D)" defines "B ≡ supapartment C E" and "B' ≡ supapartment D E" defines "f ≡ restrict1 (canonical_retraction A D ∘ canonical_retraction B C) (⋃A)" and "g ≡ restrict1 (canonical_retraction A C ∘ canonical_retraction B' D) (⋃A)" shows "OpposedThinChamberComplexFoldings A f g C" proof (rule OpposedThinChamberComplexFoldings.intro) from assms show "ChamberComplexFolding A f" "ChamberComplexFolding A g" using apartments_have_many_foldings1(2,4)[of A C D] by auto show "OpposedThinChamberComplexFoldings_axioms A f g C" proof ( unfold_locales, rule chamber_in_apartment, rule assms(1), rule assms(6), rule assms(2) ) from assms(1-7) E_def B_def B'_def g_def f_def have gC: "g`C = D" and fD: "f`D = C" using apartments_have_many_foldings1(1)[of A C D] apartments_have_many_foldings1(3)[of A C D] by auto with assms(4,5) show "C ∼ g`C" "C ≠ g`C" "f`g`C = C" by auto qed qed (rule thincomplexes, rule assms(1)) lemma apartments_have_many_foldings3: assumes "A∈𝒜" "chamber C" "chamber D" "C∼D" "C≠D" "C∈A" "D∈A" shows "∃f g. OpposedThinChamberComplexFoldings A f g C ∧ D=g`C" proof define E where "E = some_third_chamber C D (C∩D)" define B where "B = supapartment C E" define f where "f = restrict1 (canonical_retraction A D ∘ canonical_retraction B C) (⋃A)" show "∃g. OpposedThinChamberComplexFoldings A f g C ∧ D = g ` C" proof define B' where "B' = supapartment D E" define g where "g = restrict1 (canonical_retraction A C ∘ canonical_retraction B' D) (⋃A)" from assms E_def B_def f_def B'_def g_def show "OpposedThinChamberComplexFoldings A f g C ∧ D = g`C" using apartments_have_many_foldings1(3)[of A C D] apartments_have_many_foldings2 by auto qed qed lemma apartments_have_many_foldings: assumes "A∈𝒜" "C∈A" "chamber C" shows "ThinChamberComplexManyFoldings A C" proof ( rule ThinChamberComplex.ThinChamberComplexManyFoldingsI, rule thincomplexes, rule assms(1), rule chamber_in_apartment, rule assms(1), rule assms(2), rule assms(3) ) from assms(1) show "⋀C D. ChamberComplex.chamber A C ⟹ ChamberComplex.chamber A D ⟹ C∼D ⟹ C≠D ⟹ ∃f g. OpposedThinChamberComplexFoldings A f g C ∧ D = g ` C" using apartments_have_many_foldings3 apartment_chamber apartment_chamberD_simplex by simp qed theorem apartments_are_coxeter: "A∈𝒜 ⟹ ∃S::'a permutation set. ( CoxeterComplex S ∧ (∃ψ. ChamberComplexIsomorphism A (CoxeterComplex.TheComplex S) ψ) )" using no_trivial_apartments apartment_simplex_in_max[of A] apartment_chamberD_simplex[of A] apartment_chamber[of A] apartments_have_many_foldings[of A] ThinChamberComplexManyFoldings.ex_iso_to_coxeter_complex[of A] by fastforce corollary apartments_are_uniformly_coxeter: assumes "X≠{}" shows "∃S::'a permutation set. CoxeterComplex S ∧ (∀A∈𝒜. ∃ψ. ChamberComplexIsomorphism A (CoxeterComplex.TheComplex S) ψ )" proof- from assms obtain C where C: "chamber C" using simplex_in_max by fast from this obtain A where A: "A∈𝒜" "C∈A" using containtwo by fast from A(1) obtain S :: "'a permutation set" and ψ where S: "CoxeterComplex S" and ψ: "ChamberComplexIsomorphism A (CoxeterComplex.TheComplex S) ψ" using apartments_are_coxeter by fast have "∀B∈𝒜. ∃φ. ChamberComplexIsomorphism B (CoxeterComplex.TheComplex S) φ" proof fix B assume B: "B∈𝒜" hence "B≠{}" using no_trivial_apartments by fast with B obtain C' where C': "chamber C'" "C'∈B" using apartment_simplex_in_max apartment_chamberD_simplex apartment_chamber[OF B] by force from C C'(1) obtain B' where "B'∈𝒜" "C∈B'" "C'∈B'" using containtwo by fast with A B C C' ψ show "∃φ. ChamberComplexIsomorphism B (CoxeterComplex.TheComplex S) φ" using strong_intersecttwo ChamberComplexIsomorphism.iso_comp[of B' A _ _ ψ] ChamberComplexIsomorphism.iso_comp[of B B'] by blast qed with S show ?thesis by auto qed end (* context Building *) end (* theory *)