section ‹Chamber complexes› text ‹ Now we develop the basic theory of chamber complexes, including both thin and thick complexes. Some terminology: a maximal simplex is now called a chamber, and a chain (with respect to adjacency) of chambers is now called a gallery. A gallery in which no chamber appears more than once is called proper, and we use the prefix p as a naming convention to denote proper. Again, we remind the reader that some sources reserve the name gallery for (a slightly weaker notion of) what we are calling a proper gallery, using pregallery to denote an improper gallery. › theory Chamber imports Algebra Simplicial begin subsection ‹Locale definition and basic facts› locale ChamberComplex = SimplicialComplex X for X :: "'a set set" + assumes simplex_in_max : "y∈X ⟹ ∃x. maxsimp x ∧ y⊆x" and maxsimp_connect: "⟦ x ≠ y; maxsimp x; maxsimp y ⟧ ⟹ ∃xs. maxsimpchain (x#xs@[y])" context ChamberComplex begin abbreviation "chamber ≡ maxsimp" abbreviation "gallery ≡ maxsimpchain" abbreviation "pgallery ≡ pmaxsimpchain" abbreviation "min_gallery ≡ min_maxsimpchain" abbreviation "supchamber v ≡ (SOME C. chamber C ∧ v∈C)" lemmas faces = faces lemmas singleton_simplex = singleton_simplex lemmas chamberI = maxsimpI lemmas chamberD_simplex = maxsimpD_simplex lemmas chamberD_maximal = maxsimpD_maximal lemmas finite_chamber = finite_maxsimp lemmas chamber_nempty = maxsimp_nempty lemmas chamber_vertices = maxsimp_vertices lemmas gallery_def = maxsimpchain_def lemmas gallery_snocI = maxsimpchain_snocI lemmas galleryD_chamber = maxsimpchainD_maxsimp lemmas galleryD_adj = maxsimpchainD_adj lemmas gallery_CConsI = maxsimpchain_CConsI lemmas gallery_Cons_reduce = maxsimpchain_Cons_reduce lemmas gallery_append_reduce1 = maxsimpchain_append_reduce1 lemmas gallery_append_reduce2 = maxsimpchain_append_reduce2 lemmas gallery_remdup_adj = maxsimpchain_remdup_adj lemmas gallery_obtain_pgallery = maxsimpchain_obtain_pmaxsimpchain lemmas pgallery_def = pmaxsimpchain_def lemmas pgalleryI_gallery = pmaxsimpchainI_maxsimpchain lemmas pgalleryD_chamber = pmaxsimpchainD_maxsimp lemmas pgalleryD_adj = pmaxsimpchainD_adj lemmas pgalleryD_distinct = pmaxsimpchainD_distinct lemmas pgallery_Cons_reduce = pmaxsimpchain_Cons_reduce lemmas pgallery_append_reduce1 = pmaxsimpchain_append_reduce1 lemmas pgallery = pmaxsimpchain lemmas min_gallery_simps = min_maxsimpchain.simps lemmas min_galleryI_betw = min_maxsimpchainI_betw lemmas min_galleryI_betw_compare = min_maxsimpchainI_betw_compare lemmas min_galleryD_min_betw = min_maxsimpchainD_min_betw lemmas min_galleryD_gallery = min_maxsimpchainD_maxsimpchain lemmas min_gallery_pgallery = min_maxsimpchain_pmaxsimpchain lemmas min_gallery_rev = min_maxsimpchain_rev lemmas min_gallery_adj = min_maxsimpchain_adj lemmas not_min_galleryI_betw = not_min_maxsimpchainI_betw lemmas min_gallery_betw_CCons_reduce = min_maxsimpchain_betw_CCons_reduce lemmas min_gallery_betw_uniform_length = min_maxsimpchain_betw_uniform_length lemmas vertex_set_int = vertex_set_int[OF ChamberComplex.axioms(1)] lemma chamber_pconnect: "⟦ x ≠ y; chamber x; chamber y ⟧ ⟹ ∃xs. pgallery (x#xs@[y])" using maxsimp_connect[of x y] gallery_obtain_pgallery[of x y] by fast lemma supchamberD: assumes "v∈⋃X" defines "C ≡ supchamber v" shows "chamber C" "v∈C" using assms simplex_in_max someI[of "λC. chamber C ∧ v∈C"] by auto definition "ChamberSubcomplex Y ≡ Y ⊆ X ∧ ChamberComplex Y ∧ (∀C. ChamberComplex.chamber Y C ⟶ chamber C)" lemma ChamberSubcomplexI: assumes "Y⊆X" "ChamberComplex Y" "⋀y. ChamberComplex.chamber Y y ⟹ chamber y" shows "ChamberSubcomplex Y" using assms ChamberSubcomplex_def by fast lemma ChamberSubcomplexD_sub: "ChamberSubcomplex Y ⟹ Y ⊆ X" using ChamberSubcomplex_def by fast lemma ChamberSubcomplexD_complex: "ChamberSubcomplex Y ⟹ ChamberComplex Y" unfolding ChamberSubcomplex_def by fast lemma chambersub_imp_sub: "ChamberSubcomplex Y ⟹ Subcomplex Y" using ChamberSubcomplex_def ChamberComplex.axioms(1) by fast lemma chamber_in_subcomplex: "⟦ ChamberSubcomplex Y; C ∈ Y; chamber C ⟧ ⟹ ChamberComplex.chamber Y C" using chambersub_imp_sub max_in_subcomplex by simp lemma subcomplex_chamber: "ChamberSubcomplex Y ⟹ ChamberComplex.chamber Y C ⟹ chamber C" unfolding ChamberSubcomplex_def by fast lemma gallery_in_subcomplex: "⟦ ChamberSubcomplex Y; set ys ⊆ Y; gallery ys ⟧ ⟹ ChamberComplex.gallery Y ys" using chambersub_imp_sub maxsimpchain_in_subcomplex by simp lemma subcomplex_gallery: "ChamberSubcomplex Y ⟹ ChamberComplex.gallery Y Cs ⟹ gallery Cs" using ChamberSubcomplex_def gallery_def ChamberComplex.gallery_def by fastforce lemma subcomplex_pgallery: "ChamberSubcomplex Y ⟹ ChamberComplex.pgallery Y Cs ⟹ pgallery Cs" using ChamberSubcomplex_def pgallery_def ChamberComplex.pgallery_def by fastforce lemma min_gallery_in_subcomplex: assumes "ChamberSubcomplex Y" "min_gallery Cs" "set Cs ⊆ Y" shows "ChamberComplex.min_gallery Y Cs" proof (cases Cs rule: list_cases_Cons_snoc) case Nil with assms(1) show ?thesis using ChamberSubcomplexD_complex ChamberComplex.min_gallery_simps(1) by fast next case Single with assms show ?thesis using min_galleryD_gallery galleryD_chamber chamber_in_subcomplex ChamberComplex.min_gallery_simps(2) ChamberSubcomplexD_complex by force next case (Cons_snoc C Ds D) with assms show ?thesis using ChamberSubcomplexD_complex min_gallery_pgallery pgalleryD_distinct[of "C#Ds@[D]"] pgallery gallery_in_subcomplex[of Y] subcomplex_gallery min_galleryD_min_betw ChamberComplex.min_galleryI_betw[of Y] by force qed lemma chamber_card: "chamber C ⟹ chamber D ⟹ card C = card D" using maxsimp_connect[of C D] galleryD_adj adjacentchain_card by (cases "C=D") auto lemma chamber_facet_is_chamber_facet: "⟦ chamber C; chamber D; z⊲C; z⊆D ⟧ ⟹ z⊲D" using finite_chamber finite_facetrel_card chamber_card[of C] by (fastforce intro: facetrelI_cardSuc) lemma chamber_adj: assumes "chamber C" "D∈X" "C ∼ D" shows "chamber D" proof- from assms(2) obtain B where B: "chamber B" "D⊆B" using simplex_in_max by fast with assms(1,3) show ?thesis using chamber_card[of B] adjacent_card finite_chamber card_subset_eq[of B D] by force qed lemma : assumes "chamber C" "chamber (insert v z)" "z⊲C" shows "z⊲insert v z" proof (rule facetrelI) from assms show "v∉z" using finite_chamber[of C] finite_chamber[of "insert v z"] card_insert_if[of z v] by (auto simp add: finite_facetrel_card chamber_card) qed simp lemma adjacentset_chamber: "chamber C ⟹ D∈adjacentset C ⟹ chamber D" using adjacentset_def chamber_adj by fast lemma : "⟦ chamber C; z⊲C; D∈X; z⊲D ⟧ ⟹ chamber D" by (fast intro: chamber_adj adjacentI) lemma adjacentset_conv_facetchambersets: assumes "X ≠ {{}}" "chamber C" shows "adjacentset C = (⋃v∈C. {D∈X. C-{v}⊲D})" proof (rule seteqI) fix D assume D: "D ∈ adjacentset C" show "D ∈ (⋃v∈C. {D∈X. C-{v}⊲D})" proof (cases "D=C") case True with assms have "C ≠ {}" and "C ∈ X" using chamber_nempty chamberD_simplex by auto with True assms show ?thesis using facetrel_diff_vertex by fastforce next case False from D have D': "C∼D" using adjacentsetD_adj by fast with False obtain v where v: "v∉D" "C = insert v (C∩D)" using adjacent_int_decomp by fast hence "C-{v} = C∩D" by auto with D' False have "C-{v} ⊲ D" using adjacent_int_facet2 by auto with assms(2) D v(2) show ?thesis using adjacentset_def by fast qed next from assms(2) show "⋀D. D ∈ (⋃v∈C. {E∈X. C-{v}⊲E}) ⟹ D ∈ adjacentset C" using facetrel_diff_vertex adjacentI unfolding adjacentset_def by fastforce qed end (* context ChamberComplex *) subsection ‹The system of chambers and distance between chambers› text ‹ We now examine the system of all chambers in more detail, and explore the distance function on this system provided by lengths of minimal galleries. › context ChamberComplex begin definition chamber_system :: "'a set set" where "chamber_system ≡ {C. chamber C}" abbreviation "𝒞 ≡ chamber_system" definition chamber_distance :: "'a set ⇒ 'a set ⇒ nat" where "chamber_distance C D = (if C=D then 0 else Suc (length (ARG_MIN length Cs. gallery (C#Cs@[D]))))" definition closest_supchamber :: "'a set ⇒ 'a set ⇒ 'a set" where "closest_supchamber F D = (ARG_MIN (λC. chamber_distance C D) C. chamber C ∧ F⊆C)" definition "face_distance F D ≡ chamber_distance (closest_supchamber F D) D" lemma chamber_system_simplices: "𝒞 ⊆ X" using chamberD_simplex unfolding chamber_system_def by fast lemma gallery_chamber_system: "gallery Cs ⟹ set Cs ⊆ 𝒞" using galleryD_chamber chamber_system_def by fast lemmas pgallery_chamber_system = gallery_chamber_system[OF pgallery] lemma chamber_distance_le: "gallery (C#Cs@[D]) ⟹ chamber_distance C D ≤ Suc (length Cs)" using chamber_distance_def arg_min_nat_le[of "λCs. gallery (C#Cs@[D])" _ length] by auto lemma min_gallery_betw_chamber_distance: "min_gallery (C#Cs@[D]) ⟹ chamber_distance C D = Suc (length Cs)" using chamber_distance_def[of C D] is_arg_min_size[of length _ Cs] by auto lemma min_galleryI_chamber_distance_betw: "gallery (C#Cs@[D]) ⟹ Suc (length Cs) = chamber_distance C D ⟹ min_gallery (C#Cs@[D])" using chamber_distance_def chamber_distance_le min_galleryI_betw[of C D] by fastforce lemma gallery_least_length: assumes "chamber C" "chamber D" "C≠D" defines "Cs ≡ ARG_MIN length Cs. gallery (C#Cs@[D])" shows "gallery (C#Cs@[D])" using assms maxsimp_connect[of C D] arg_min_natI by fast lemma min_gallery_least_length: assumes "chamber C" "chamber D" "C≠D" defines "Cs ≡ ARG_MIN length Cs. gallery (C#Cs@[D])" shows "min_gallery (C#Cs@[D])" unfolding Cs_def using assms gallery_least_length by (blast intro: min_galleryI_betw arg_min_nat_le) lemma pgallery_least_length: assumes "chamber C" "chamber D" "C≠D" defines "Cs ≡ ARG_MIN length Cs. gallery (C#Cs@[D])" shows "pgallery (C#Cs@[D])" using assms min_gallery_least_length min_gallery_pgallery by fast lemma closest_supchamberD: assumes "F∈X" "chamber D" shows "chamber (closest_supchamber F D)" "F ⊆ closest_supchamber F D" using assms arg_min_natI[of "λC. chamber C ∧ F⊆C" ] simplex_in_max[of F] unfolding closest_supchamber_def by auto lemma closest_supchamber_closest: "chamber C ⟹ F⊆C ⟹ chamber_distance (closest_supchamber F D) D ≤ chamber_distance C D" using arg_min_nat_le[of "λC. chamber C ∧ F⊆C" C] closest_supchamber_def by simp lemma face_distance_le: "chamber C ⟹ F⊆C ⟹ face_distance F D ≤ chamber_distance C D" unfolding face_distance_def closest_supchamber_def by (auto intro: arg_min_nat_le) lemma face_distance_eq_0: "chamber C ⟹ F⊆C ⟹ face_distance F C = 0" using chamber_distance_def closest_supchamber_def face_distance_def arg_min_equality[ of "λC. chamber C ∧ F⊆C" C "λD. chamber_distance D C" ] by simp end (* context ChamberComplex *) subsection ‹Labelling a chamber complex› text ‹ A labelling of a chamber complex is a function on the vertex set so that each chamber is in bijective correspondence with the label set (chambers all have the same number of vertices). › context ChamberComplex begin definition label_wrt :: "'b set ⇒ ('a⇒'b) ⇒ bool" where "label_wrt B f ≡ (∀C∈𝒞. bij_betw f C B)" lemma label_wrtD: "label_wrt B f ⟹ C∈𝒞 ⟹ bij_betw f C B" using label_wrt_def by fast lemma label_wrtD': "label_wrt B f ⟹ chamber C ⟹ bij_betw f C B" using label_wrt_def chamber_system_def by fast lemma label_wrt_adjacent: assumes "label_wrt B f" "chamber C" "chamber D" "C∼D" "v∈C-D" "w∈D-C" shows "f v = f w" proof- from assms(5) have "f`D = insert (f v) (f`(C∩D))" using adjacent_conv_insert[OF assms(4), of v] label_wrtD'[OF assms(1,2)] label_wrtD'[OF assms(1,3)] bij_betw_imp_surj_on[of f] by force with assms(6) show ?thesis using adjacent_sym[OF assms(4)] adjacent_conv_insert[of D C] inj_on_insert[of f w "C∩D"] bij_betw_imp_inj_on[OF label_wrtD', OF assms(1,3)] by (force simp add: Int_commute) qed lemma : "⟦ label_wrt B f; chamber (insert v z); chamber (insert w z); v∉z; w∉z ⟧ ⟹ f v = f w" by (auto intro: label_wrt_adjacent adjacentI facetrelI) lemma label_wrt_elt_image: "label_wrt B f ⟹ v∈⋃X ⟹ f v ∈ B" using simplex_in_max label_wrtD' bij_betw_imp_surj_on by fast end (* context ChamberComplex *) subsection ‹Morphisms of chamber complexes› text ‹ While any function on the vertex set of a simplicial complex can be considered a morphism of simplicial complexes onto its image, for chamber complexes we require the function send chambers onto chambers of the same cardinality in some chamber complex of the codomain. › subsubsection ‹Morphism locale and basic facts› locale ChamberComplexMorphism = domain: ChamberComplex X + codomain: ChamberComplex Y for X :: "'a set set" and Y :: "'b set set" + fixes f :: "'a⇒'b" assumes chamber_map: "domain.chamber C ⟹ codomain.chamber (f`C)" and dim_map : "domain.chamber C ⟹ card (f`C) = card C" lemma (in ChamberComplex) trivial_morphism: "ChamberComplexMorphism X X id" by unfold_locales auto lemma (in ChamberComplex) inclusion_morphism: assumes "ChamberSubcomplex Y" shows "ChamberComplexMorphism Y X id" by ( rule ChamberComplexMorphism.intro, rule ChamberSubcomplexD_complex, rule assms, unfold_locales ) (auto simp add: subcomplex_chamber[OF assms]) context ChamberComplexMorphism begin lemmas domain_complex = domain.ChamberComplex_axioms lemmas codomain_complex = codomain.ChamberComplex_axioms lemmas simplicialcomplex_image = domain.map_is_simplicial_morph[of f] lemma cong: "fun_eq_on g f (⋃X) ⟹ ChamberComplexMorphism X Y g" using chamber_map domain.chamber_vertices fun_eq_on_im[of g f] dim_map domain.chamber_vertices by unfold_locales auto lemma comp: assumes "ChamberComplexMorphism Y Z g" shows "ChamberComplexMorphism X Z (g∘f)" proof ( rule ChamberComplexMorphism.intro, rule domain_complex, rule ChamberComplexMorphism.axioms(2), rule assms, unfold_locales ) fix C assume C: "domain.chamber C" from C show "SimplicialComplex.maxsimp Z ((g∘f)`C)" using chamber_map ChamberComplexMorphism.chamber_map[OF assms] by (force simp add: image_comp[THEN sym]) from C show "card ((g ∘ f)`C) = card C" using chamber_map dim_map ChamberComplexMorphism.dim_map[OF assms] by (force simp add: image_comp[THEN sym]) qed lemma restrict_domain: assumes "domain.ChamberSubcomplex W" shows "ChamberComplexMorphism W Y f" proof ( rule ChamberComplexMorphism.intro, rule domain.ChamberSubcomplexD_complex, rule assms, rule codomain_complex, unfold_locales ) fix C assume "ChamberComplex.chamber W C" with assms show "codomain.chamber (f`C)" "card (f`C) = card C" using domain.subcomplex_chamber chamber_map dim_map by auto qed lemma restrict_codomain: assumes "codomain.ChamberSubcomplex Z" "f⊢X ⊆ Z" shows "ChamberComplexMorphism X Z f" proof ( rule ChamberComplexMorphism.intro, rule domain_complex, rule codomain.ChamberSubcomplexD_complex, rule assms, unfold_locales ) fix C assume "domain.chamber C" with assms show "SimplicialComplex.maxsimp Z (f`C)" "card (f ` C) = card C" using domain.chamberD_simplex[of C] chamber_map codomain.chamber_in_subcomplex dim_map by auto qed lemma inj_on_chamber: "domain.chamber C ⟹ inj_on f C" using domain.finite_chamber dim_map by (fast intro: eq_card_imp_inj_on) lemma bij_betw_chambers: "domain.chamber C ⟹ bij_betw f C (f`C)" using inj_on_chamber by (fast intro: bij_betw_imageI) lemma card_map: "x∈X ⟹ card (f`x) = card x" using domain.simplex_in_max subset_inj_on[OF inj_on_chamber] domain.finite_simplex inj_on_iff_eq_card by blast lemma codim_map: assumes "domain.chamber C" "y ⊆ C" shows "card (f`C - f`y) = card (C-y)" using assms dim_map domain.chamberD_simplex domain.faces[of C y] domain.finite_simplex card_Diff_subset[of "f`y" "f`C"] card_map card_Diff_subset[of y C] by auto lemma simplex_map: "x∈X ⟹ f`x∈Y" using chamber_map domain.simplex_in_max codomain.chamberD_simplex codomain.faces[of _ "f`x"] by force lemma simplices_map: "f⊢X ⊆ Y" using simplex_map by fast lemma vertex_map: "x ∈ ⋃X ⟹ f x ∈ ⋃Y" using simplex_map by fast lemma facet_map: "domain.chamber C ⟹ z⊲C ⟹ f`z ⊲ f`C" using facetrel_subset facetrel_card codim_map[of C z] by (fastforce intro: facetrelI_card) lemma adj_int_im: assumes "domain.chamber C" "domain.chamber D" "C ∼ D" "f`C ≠ f`D" shows "(f`C ∩ f`D) ⊲ f`C" proof (rule facetrelI_card) from assms(1,2) chamber_map have 1: "f`C ⊆ f`D ⟹ f`C = f`D" using codomain.chamberD_simplex codomain.chamberD_maximal[of "f`C" "f`D"] by simp thus "f ` C ∩ f ` D ⊆ f ` C" by fast from assms(1) have "card (f`C - f`C ∩ f`D) ≤ card (f`C - f`(C∩D))" using domain.finite_chamber card_mono[of "f`C - f`(C∩D)" "f`C - f`C ∩ f`D"] by fast moreover from assms(1,3,4) have "card (f`C - f`(C∩D)) = 1" using codim_map[of C "C∩D"] adjacent_int_facet1 facetrel_card by fastforce ultimately have "card (f`C - f`C ∩ f`D) ≤ 1" by simp moreover from 1 assms(1,4) have "card (f`C - f`C ∩ f`D) ≠ 0" using domain.finite_chamber by auto ultimately show "card (f`C - f`C ∩ f`D) = 1" by simp qed lemma adj_map': assumes "domain.chamber C" "domain.chamber D" "C ∼ D" "f`C ≠ f`D" shows "f`C ∼ f`D" using assms(3,4) adj_int_im[OF assms] adjacent_sym adj_int_im[OF assms(2) assms(1)] by (auto simp add: Int_commute intro: adjacentI) lemma adj_map: "⟦ domain.chamber C; domain.chamber D; C ∼ D ⟧ ⟹ f`C ∼ f`D" using adjacent_refl[of "f`C"] adj_map' empty_not_adjacent[of D] by fastforce lemma chamber_vertex_outside_facet_image: assumes "v∉z" "domain.chamber (insert v z)" shows "f v ∉ f`z" proof- from assms(1) have "insert v z - z = {v}" by force with assms(2) show ?thesis using codim_map by fastforce qed lemma expand_codomain: assumes "ChamberComplex Z" "ChamberComplex.ChamberSubcomplex Z Y" shows "ChamberComplexMorphism X Z f" proof ( rule ChamberComplexMorphism.intro, rule domain_complex, rule assms(1), unfold_locales ) from assms show "⋀x. domain.chamber x ⟹ SimplicialComplex.maxsimp Z (f ` x)" using chamber_map ChamberComplex.subcomplex_chamber by fast qed (auto simp add: dim_map) end (* context ChamberComplexMorphism *) subsubsection ‹Action on pregalleries and galleries› context ChamberComplexMorphism begin lemma gallery_map: "domain.gallery Cs ⟹ codomain.gallery (f⊨Cs)" proof (induct Cs rule: list_induct_CCons) case (Single C) thus ?case using domain.galleryD_chamber chamber_map codomain.gallery_def by auto next case (CCons B C Cs) have "codomain.gallery (f`B # f`C # f⊨Cs)" proof (rule codomain.gallery_CConsI) from CCons(2) show "codomain.chamber (f ` B)" using domain.galleryD_chamber chamber_map by simp from CCons show "codomain.gallery (f`C # f⊨Cs)" using domain.gallery_Cons_reduce by auto from CCons(2) show "f`B ∼ f`C" using domain.gallery_Cons_reduce[of B "C#Cs"] domain.galleryD_adj domain.galleryD_chamber adj_map by fastforce qed thus ?case by simp qed (simp add: codomain.maxsimpchain_def) lemma gallery_betw_map: "domain.gallery (C#Cs@[D]) ⟹ codomain.gallery (f`C # f⊨Cs @ [f`D])" using gallery_map by fastforce end (* context ChamberComplexMorphism *) subsubsection ‹Properties of the image› context ChamberComplexMorphism begin lemma subcomplex_image: "codomain.Subcomplex (f⊢X)" using simplicialcomplex_image simplex_map by fast lemmas chamber_in_image = codomain.max_in_subcomplex[OF subcomplex_image] lemma maxsimp_map_into_image: assumes "domain.chamber x" shows "SimplicialComplex.maxsimp (f⊢X) (f`x)" proof ( rule SimplicialComplex.maxsimpI, rule simplicialcomplex_image, rule imageI, rule domain.chamberD_simplex, rule assms ) from assms show "⋀z. z∈f⊢X ⟹ f`x ⊆ z ⟹ z = f`x" using chamber_map[of x] simplex_map codomain.chamberD_maximal[of "f`x"] by blast qed lemma maxsimp_preimage: assumes "C∈X" "SimplicialComplex.maxsimp (f⊢X) (f`C)" shows "domain.chamber C" proof- from assms(1) obtain D where D: "domain.chamber D" "C⊆D" using domain.simplex_in_max by fast have "C=D" proof (rule card_subset_eq) from D(1) show "finite D" using domain.finite_chamber by fast with assms D show "card C = card D" using domain.chamberD_simplex simplicialcomplex_image SimplicialComplex.maxsimpD_maximal[of "f⊢X" "f`C" "f`D"] card_mono[of D C] domain.finite_simplex card_image_le[of C f] dim_map by force qed (rule D(2)) with D(1) show ?thesis by fast qed lemma chamber_preimage: "C∈X ⟹ codomain.chamber (f`C) ⟹ domain.chamber C" using chamber_in_image maxsimp_preimage by simp lemma chambercomplex_image: "ChamberComplex (f⊢X)" proof (intro_locales, rule simplicialcomplex_image, unfold_locales) show "⋀y. y∈f⊢X ⟹ ∃x. SimplicialComplex.maxsimp (f⊢X) x ∧ y ⊆ x" using domain.simplex_in_max maxsimp_map_into_image by fast next fix x y assume xy: "x≠y" "SimplicialComplex.maxsimp (f⊢X) x" "SimplicialComplex.maxsimp (f⊢X) y" from xy(2,3) obtain zx zy where zxy: "zx∈X" "x = f`zx" "zy∈X" "y = f`zy " using SimplicialComplex.maxsimpD_simplex[OF simplicialcomplex_image, of x] SimplicialComplex.maxsimpD_simplex[OF simplicialcomplex_image, of y] by fast with xy obtain ws where ws: "domain.gallery (zx#ws@[zy])" using maxsimp_preimage domain.maxsimp_connect[of zx zy] by auto with ws zxy(2,4) have "SimplicialComplex.maxsimpchain (f⊢X) (x#(f⊨ws)@[y])" using gallery_map[of "zx#ws@[zy]"] domain.galleryD_chamber domain.chamberD_simplex codomain.galleryD_chamber codomain.max_in_subcomplex[OF subcomplex_image] codomain.galleryD_adj SimplicialComplex.maxsimpchain_def[OF simplicialcomplex_image] by auto thus "∃xs. SimplicialComplex.maxsimpchain (f⊢X) (x#xs@[y])" by fast qed lemma chambersubcomplex_image: "codomain.ChamberSubcomplex (f⊢X)" using simplices_map chambercomplex_image ChamberComplex.chamberD_simplex chambercomplex_image maxsimp_preimage chamber_map by (force intro: codomain.ChamberSubcomplexI) lemma restrict_codomain_to_image: "ChamberComplexMorphism X (f⊢X) f" using restrict_codomain chambersubcomplex_image by fast end (* context ChamberComplexMorphism *) subsubsection ‹Action on the chamber system› context ChamberComplexMorphism begin lemma chamber_system_into: "f⊢domain.𝒞 ⊆ codomain.𝒞" using chamber_map domain.chamber_system_def codomain.chamber_system_def by auto lemma chamber_system_image: "f⊢domain.𝒞 = codomain.𝒞 ∩ (f⊢X)" proof show "f⊢domain.𝒞 ⊆ codomain.𝒞 ∩ (f⊢X)" using chamber_system_into domain.chamber_system_simplices by fast show "f⊢domain.𝒞 ⊇ codomain.𝒞 ∩ (f⊢X)" proof fix D assume "D ∈ codomain.𝒞 ∩ (f⊢X)" hence "∃C. domain.chamber C ∧ f`C = D" using codomain.chamber_system_def chamber_preimage by fast thus "D ∈ f⊢domain.𝒞" using domain.chamber_system_def by auto qed qed lemma image_chamber_system: "ChamberComplex.𝒞 (f⊢X) = f ⊢ domain.𝒞" using ChamberComplex.chamber_system_def codomain.subcomplex_chamber ChamberComplex.chamberD_simplex chambercomplex_image chambersubcomplex_image chamber_system_image codomain.chamber_in_subcomplex codomain.chamber_system_def by auto lemma image_chamber_system_image: "ChamberComplex.𝒞 (f⊢X) = codomain.𝒞 ∩ (f⊢X)" using image_chamber_system chamber_system_image by simp lemma face_distance_eq_chamber_distance_map: assumes "domain.chamber C" "domain.chamber D" "C≠D" "z⊆C" "codomain.face_distance (f`z) (f`D) = domain.face_distance z D" "domain.face_distance z D = domain.chamber_distance C D" shows "codomain.face_distance (f`z) (f`D) = codomain.chamber_distance (f`C) (f`D)" using assms codomain.face_distance_le[of "f`C" "f`z" "f`D"] chamber_map codomain.chamber_distance_le gallery_betw_map[OF domain.gallery_least_length, of C D] domain.chamber_distance_def by force lemma face_distance_eq_chamber_distance_min_gallery_betw_map: assumes "domain.chamber C" "domain.chamber D" "C≠D" "z⊆C" "codomain.face_distance (f`z) (f`D) = domain.face_distance z D" "domain.face_distance z D = domain.chamber_distance C D" "domain.min_gallery (C#Cs@[D])" shows "codomain.min_gallery (f⊨(C#Cs@[D]))" using assms face_distance_eq_chamber_distance_map[of C D z] gallery_map[OF domain.min_galleryD_gallery, OF assms(7)] domain.min_gallery_betw_chamber_distance[OF assms(7)] codomain.min_galleryI_chamber_distance_betw[of "f`C" "f⊨Cs" "f`D"] by auto end (* context ChamberComplexMorphism *) subsubsection ‹Isomorphisms› locale ChamberComplexIsomorphism = ChamberComplexMorphism X Y f for X :: "'a set set" and Y :: "'b set set" and f :: "'a⇒'b" + assumes bij_betw_vertices: "bij_betw f (⋃X) (⋃Y)" and surj_simplex_map : "f⊢X = Y" lemma (in ChamberComplexIsomorphism) inj: "inj_on f (⋃X)" using bij_betw_vertices bij_betw_def by fast sublocale ChamberComplexIsomorphism < SimplicialComplexIsomorphism using inj by (unfold_locales) fast lemma (in ChamberComplex) trivial_isomorphism: "ChamberComplexIsomorphism X X id" using trivial_morphism bij_betw_id by unfold_locales (auto intro: ChamberComplexIsomorphism.intro) lemma (in ChamberComplexMorphism) isoI_inverse: assumes "ChamberComplexMorphism Y X g" "fixespointwise (g∘f) (⋃X)" "fixespointwise (f∘g) (⋃Y)" shows "ChamberComplexIsomorphism X Y f" proof (rule ChamberComplexIsomorphism.intro) show "ChamberComplexMorphism X Y f" .. show "ChamberComplexIsomorphism_axioms X Y f" proof from assms show "bij_betw f (⋃X) (⋃Y)" using vertex_map ChamberComplexMorphism.vertex_map comps_fixpointwise_imp_bij_betw[of f "⋃X" "⋃Y" g] by fast show "f⊢X = Y" proof (rule order.antisym, rule simplices_map, rule subsetI) fix y assume "y∈Y" moreover hence "(f∘g) ` y ∈ f⊢X" using ChamberComplexMorphism.simplex_map[OF assms(1)] by (simp add: image_comp[THEN sym]) ultimately show "y ∈ f⊢X" using fixespointwise_subset[OF assms(3), of y] fixespointwise_im by fastforce qed qed qed context ChamberComplexIsomorphism begin lemmas domain_complex = domain_complex lemmas chamber_map = chamber_map lemmas dim_map = dim_map lemmas gallery_map = gallery_map lemmas simplex_map = simplex_map lemmas chamber_preimage = chamber_preimage lemma chamber_morphism: "ChamberComplexMorphism X Y f" .. lemma pgallery_map: "domain.pgallery Cs ⟹ codomain.pgallery (f⊨Cs)" using pmaxsimpchain_map surj_simplex_map by simp lemma iso_cong: assumes "fun_eq_on g f (⋃X)" shows "ChamberComplexIsomorphism X Y g" proof ( rule ChamberComplexIsomorphism.intro, rule cong, rule assms, unfold_locales ) from assms show "bij_betw g (⋃X) (⋃Y)" using bij_betw_vertices fun_eq_on_bij_betw by blast show "g ⊢ X = Y" using setsetmapim_cong[OF assms] surj_simplex_map by simp qed lemma iso_comp: assumes "ChamberComplexIsomorphism Y Z g" shows "ChamberComplexIsomorphism X Z (g∘f)" by ( rule ChamberComplexIsomorphism.intro, rule comp, rule ChamberComplexIsomorphism.axioms(1), rule assms, unfold_locales, rule bij_betw_trans, rule bij_betw_vertices, rule ChamberComplexIsomorphism.bij_betw_vertices, rule assms ) (simp add: setsetmapim_comp surj_simplex_map assms ChamberComplexIsomorphism.surj_simplex_map ) lemma inj_on_chamber_system: "inj_on ((`) f) domain.𝒞" proof (rule inj_onI) fix C D show "⟦ C ∈ domain.𝒞; D ∈ domain.𝒞; f`C = f`D ⟧ ⟹ C=D" using domain.chamber_system_def domain.chamber_pconnect[of C D] pgallery_map codomain.pgalleryD_distinct by fastforce qed lemma inv: "ChamberComplexIsomorphism Y X (the_inv_into (⋃X) f)" proof show "bij_betw (the_inv_into (⋃X) f) (⋃Y) (⋃X)" using bij_betw_vertices bij_betw_the_inv_into by fast show 4: "(the_inv_into (⋃X) f) ⊢ Y = X" using bij_betw_imp_inj_on[OF bij_betw_vertices] surj_simplex_map setsetmapim_the_inv_into by force next fix C assume C: "codomain.chamber C" hence C': "C∈f⊢X" using codomain.chamberD_simplex surj_simplex_map by fast show "domain.chamber (the_inv_into (⋃X) f ` C)" proof (rule domain.chamberI) from C' obtain D where "D∈X" "the_inv_into (⋃X) f ` C = D" using the_inv_into_f_im_f_im[OF inj] by blast thus "the_inv_into (⋃X) f ` C ∈ X" by simp fix z assume z: "z∈X" "the_inv_into (⋃X) f ` C ⊆ z" with C have "f`z = C" using C' f_im_the_inv_into_f_im[OF inj, of C] surj_simplex_map codomain.chamberD_maximal[of C "f`z"] by blast with z(1) show "z = the_inv_into (⋃X) f ` C" using the_inv_into_f_im_f_im[OF inj] by auto qed from C show "card (the_inv_into (⋃X) f ` C) = card C" using C' codomain.finite_chamber subset_inj_on[OF inj_on_the_inv_into, OF inj, of C] by (fast intro: inj_on_iff_eq_card[THEN iffD1]) qed lemma chamber_distance_map: assumes "domain.chamber C" "domain.chamber D" shows "codomain.chamber_distance (f`C) (f`D) = domain.chamber_distance C D" proof (cases "f`C=f`D") case True moreover with assms have "C=D" using inj_onD[OF inj_on_chamber_system] domain.chamber_system_def by simp ultimately show ?thesis using domain.chamber_distance_def codomain.chamber_distance_def by simp next case False define Cs Ds where "Cs = (ARG_MIN length Cs. domain.gallery (C#Cs@[D]))" and "Ds = (ARG_MIN length Ds. codomain.gallery (f`C # Ds @ [f`D]))" from assms False Cs_def have "codomain.gallery (f`C # f⊨Cs @ [f`D])" using gallery_map domain.maxsimp_connect[of C D] arg_min_natI[of "λCs. domain.gallery (C#Cs@[D])"] by fastforce moreover from assms Cs_def have "⋀Es. codomain.gallery (f`C # Es @ [f`D]) ⟹ length (f⊨Cs) ≤ length Es" using ChamberComplexIsomorphism.gallery_map[OF inv] the_inv_into_f_im_f_im[OF inj, of C] the_inv_into_f_im_f_im[OF inj, of D] domain.chamberD_simplex[of C] domain.chamberD_simplex[of D] domain.maxsimp_connect[of C D] arg_min_nat_le[of "λCs. domain.gallery (C#Cs@[D])" _ length] by force ultimately have "length Ds = length (f⊨Cs)" unfolding Ds_def by (fast intro: arg_min_equality) with False Cs_def Ds_def show ?thesis using domain.chamber_distance_def codomain.chamber_distance_def by auto qed lemma face_distance_map: assumes "domain.chamber C" "F∈X" shows "codomain.face_distance (f`F) (f`C) = domain.face_distance F C" proof- define D D' invf where "D = domain.closest_supchamber F C" and "D' = codomain.closest_supchamber (f`F) (f`C)" and "invf = the_inv_into (⋃X) f" from assms D_def D'_def invf_def have chambers: "codomain.chamber (f`C)" "domain.chamber D" "codomain.chamber D'" "codomain.chamber (f`D)" "domain.chamber (invf`D')" using domain.closest_supchamberD(1) simplex_map codomain.closest_supchamberD(1) chamber_map ChamberComplexIsomorphism.chamber_map[OF inv] by auto have "codomain.chamber_distance D' (f`C) ≤ domain.chamber_distance D C" proof- from assms D_def D'_def have "codomain.chamber_distance D' (f`C) ≤ codomain.chamber_distance (f`D) (f`C)" using chambers(4) domain.closest_supchamberD(2) codomain.closest_supchamber_def by (fastforce intro: arg_min_nat_le) with assms D_def D'_def show ?thesis using chambers(2) chamber_distance_map by simp qed moreover have "domain.chamber_distance D C ≤ codomain.chamber_distance D' (f`C)" proof- from assms D'_def have "invf`f`F ⊆ invf`D'" using chambers(1) simplex_map codomain.closest_supchamberD(2) by fast with assms(2) invf_def have "F ⊆ invf`D'" using the_inv_into_f_im_f_im[OF inj, of F] by fastforce with D_def have "domain.chamber_distance D C ≤ domain.chamber_distance (invf ` D') C" using chambers(5) domain.closest_supchamber_def by (auto intro: arg_min_nat_le) with assms(1) invf_def show ?thesis using chambers(3,5) surj_simplex_map codomain.chamberD_simplex f_im_the_inv_into_f_im[OF inj, of D'] chamber_distance_map[of "invf`D'" C] by fastforce qed ultimately show ?thesis using D_def D'_def domain.face_distance_def codomain.face_distance_def by simp qed end (* context ChamberComplexIsomorphism *) subsubsection ‹Endomorphisms› locale ChamberComplexEndomorphism = ChamberComplexMorphism X X f for X :: "'a set set" and f :: "'a⇒'a" + assumes trivial_outside : "v∉⋃X ⟹ f v = v" ― ‹to facilitate uniqueness arguments› lemma (in ChamberComplex) trivial_endomorphism: "ChamberComplexEndomorphism X id" by ( rule ChamberComplexEndomorphism.intro, rule trivial_morphism, unfold_locales ) simp context ChamberComplexEndomorphism begin abbreviation "ChamberSubcomplex ≡ domain.ChamberSubcomplex" abbreviation "Subcomplex ≡ domain.Subcomplex" abbreviation "chamber ≡ domain.chamber" abbreviation "gallery ≡ domain.gallery" abbreviation "𝒞 ≡ domain.chamber_system" abbreviation "label_wrt ≡ domain.label_wrt" lemmas dim_map = dim_map lemmas simplex_map = simplex_map lemmas vertex_map = vertex_map lemmas chamber_map = chamber_map lemmas adj_map = adj_map lemmas facet_map = facet_map lemmas bij_betw_chambers = bij_betw_chambers lemmas chamber_system_into = chamber_system_into lemmas chamber_system_image = chamber_system_image lemmas image_chamber_system = image_chamber_system lemmas chambercomplex_image = chambercomplex_image lemmas chambersubcomplex_image = chambersubcomplex_image lemmas face_distance_eq_chamber_distance_map = face_distance_eq_chamber_distance_map lemmas face_distance_eq_chamber_distance_min_gallery_betw_map = face_distance_eq_chamber_distance_min_gallery_betw_map lemmas facedist_chdist_mingal_btwmap = face_distance_eq_chamber_distance_min_gallery_betw_map lemmas trivial_endomorphism = domain.trivial_endomorphism lemmas finite_simplices = domain.finite_simplices lemmas faces = domain.faces lemmas maxsimp_connect = domain.maxsimp_connect lemmas simplex_in_max = domain.simplex_in_max lemmas chamberD_simplex = domain.chamberD_simplex lemmas chamber_system_def = domain.chamber_system_def lemmas chamber_system_simplices = domain.chamber_system_simplices lemmas galleryD_chamber = domain.galleryD_chamber lemmas galleryD_adj = domain.galleryD_adj lemmas gallery_append_reduce1 = domain.gallery_append_reduce1 lemmas gallery_Cons_reduce = domain.gallery_Cons_reduce lemmas gallery_chamber_system = domain.gallery_chamber_system lemmas label_wrtD = domain.label_wrtD lemmas label_wrt_adjacent = domain.label_wrt_adjacent lemma endo_comp: assumes "ChamberComplexEndomorphism X g" shows "ChamberComplexEndomorphism X (g∘f)" proof (rule ChamberComplexEndomorphism.intro) from assms show "ChamberComplexMorphism X X (g∘f)" using comp ChamberComplexEndomorphism.axioms by fast from assms show "ChamberComplexEndomorphism_axioms X (g∘f)" using trivial_outside ChamberComplexEndomorphism.trivial_outside by unfold_locales auto qed lemma restrict_endo: assumes "ChamberSubcomplex Y" "f⊢Y ⊆ Y" shows "ChamberComplexEndomorphism Y (restrict1 f (⋃Y))" proof (rule ChamberComplexEndomorphism.intro) from assms show "ChamberComplexMorphism Y Y (restrict1 f (⋃Y))" using ChamberComplexMorphism.cong[of Y Y] ChamberComplexMorphism.restrict_codomain restrict_domain fun_eq_on_restrict1 by fast show "ChamberComplexEndomorphism_axioms Y (restrict1 f (⋃Y))" by unfold_locales simp qed lemma funpower_endomorphism: "ChamberComplexEndomorphism X (f^^n)" proof (induct n) case 0 show ?case using trivial_endomorphism subst[of id] by fastforce next case (Suc m) hence "ChamberComplexEndomorphism X (f^^m ∘ f)" using endo_comp by auto moreover have "f^^m ∘ f = f^^(Suc m)" by (simp add: funpow_Suc_right[THEN sym]) ultimately show ?case using subst[of _ _ "λf. ChamberComplexEndomorphism X f"] by fast qed end (* context ChamberComplexEndomorphism *) lemma (in ChamberComplex) fold_chamber_complex_endomorph_list: "∀x∈set xs. ChamberComplexEndomorphism X (f x) ⟹ ChamberComplexEndomorphism X (fold f xs)" proof (induct xs) case Nil show ?case using trivial_endomorphism subst[of id] by fastforce next case (Cons x xs) hence "ChamberComplexEndomorphism X (fold f xs ∘ f x)" using ChamberComplexEndomorphism.endo_comp by auto moreover have "fold f xs ∘ f x = fold f (x#xs)" by simp ultimately show ?case using subst[of _ _ "λf. ChamberComplexEndomorphism X f"] by fast qed context ChamberComplexEndomorphism begin lemma split_gallery: "⟦ C∈f⊢𝒞; D∈𝒞-f⊢𝒞; gallery (C#Cs@[D]) ⟧ ⟹ ∃As A B Bs. A∈f⊢𝒞 ∧ B∈𝒞-f⊢𝒞 ∧ C#Cs@[D] = As@A#B#Bs" proof (induct Cs arbitrary: C) case Nil define As :: "'a set list" where "As = []" hence "C#[]@[D] = As@C#D#As" by simp with Nil(1,2) show ?case by auto next case (Cons E Es) show ?case proof (cases "E∈f⊢𝒞") case True from Cons(4) have "gallery (E#Es@[D])" using gallery_Cons_reduce by simp with True obtain As A B Bs where 1: "A∈f⊢𝒞" "B∈𝒞-f⊢𝒞" "E#Es@[D] = As@A#B#Bs" using Cons(1)[of E] Cons(3) by blast from 1(3) have "C#(E#Es)@[D] = (C#As)@A#B#Bs" by simp with 1(1,2) show ?thesis by blast next case False hence "E∈𝒞-f⊢𝒞" using gallery_chamber_system[OF Cons(4)] by simp moreover have "C#(E#Es)@[D] = []@C#E#(Es@[D])" by simp ultimately show ?thesis using Cons(2) by blast qed qed lemma respects_labels_adjacent: assumes "label_wrt B φ" "chamber C" "chamber D" "C∼D" "∀v∈C. φ (f v) = φ v" shows "∀v∈D. φ (f v) = φ v" proof (cases "C=D") case False have CD: "C≠D" by fact with assms(4) obtain w where w: "w∉D" "C = insert w (C∩D)" using adjacent_int_decomp by fast with assms(2) have fC: "f w ∉ f`(C∩D)" "f`C = insert (f w) (f`(C∩D))" using chamber_vertex_outside_facet_image[of w "C∩D"] by auto show ?thesis proof fix v assume v: "v∈D" show "φ (f v) = φ v" proof (cases "v∈C") case False with assms(3,4) v have fD: "f v ∉ f`(D∩C)" "f`D = insert (f v) (f`(D∩C))" using adjacent_sym[of C D] adjacent_conv_insert[of D C v] chamber_vertex_outside_facet_image[of v "D∩C"] by auto have "φ (f v) = φ (f w)" proof (cases "f`C=f`D") case True with fC fD have "f v = f w" by (auto simp add: Int_commute) thus ?thesis by simp next case False from assms(2-4) have "chamber (f`C)" "chamber (f`D)" and fCfD: "f`C∼f`D" using chamber_map adj_map by auto moreover from assms(4) fC fCfD False have "f w ∈ f`C - f`D" using adjacent_to_adjacent_int[of C D f] by auto ultimately show ?thesis using assms(4) fD fCfD False adjacent_sym adjacent_to_adjacent_int[of D C f] label_wrt_adjacent[OF assms(1), of "f`C" "f`D" "f w" "f v", THEN sym] by auto qed with False v w assms(5) show ?thesis using label_wrt_adjacent[OF assms(1-4), of w v, THEN sym] by fastforce qed (simp add: assms(5)) qed qed (simp add: assms(5)) lemma respects_labels_gallery: assumes "label_wrt B φ" "∀v∈C. φ (f v) = φ v" shows "gallery (C#Cs@[D]) ⟹ ∀v∈D. φ (f v) = φ v" proof (induct Cs arbitrary: D rule: rev_induct) case Nil with assms(2) show ?case using galleryD_chamber galleryD_adj respects_labels_adjacent[OF assms(1), of C D] by force next case (snoc E Es) with assms(2) show ?case using gallery_append_reduce1[of "C#Es@[E]"] galleryD_chamber galleryD_adj binrelchain_append_reduce2[of adjacent "C#Es" "[E,D]"] respects_labels_adjacent[OF assms(1), of E D] by force qed lemma respect_label_fix_chamber_imp_fun_eq_on: assumes label : "label_wrt B φ" and chamber: "chamber C" "f`C = g`C" and respect: "∀v∈C. φ (f v) = φ v" "∀v∈C. φ (g v) = φ v" shows "fun_eq_on f g C" proof (rule fun_eq_onI) fix v assume "v∈C" moreover with respect have "φ (f v) = φ (g v)" by simp ultimately show "f v = g v" using label chamber chamber_map chamber_system_def label_wrtD[of B φ "f`C"] bij_betw_imp_inj_on[of φ] inj_onD by fastforce qed lemmas respects_label_fixes_chamber_imp_fixespointwise = respect_label_fix_chamber_imp_fun_eq_on[of _ _ _ id, simplified] end (* context ChamberComplexEndomorphism *) subsubsection ‹Automorphisms› locale ChamberComplexAutomorphism = ChamberComplexIsomorphism X X f for X :: "'a set set" and f :: "'a⇒'a" + assumes trivial_outside : "v∉⋃X ⟹ f v = v" ― ‹to facilitate uniqueness arguments› sublocale ChamberComplexAutomorphism < ChamberComplexEndomorphism using trivial_outside by unfold_locales fast lemma (in ChamberComplex) trivial_automorphism: "ChamberComplexAutomorphism X id" using trivial_isomorphism by unfold_locales (auto intro: ChamberComplexAutomorphism.intro) context ChamberComplexAutomorphism begin lemmas facet_map = facet_map lemmas chamber_map = chamber_map lemmas chamber_morphism = chamber_morphism lemmas bij_betw_vertices = bij_betw_vertices lemmas surj_simplex_map = surj_simplex_map lemma bij: "bij f" proof (rule bijI) show "inj f" proof (rule injI) fix x y assume "f x = f y" thus "x = y" using bij_betw_imp_inj_on[OF bij_betw_vertices] inj_onD[of f "⋃X" x y] vertex_map trivial_outside by (cases "x∈⋃X" "y∈⋃X" rule: two_cases) auto qed show "surj f" unfolding surj_def proof fix y show "∃x. y = f x" using bij_betw_imp_surj_on[OF bij_betw_vertices] trivial_outside[THEN sym, of y] by (cases "y∈⋃X") auto qed qed lemma comp: assumes "ChamberComplexAutomorphism X g" shows "ChamberComplexAutomorphism X (g∘f)" proof ( rule ChamberComplexAutomorphism.intro, rule ChamberComplexIsomorphism.intro, rule ChamberComplexMorphism.comp ) from assms show "ChamberComplexMorphism X X g" using ChamberComplexAutomorphism.chamber_morphism by fast show "ChamberComplexIsomorphism_axioms X X (g ∘ f)" proof from assms show "bij_betw (g∘f) (⋃X) (⋃X)" using bij_betw_vertices ChamberComplexAutomorphism.bij_betw_vertices bij_betw_trans by fast from assms show "(g∘f) ⊢ X = X" using surj_simplex_map ChamberComplexAutomorphism.surj_simplex_map by (force simp add: setsetmapim_comp) qed show "ChamberComplexAutomorphism_axioms X (g ∘ f)" using trivial_outside ChamberComplexAutomorphism.trivial_outside[OF assms] by unfold_locales auto qed unfold_locales lemma equality: assumes "ChamberComplexAutomorphism X g" "fun_eq_on f g (⋃X)" shows "f = g" proof fix x show "f x = g x" using trivial_outside fun_eq_onD[OF assms(2)] ChamberComplexAutomorphism.trivial_outside[OF assms(1)] by force qed end (* context ChamberComplexAutomorphism *) subsubsection ‹Retractions› text ‹A retraction of a chamber complex is an endomorphism that is the identity on its image.› locale ChamberComplexRetraction = ChamberComplexEndomorphism X f for X :: "'a set set" and f :: "'a⇒'a" + assumes retraction: "v∈⋃X ⟹ f (f v) = f v" begin lemmas simplex_map = simplex_map lemmas chamber_map = chamber_map lemmas gallery_map = gallery_map lemma vertex_retraction: "v∈f`(⋃X) ⟹ f v = v" using retraction by fast lemma simplex_retraction1: "x∈f⊢X ⟹ fixespointwise f x" using retraction fixespointwiseI[of x f] by auto lemma simplex_retraction2: "x∈f⊢X ⟹ f`x = x" using retraction retraction[THEN sym] by blast lemma chamber_retraction1: "C∈f⊢𝒞 ⟹ fixespointwise f C" using chamber_system_simplices simplex_retraction1 by auto lemma chamber_retraction2: "C∈f⊢𝒞 ⟹ f`C = C" using chamber_system_simplices simplex_retraction2[of C] by auto lemma respects_labels: assumes "label_wrt B φ" "v∈(⋃X)" shows "φ (f v) = φ v" proof- from assms(2) obtain C where "chamber C" "v∈C" using simplex_in_max by fast thus ?thesis using chamber_retraction1[of C] chamber_system_def chamber_map maxsimp_connect[of "f`C" C] chamber_retraction1[of "f`C"] respects_labels_gallery[OF assms(1), THEN bspec, of "f`C" _ C v] by (force simp add: fixespointwiseD) qed end (* context ChamberComplexRetraction *) subsubsection ‹Foldings of chamber complexes› text ‹ A folding of a chamber complex is a retraction that literally folds the complex in half, in that each chamber in the image is the image of precisely two chambers: itself (since a folding is a retraction) and a unique chamber outside the image. › paragraph ‹Locale definition› text ‹ Here we define the locale and collect some lemmas inherited from the @{const ChamberComplexRetraction} locale. › locale ChamberComplexFolding = ChamberComplexRetraction X f for X :: "'a set set" and f :: "'a⇒'a" + assumes folding: "chamber C ⟹ C∈f⊢X ⟹ ∃!D. chamber D ∧ D∉f⊢X ∧ f`D = C" begin lemmas folding_ex = ex1_implies_ex[OF folding] lemmas chamber_system_into = chamber_system_into lemmas gallery_map = gallery_map lemmas chamber_retraction1 = chamber_retraction1 lemmas chamber_retraction2 = chamber_retraction2 end (* context ChamberComplexFolding *) paragraph ‹Decomposition into half chamber systems and half apartments› text ‹ Here we describe how a folding splits the chamber system of the complex into its image and the complement of its image. The chamber subcomplex consisting of all simplices contained in a chamber of a given half of the chamber system is called a half-apartment. › context ChamberComplexFolding begin definition opp_half_apartment :: "'a set set" where "opp_half_apartment ≡ {x∈X. ∃C∈𝒞-f⊢𝒞. x⊆C}" abbreviation "Y ≡ opp_half_apartment" lemma opp_half_apartment_subset_complex: "Y⊆X" using opp_half_apartment_def by fast lemma simplicialcomplex_opp_half_apartment: "SimplicialComplex Y" proof show "∀x∈Y. finite x" using opp_half_apartment_subset_complex finite_simplices by fast next fix x y assume "x∈Y" "y⊆x" thus "y∈Y" using opp_half_apartment_subset_complex faces[of x y] unfolding opp_half_apartment_def by auto qed lemma subcomplex_opp_half_apartment: "Subcomplex Y" using opp_half_apartment_subset_complex simplicialcomplex_opp_half_apartment by fast lemma opp_half_apartmentI: "⟦ x∈X; C∈𝒞-f⊢𝒞; x⊆C ⟧ ⟹ x∈Y" using opp_half_apartment_def by auto lemma opp_chambers_subset_opp_half_apartment: "𝒞-f⊢𝒞 ⊆ Y" proof fix C assume "C ∈ 𝒞-f⊢𝒞" thus "C ∈ Y" using chamber_system_simplices opp_half_apartmentI by auto qed lemma maxsimp_in_opp_half_apartment: assumes "SimplicialComplex.maxsimp Y C" shows "C ∈ 𝒞-f⊢𝒞" proof- from assms obtain D where D: "D∈𝒞-f⊢𝒞" "C⊆D" using SimplicialComplex.maxsimpD_simplex[ OF simplicialcomplex_opp_half_apartment, of C ] opp_half_apartment_def by auto with assms show ?thesis using opp_chambers_subset_opp_half_apartment SimplicialComplex.maxsimpD_maximal[ OF simplicialcomplex_opp_half_apartment ] by force qed lemma chamber_in_opp_half_apartment: "SimplicialComplex.maxsimp Y C ⟹ chamber C" using maxsimp_in_opp_half_apartment chamber_system_def by fast end (* context ChamberComplexFolding *) paragraph ‹Mapping between half chamber systems for foldings› text ‹ Since each chamber in the image of the folding is the image of a unique chamber in the complement of the image, we obtain well-defined functions from one half chamber system to the other. › context ChamberComplexFolding begin abbreviation "opp_chamber C ≡ THE D. D∈𝒞-f⊢𝒞 ∧ f`D = C" abbreviation "flop C ≡ if C ∈ f⊢𝒞 then opp_chamber C else f`C" lemma inj_on_opp_chambers': assumes "chamber C" "C∉f⊢X" "chamber D" "D∉f⊢X" "f`C = f`D" shows "C=D" proof- from assms(1) folding have ex1: "∃!B. chamber B ∧ B∉f⊢X ∧ f`B = f`C" using chamberD_simplex chamber_map by auto from assms show ?thesis using ex1_unique[OF ex1, of C D] by blast qed lemma inj_on_opp_chambers'': "⟦ C ∈ 𝒞-f⊢𝒞; D ∈ 𝒞-f⊢𝒞; f`C = f`D ⟧ ⟹ C=D" using chamber_system_def chamber_system_image inj_on_opp_chambers' by auto lemma inj_on_opp_chambers: "inj_on ((`) f) (𝒞-f⊢𝒞)" using inj_on_opp_chambers'' inj_onI[of "𝒞-f⊢𝒞" "(`) f"] by fast lemma opp_chambers_surj: "f⊢(𝒞-(f⊢𝒞)) = f⊢𝒞" proof (rule seteqI) fix D assume D: "D ∈ f⊢𝒞" from this obtain B where "chamber B" "B∉f⊢X" "f`B = D" using chamber_system_def chamber_map chamberD_simplex folding_ex[of D] by auto thus "D ∈ f⊢(𝒞 - f⊢𝒞)" using chamber_system_image chamber_system_def by auto qed fast lemma opp_chambers_bij: "bij_betw ((`) f) (𝒞-(f⊢𝒞)) (f⊢𝒞)" using inj_on_opp_chambers opp_chambers_surj bij_betw_def[of "(`) f"] by auto lemma folding': assumes "C∈f⊢𝒞" shows "∃!D∈𝒞-f⊢𝒞. f`D = C" proof (rule ex_ex1I) from assms show "∃D. D ∈ 𝒞-f⊢𝒞 ∧ f`D = C" using chamber_system_image chamber_system_def folding_ex[of C] by auto next fix B D assume "B ∈ 𝒞-f⊢𝒞 ∧ f`B = C" "D ∈ 𝒞-f⊢𝒞 ∧ f`D = C" with assms show "B=D" using chamber_system_def chamber_system_image chamber_map chamberD_simplex ex1_unique[OF folding, of C B D] by auto qed lemma opp_chambers_distinct_map: "set Cs ⊆ 𝒞-f⊢𝒞 ⟹ distinct Cs ⟹ distinct (f⊨Cs)" using distinct_map subset_inj_on[OF inj_on_opp_chambers] by auto lemma opp_chamberD1: "C∈f⊢𝒞 ⟹ opp_chamber C ∈ 𝒞-f⊢𝒞" using theI'[OF folding'] by simp lemma opp_chamberD2: "C∈f⊢𝒞 ⟹ f`(opp_chamber C) = C" using theI'[OF folding'] by simp lemma opp_chamber_reverse: "C∈𝒞-f⊢𝒞 ⟹ opp_chamber (f`C) = C" using the1_equality[OF folding'] by simp lemma f_opp_chamber_list: "set Cs ⊆ f⊢𝒞 ⟹ f⊨(map opp_chamber Cs) = Cs" using opp_chamberD2 by (induct Cs) auto lemma flop_chamber: "chamber C ⟹ chamber (flop C)" using chamber_map opp_chamberD1 chamber_system_def by auto end (* context ChamberComplexFolding *) subsection ‹Thin chamber complexes› text ‹ A thin chamber complex is one in which every facet is a facet in exactly two chambers. Slightly more generally, we first consider the case of a chamber complex in which every facet is a facet of at most two chambers. One of the main results obtained at this point is the so-called standard uniqueness argument, which essentially states that two morphisms on a thin chamber complex that agree on a particular chamber must in fact agree on the entire complex. Following that, foldings of thin chamber complexes are investigated. In particular, we are interested in pairs of opposed foldings. › subsubsection ‹Locales and basic facts› locale ThinishChamberComplex = ChamberComplex X for X :: "'a set set" + assumes thinish: "⟦ chamber C; z⊲C; ∃D∈X-{C}. z⊲D ⟧ ⟹ ∃!D∈X-{C}. z⊲D" ― ‹being adjacent to a chamber, such a @{term D} would also be a chamber (see lemma @{text "chamber_adj"})› begin lemma facet_unique_other_chamber: "⟦ chamber B; z⊲B; chamber C; z⊲C; chamber D; z⊲D; C≠B; D≠B ⟧ ⟹ C=D" using chamberD_simplex bex1_equality[OF thinish, OF _ _ bexI, of B z C C D] by auto lemma finite_adjacentset: assumes "chamber C" shows "finite (adjacentset C)" proof (cases "X = {{}}") case True thus ?thesis using adjacentset_def by simp next case False moreover have "finite (⋃v∈C. {D∈X. C-{v}⊲D})" proof from assms show "finite C" using finite_chamber by simp next fix v assume "v∈C" with assms have Cv: "C-{v}⊲C" using chamberD_simplex facetrel_diff_vertex by fast with assms have C: "C∈{D∈X. C-{v}⊲D}" using chamberD_simplex by fast show "finite {D∈X. C-{v}⊲D}" proof (cases "{D∈X. C-{v}⊲D} - {C} = {}") case True hence 1: "{D∈X. C-{v}⊲D} = {C}" using C by auto show ?thesis using ssubst[OF 1, of finite] by simp next case False from this obtain D where D: "D∈X-{C}" "C-{v}⊲D" by fast with assms have 2: "{D∈X. C-{v}⊲D} ⊆ {C,D}" using Cv chamber_shared_facet[of C] facet_unique_other_chamber[of C _ D] by fastforce show ?thesis using finite_subset[OF 2] by simp qed qed ultimately show ?thesis using assms adjacentset_conv_facetchambersets by simp qed lemma label_wrt_eq_on_adjacent_vertex: fixes v v' :: 'a and z z' :: "'a set" defines D : "D ≡ insert v z" and D': "D' ≡ insert v' z'" assumes label : "label_wrt B f" "f v = f v'" and chambers: "chamber C" "chamber D" "chamber D'" "z⊲C" "z'⊲C" "D≠C" "D'≠C" shows "D = D'" proof ( rule facet_unique_other_chamber, rule chambers(1), rule chambers(4), rule chambers(2) ) from D D' chambers(1-5) have z: "z⊲D" and z': "z'⊲D'" using chambers_share_facet by auto show "z⊲D" by fact from chambers(4,5) obtain w w' where w : "w ∉ z " "C = insert w z" and w': "w'∉ z'" "C = insert w' z'" unfolding facetrel_def by fastforce from w' D' chambers(1,3) have "f`z' = f`C - {f v'}" using z' label_wrtD'[OF label(1), of C] bij_betw_imp_inj_on[of f C] facetrel_complement_vertex[of z'] label_wrt_adjacent_shared_facet[OF label(1), of v'] by simp moreover from w D chambers(1,2) have "f`z = f`C - {f v}" using z label_wrtD'[OF label(1), of C] bij_betw_imp_inj_on[of f C] facetrel_complement_vertex[of z] label_wrt_adjacent_shared_facet[OF label(1), of v] by simp ultimately show "z⊲D'" using z' chambers(1,4,5) label(2) facetrel_subset label_wrtD'[OF label(1), of C] bij_betw_imp_inj_on[of f] inj_on_eq_image[of f C z' z] by force qed (rule chambers(3), rule chambers(6), rule chambers(7)) lemma face_distance_eq_chamber_distance_compare_other_chamber: assumes "chamber C" "chamber D" "z⊲C" "z⊲D" "C≠D" "chamber_distance C E ≤ chamber_distance D E" shows "face_distance z E = chamber_distance C E" unfolding face_distance_def closest_supchamber_def proof ( rule arg_min_equality, rule conjI, rule assms(1), rule facetrel_subset, rule assms(3) ) from assms show "⋀B. chamber B ∧ z ⊆ B ⟹ chamber_distance C E ≤ chamber_distance B E" using chamber_facet_is_chamber_facet facet_unique_other_chamber by blast qed end (* context ThinishChamberComplex *) lemma (in ChamberComplexIsomorphism) : assumes dom: "domain.chamber C" "domain.chamber D" "z⊲C" "z⊲D" "C≠D" and cod: "ThinishChamberComplex Y" "codomain.chamber D'" "f`z ⊲ D'" "D' ≠ f`C" shows "f`D = D'" proof (rule ThinishChamberComplex.facet_unique_other_chamber, rule cod(1)) from dom(1,2) show "codomain.chamber (f`C)" "codomain.chamber (f`D)" using chamber_map by auto from dom show "f`z ⊲ f`C" "f`z ⊲ f`D" using facet_map by auto from dom have "domain.pgallery [C,D]" using domain.pgallery_def adjacentI by fastforce hence "codomain.pgallery [f`C,f`D]" using pgallery_map[of "[C,D]"] by simp thus "f`D ≠ f`C" using codomain.pgalleryD_distinct by fastforce qed (rule cod(2), rule cod(3), rule cod(4)) locale ThinChamberComplex = ChamberComplex X for X :: "'a set set" + assumes thin: "chamber C ⟹ z⊲C ⟹ ∃!D∈X-{C}. z⊲D" sublocale ThinChamberComplex < ThinishChamberComplex using thin by unfold_locales simp context ThinChamberComplex begin lemma thinish: "ThinishChamberComplex X" .. lemmas face_distance_eq_chamber_distance_compare_other_chamber = face_distance_eq_chamber_distance_compare_other_chamber abbreviation "the_adj_chamber C z ≡ THE D. D∈X-{C} ∧ z ⊲ D" lemma the_adj_chamber_simplex: "chamber C ⟹ z ⊲ C ⟹ the_adj_chamber C z ∈ X" using theI'[OF thin] by fast lemma the_adj_chamber_facet: "chamber C ⟹ z⊲C ⟹ z ⊲ the_adj_chamber C z" using theI'[OF thin] by fast lemma the_adj_chamber_is_adjacent: "chamber C ⟹ z⊲C ⟹ C ∼ the_adj_chamber C z" using the_adj_chamber_facet by (auto intro: adjacentI) lemma the_adj_chamber: "chamber C ⟹ z ⊲ C ⟹ chamber (the_adj_chamber C z)" using the_adj_chamber_simplex the_adj_chamber_is_adjacent by (fast intro: chamber_adj) lemma the_adj_chamber_neq: "chamber C ⟹ z ⊲ C ⟹ the_adj_chamber C z ≠ C" using theI'[OF thin] by fast lemma the_adj_chamber_adjacentset: "chamber C ⟹ z⊲C ⟹ the_adj_chamber C z ∈ adjacentset C" using adjacentset_def the_adj_chamber_simplex the_adj_chamber_is_adjacent by fast end (* context ThinChamberComplex *) lemmas (in ChamberComplexIsomorphism) = thinish_image_shared_facet[OF _ _ _ _ _ ThinChamberComplex.thinish] subsubsection ‹The standard uniqueness argument for chamber morphisms of thin chamber complexes› context ThinishChamberComplex begin lemma standard_uniqueness_dbl: assumes morph : "ChamberComplexMorphism W X f" "ChamberComplexMorphism W X g" and chambers: "ChamberComplex.chamber W C" "ChamberComplex.chamber W D" "C∼D" "f`D ≠ f`C" "g`D ≠ g`C" "chamber (g`D)" and funeq : "fun_eq_on f g C" shows "fun_eq_on f g D" proof (rule fun_eq_onI) fix v assume v: "v∈D" show "f v = g v" proof (cases "v∈C") case True with funeq show ?thesis using fun_eq_onD by fast next case False define F G where "F = f`C ∩ f`D" and "G = g`C ∩ g`D" from morph(1) chambers(1-4) have 1: "f`C ∼ f`D" using ChamberComplexMorphism.adj_map' by fast with F_def chambers(4) have F_facet: "F⊲f`C" "F⊲f`D" using adjacent_int_facet1[of "f`C"] adjacent_int_facet2[of "f`C"] by auto from F_def G_def chambers have "G = F" using ChamberComplexMorphism.adj_map'[OF morph(2)] adjacent_to_adjacent_int[of C D g] 1 adjacent_to_adjacent_int[of C D f] funeq fun_eq_on_im[of f g] by force with G_def morph(2) chambers have F_facet': "F⊲g`D" using ChamberComplexMorphism.adj_map' adjacent_int_facet2 by blast with chambers(1,2,4,5) have 2: "g`D = f`D" using ChamberComplexMorphism.chamber_map[OF morph(1)] F_facet ChamberComplexMorphism.chamber_map[OF morph(2)] fun_eq_on_im[OF funeq] facet_unique_other_chamber[of "f`C" F "g`D" "f`D"] by auto from chambers(3) v False have 3: "D = insert v (D∩C)" using adjacent_sym adjacent_conv_insert by fast from chambers(4) obtain w where w: "w ∉ f`C" "w ∈ f`D" using adjacent_int_decomp[OF adjacent_sym, OF 1] by blast with 3 have "w = f v" by fast moreover from 2 w(2) obtain v' where "v'∈D" "w = g v'" by auto ultimately show ?thesis using w(1) 3 funeq by (fastforce simp add: fun_eq_on_im) qed qed lemma standard_uniqueness_pgallery_betw: assumes morph : "ChamberComplexMorphism W X f" "ChamberComplexMorphism W X g" and chambers: "fun_eq_on f g C" "ChamberComplex.gallery W (C#Cs@[D])" "pgallery (f⊨(C#Cs@[D]))" "pgallery (g⊨(C#Cs@[D]))" shows "fun_eq_on f g D" proof- from morph(1) have W: "ChamberComplex W" using ChamberComplexMorphism.domain_complex by fast have "⟦ fun_eq_on f g C; ChamberComplex.gallery W (C#Cs@[D]); pgallery (f⊨(C#Cs@[D])); pgallery (g⊨(C#Cs@[D])) ⟧ ⟹ fun_eq_on f g D" proof (induct Cs arbitrary: C) case Nil from assms Nil(1) show ?case using ChamberComplex.galleryD_chamber[OF W Nil(2)] ChamberComplex.galleryD_adj[OF W Nil(2)] pgalleryD_distinct[OF Nil(3)] pgalleryD_distinct[OF Nil(4)] pgalleryD_chamber[OF Nil(4)] standard_uniqueness_dbl[of W f g C D] by auto next case (Cons B Bs) have "fun_eq_on f g B" proof (rule standard_uniqueness_dbl, rule morph(1), rule morph(2)) show "ChamberComplex.chamber W C" "ChamberComplex.chamber W B" "C∼B" using ChamberComplex.galleryD_chamber[OF W Cons(3)] ChamberComplex.galleryD_adj[OF W Cons(3)] by auto show "f`B ≠ f`C" using pgalleryD_distinct[OF Cons(4)] by fastforce show "g`B ≠ g`C" using pgalleryD_distinct[OF Cons(5)] by fastforce show "chamber (g`B)" using pgalleryD_chamber[OF Cons(5)] by fastforce qed (rule Cons(2)) with Cons(1,3-5) show ?case using ChamberComplex.gallery_Cons_reduce[OF W, of C "B#Bs@[D]"] pgallery_Cons_reduce[of "f`C" "f⊨(B#Bs@[D])"] pgallery_Cons_reduce[of "g`C" "g⊨(B#Bs@[D])"] by force qed with chambers show ?thesis by simp qed lemma standard_uniqueness: assumes morph : "ChamberComplexMorphism W X f" "ChamberComplexMorphism W X g" and chamber : "ChamberComplex.chamber W C" "fun_eq_on f g C" and map_gals: "⋀Cs. ChamberComplex.min_gallery W (C#Cs) ⟹ pgallery (f⊨(C#Cs))" "⋀Cs. ChamberComplex.min_gallery W (C#Cs) ⟹ pgallery (g⊨(C#Cs))" shows "fun_eq_on f g (⋃W)" proof (rule fun_eq_onI) from morph(1) have W: "ChamberComplex W" using ChamberComplexMorphism.axioms(1) by fast fix v assume "v ∈ ⋃W" from this obtain D where "ChamberComplex.chamber W D" "v∈D" using ChamberComplex.simplex_in_max[OF W] by auto moreover define Cs where "Cs = (ARG_MIN length Cs. ChamberComplex.gallery W (C#Cs@[D]))" ultimately show "f v = g v" using chamber map_gals[of "Cs@[D]"] ChamberComplex.gallery_least_length[OF W] ChamberComplex.min_gallery_least_length[OF W] standard_uniqueness_pgallery_betw[OF morph(1,2) chamber(2), of Cs] fun_eq_onD[of f g D] by (cases "D=C") auto qed lemma standard_uniqueness_isomorphs: assumes "ChamberComplexIsomorphism W X f" "ChamberComplexIsomorphism W X g" "ChamberComplex.chamber W C" "fun_eq_on f g C" shows "fun_eq_on f g (⋃W)" using assms ChamberComplexIsomorphism.chamber_morphism ChamberComplexIsomorphism.domain_complex ChamberComplex.min_gallery_pgallery ChamberComplexIsomorphism.pgallery_map by (blast intro: standard_uniqueness) lemma standard_uniqueness_automorphs: assumes "ChamberComplexAutomorphism X f" "ChamberComplexAutomorphism X g" "chamber C" "fun_eq_on f g C" shows "f=g" using assms ChamberComplexAutomorphism.equality standard_uniqueness_isomorphs ChamberComplexAutomorphism.axioms(1) by blast end (* context ThinishChamberComplex *) context ThinChamberComplex begin lemmas standard_uniqueness = standard_uniqueness lemmas standard_uniqueness_isomorphs = standard_uniqueness_isomorphs lemmas standard_uniqueness_pgallery_betw = standard_uniqueness_pgallery_betw end (* context ThinChamberComplex *) subsection ‹Foldings of thin chamber complexes› subsubsection ‹Locale definition and basic facts› locale ThinishChamberComplexFolding = ThinishChamberComplex X + folding: ChamberComplexFolding X f for X :: "'a set set" and f :: "'a⇒'a" begin abbreviation "opp_chamber ≡ folding.opp_chamber" lemma adjacent_half_chamber_system_image: assumes chambers: "C ∈ f⊢𝒞" "D ∈ 𝒞-f⊢𝒞" and adjacent: "C∼D" shows "f`D = C" proof- from adjacent obtain z where z: "z⊲C" "z⊲D" using adjacent_def by fast moreover from z(1) chambers(1) have fz: "f`z = z" using facetrel_subset[of z C] chamber_system_simplices folding.simplicialcomplex_image SimplicialComplex.faces[of "f⊢X" C z] folding.simplex_retraction2[of z] by auto moreover from chambers have "f`D ≠ D" "C≠D" by auto ultimately show ?thesis using chambers chamber_system_def folding.chamber_map folding.facet_map[of D z] facet_unique_other_chamber[of D z "f`D" C] by force qed lemma adjacent_half_chamber_system_image_reverse: "⟦ C ∈ f⊢𝒞; D ∈ 𝒞-f⊢𝒞; C∼D ⟧ ⟹ opp_chamber C = D" using adjacent_half_chamber_system_image[of C D] the1_equality[OF folding.folding'] by fastforce lemma chamber_image_closer: assumes "D∈𝒞-f⊢𝒞" "B∈f⊢𝒞" "B≠f`D" "gallery (B#Ds@[D])" shows "∃Cs. gallery (B#Cs@[f`D]) ∧ length Cs < length Ds" proof- from assms(1,2,4) obtain As A E Es where split: "A∈f⊢𝒞" "E∈𝒞-f⊢𝒞" "B#Ds@[D] = As@A#E#Es" using folding.split_gallery[of B D Ds] by blast from assms(4) split(3) have "A∼E" using gallery_append_reduce2[of As "A#E#Es"] galleryD_adj[of "A#E#Es"] by simp with assms(2) split(1,2) have fB: "f`B = B" and fA: "f`A = A" and fE: "f`E = A" using folding.chamber_retraction2 adjacent_half_chamber_system_image[of A E] by auto show "∃Cs. gallery (B#Cs@[f`D]) ∧ length Cs < length Ds" proof (cases As) case Nil have As: "As = []" by fact show ?thesis proof (cases Es rule: rev_cases) case Nil with split(3) As assms(3) fE show ?thesis by simp next case (snoc Fs F) with assms(4) split(3) As fE have "Ds = E#Fs" "gallery (B # f⊨Fs @ [f`D])" using fB folding.gallery_map[of "B#E#Fs@[D]"] gallery_Cons_reduce by auto thus ?thesis by auto qed next case (Cons H Hs) show ?thesis proof (cases Es rule: rev_cases) case Nil with assms(4) Cons split(3) have decomp: "Ds = Hs@[A]" "D=E" "gallery (B#Hs@[A,D])" by auto from decomp(2,3) fB fA fE have "gallery (B # f⊨Hs @ [f`D])" using folding.gallery_map gallery_append_reduce1[of "B # f⊨Hs @ [f`D]"] by force with decomp(1) show ?thesis by auto next case (snoc Fs F) with split(3) Cons assms(4) fB fA fE have decomp: "Ds = Hs@A#E#Fs" "gallery (B # f⊨(Hs@A#Fs) @ [f`D])" using folding.gallery_map[of "B#Hs@A#E#Fs@[D]"] gallery_remdup_adj[of "B#f⊨Hs" A "f⊨Fs@[f`D]"] by auto from decomp(1) have "length (f⊨(Hs@A#Fs)) < length Ds" by simp with decomp(2) show ?thesis by blast qed qed qed lemma chamber_image_subset: assumes D: "D∈𝒞-f⊢𝒞" defines C: "C ≡ f`D" defines "closerToC ≡ {B∈𝒞. chamber_distance B C < chamber_distance B D}" shows "f⊢𝒞 ⊆ closerToC" proof fix B assume B: "B∈f⊢𝒞" hence B': "B∈𝒞" using folding.chamber_system_into by fast show "B ∈ closerToC" proof (cases "B=C") case True with B D closerToC_def show ?thesis using B' chamber_distance_def by auto next case False define Ds where "Ds = (ARG_MIN length Ds. gallery (B#Ds@[D]))" with B C D False closerToC_def show ?thesis using chamber_system_def folding.chamber_map gallery_least_length[of B D] chamber_image_closer[of D B Ds] chamber_distance_le chamber_distance_def[of B D] by fastforce qed qed lemma gallery_double_cross_not_minimal_Cons1: "⟦ B∈f⊢𝒞; C∈𝒞-f⊢𝒞; D∈f⊢𝒞; gallery (B#C#Cs@[D]) ⟧ ⟹ ¬ min_gallery (B#C#Cs@[D])" using galleryD_adj[of "B#C#Cs@[D]"] adjacent_half_chamber_system_image[of B C] folding.gallery_map[of "B#C#Cs@[D]"] gallery_Cons_reduce[of B "B # f⊨Cs @ [D]"] is_arg_minD2[of length "(λDs. maxsimpchain (B#Ds@[D]))" _ "f⊨Cs"] min_maxsimpchain.simps(3)[of B "C#Cs" D] by(simp add: folding.chamber_retraction2)(meson