section ‹Simplicial complexes› text ‹ In this section we develop the basic theory of abstract simplicial complexes as a collection of finite sets, where the power set of each member set is contained in the collection. Note that in this development we allow the empty simplex, since allowing it or not seemed of no logical consequence, but of some small practical consequence. › theory Simplicial imports Prelim begin subsection ‹Geometric notions› text ‹ The geometric notions attached to a simplicial complex of main interest to us are those of facets (subsets of codimension one), adjacency (sharing a facet in common), and chains of adjacent simplices. › subsubsection ‹Facets› definition facetrel :: "'a set ⇒ 'a set ⇒ bool" (infix "⊲" 60) where "y ⊲ x ≡ ∃v. v ∉ y ∧ x = insert v y" lemma facetrelI: "v ∉ y ⟹ x = insert v y ⟹ y ⊲ x" using facetrel_def by fast lemma facetrelI_card: "y ⊆ x ⟹ card (x-y) = 1 ⟹ y ⊲ x" using card1[of "x-y"] by (blast intro: facetrelI) lemma facetrel_complement_vertex: "y⊲x ⟹ x = insert v y ⟹ v∉y" using facetrel_def[of y x] by fastforce lemma facetrel_diff_vertex: "v∈x ⟹ x-{v} ⊲ x" by (auto intro: facetrelI) lemma facetrel_conv_insert: "y ⊲ x ⟹ v ∈ x - y ⟹ x = insert v y" unfolding facetrel_def by fast lemma facetrel_psubset: "y ⊲ x ⟹ y ⊂ x" unfolding facetrel_def by fast lemma facetrel_subset: "y ⊲ x ⟹ y ⊆ x" using facetrel_psubset by fast lemma facetrel_card: "y ⊲ x ⟹ card (x-y) = 1" using insert_Diff_if[of _ y y] unfolding facetrel_def by fastforce lemma finite_facetrel_card: "finite x ⟹ y⊲x ⟹ card x = Suc (card y)" using facetrel_def[of y x] card_insert_disjoint[of x] by auto lemma facetrelI_cardSuc: "z⊆x ⟹ card x = Suc (card z) ⟹ z⊲x" using card_ge_0_finite finite_subset[of z] card_Diff_subset[of z x] by (force intro: facetrelI_card) lemma facet2_subset: "⟦ z⊲x; z⊲y; x∩y - z ≠ {} ⟧ ⟹ x ⊆ y" unfolding facetrel_def by force lemma inj_on_pullback_facet: assumes "inj_on f x" "z ⊲ f`x" obtains y where "y ⊲ x" "f`y = z" proof from assms(2) obtain v where v: "v∉z" "f`x = insert v z" using facetrel_def[of z] by auto define u and y where "u ≡ the_inv_into x f v" and y: "y ≡ {v∈x. f v ∈ z}" moreover with assms(2) v have "x = insert u y" using the_inv_into_f_eq[OF assms(1)] the_inv_into_into[OF assms(1)] by fastforce ultimately show "y ⊲ x" using v f_the_inv_into_f[OF assms(1)] by (force intro: facetrelI) from y assms(2) show "f`y = z" using facetrel_subset by fast qed subsubsection ‹Adjacency› definition adjacent :: "'a set ⇒ 'a set ⇒ bool" (infix "∼" 70) where "x ∼ y ≡ ∃z. z⊲x ∧ z⊲y" lemma adjacentI: "z⊲x ⟹ z⊲y ⟹ x ∼ y" using adjacent_def by fast lemma empty_not_adjacent: "¬ {} ∼ x" unfolding facetrel_def adjacent_def by fast lemma adjacent_sym: "x ∼ y ⟹ y ∼ x" unfolding adjacent_def by fast lemma adjacent_refl: assumes "x ≠ {}" shows "x ∼ x" proof- from assms obtain v where v: "v∈x" by fast thus "x ∼ x" using facetrelI[of v "x-{v}"] unfolding adjacent_def by fast qed lemma common_facet: "⟦ z⊲x; z⊲y; x ≠ y ⟧ ⟹ z = x ∩ y" using facetrel_subset facet2_subset by fast lemma adjacent_int_facet1: "x ∼ y ⟹ x ≠ y ⟹ (x ∩ y) ⊲ x" using common_facet unfolding adjacent_def by fast lemma adjacent_int_facet2: "x ∼ y ⟹ x ≠ y ⟹ (x ∩ y) ⊲ y" using adjacent_sym adjacent_int_facet1 by (fastforce simp add: Int_commute) lemma adjacent_conv_insert: "x ∼ y ⟹ v ∈ x - y ⟹ x = insert v (x∩y)" using adjacent_int_facet1 facetrel_conv_insert by fast lemma adjacent_int_decomp: "x ∼ y ⟹ x ≠ y ⟹ ∃v. v ∉ y ∧ x = insert v (x∩y)" using adjacent_int_facet1 unfolding facetrel_def by fast lemma adj_antivertex: assumes "x∼y" "x≠y" shows "∃!v. v∈x-y" proof (rule ex_ex1I) from assms obtain w where w: "w∉y" "x = insert w (x∩y)" using adjacent_int_decomp by fast thus "∃v. v∈x-y" by auto from w have "⋀v. v∈x-y ⟹ v=w" by fast thus "⋀v v'. v∈x-y ⟹ v'∈x-y ⟹ v=v'" by auto qed lemma adjacent_card: "x ∼ y ⟹ card x = card y" unfolding adjacent_def facetrel_def by (cases "finite x" "x=y" rule: two_cases) auto lemma adjacent_to_adjacent_int_subset: assumes "C ∼ D" "f`C ∼ f`D" "f`C ≠ f`D" shows "f`C ∩ f`D ⊆ f`(C∩D)" proof from assms(1,3) obtain v where v: "v ∉ D" "C = insert v (C∩D)" using adjacent_int_decomp by fast from assms(2,3) obtain w where w: "w ∉ f`D" "f`C = insert w (f`C∩f`D)" using adjacent_int_decomp[of "f`C" "f`D"] by fast from w have w': "w ∈ f`C - f`D" by fast with v assms(1,2) have fv_w: "f v = w" using adjacent_conv_insert by fast fix b assume "b ∈ f`C ∩ f`D" from this obtain a1 a2 where a1: "a1 ∈ C" "b = f a1" and a2: "a2 ∈ D" "b = f a2" by fast from v a1 a2(2) have "a1 ∉ D ⟹ f a2 = w" using fv_w by auto with a2(1) w' have "a1 ∈ D" by fast with a1 show "b ∈ f`(C∩D)" by fast qed lemma adjacent_to_adjacent_int: "⟦ C ∼ D; f`C ∼ f`D; f`C ≠ f`D ⟧ ⟹ f`(C∩D) = f`C ∩ f`D" using adjacent_to_adjacent_int_subset by fast subsubsection ‹Chains of adjacent sets› abbreviation "adjacentchain ≡ binrelchain adjacent" abbreviation "padjacentchain ≡ proper_binrelchain adjacent" lemmas adjacentchain_Cons_reduce = binrelchain_Cons_reduce [of adjacent] lemmas adjacentchain_obtain_proper = binrelchain_obtain_proper [of _ _ adjacent] lemma adjacentchain_card: "adjacentchain (x#xs@[y]) ⟹ card x = card y" using adjacent_card by (induct xs arbitrary: x) auto subsection ‹Locale and basic facts› locale SimplicialComplex = fixes X :: "'a set set" assumes finite_simplices: "∀x∈X. finite x" and faces : "x∈X ⟹ y⊆x ⟹ y∈X" context SimplicialComplex begin abbreviation "Subcomplex Y ≡ Y ⊆ X ∧ SimplicialComplex Y" definition "maxsimp x ≡ x∈X ∧ (∀z∈X. x⊆z ⟶ z=x)" definition adjacentset :: "'a set ⇒ 'a set set" where "adjacentset x = {y∈X. x∼y}" lemma finite_simplex: "x∈X ⟹ finite x" using finite_simplices by simp lemma singleton_simplex: "v∈⋃X ⟹ {v} ∈ X" using faces by auto lemma maxsimpI: "x ∈ X ⟹ (⋀z. z∈X ⟹ x⊆z ⟹ z=x) ⟹ maxsimp x" using maxsimp_def by auto lemma maxsimpD_simplex: "maxsimp x ⟹ x∈X" using maxsimp_def by fast lemma maxsimpD_maximal: "maxsimp x ⟹ z∈X ⟹ x⊆z ⟹ z=x" using maxsimp_def by auto lemmas finite_maxsimp = finite_simplex[OF maxsimpD_simplex] lemma maxsimp_nempty: "X ≠ {{}} ⟹ maxsimp x ⟹ x ≠ {}" unfolding maxsimp_def by fast lemma maxsimp_vertices: "maxsimp x ⟹ x⊆⋃X" using maxsimpD_simplex by fast lemma adjacentsetD_adj: "y ∈ adjacentset x ⟹ x∼y" using adjacentset_def by fast lemma max_in_subcomplex: "⟦ Subcomplex Y; y ∈ Y; maxsimp y ⟧ ⟹ SimplicialComplex.maxsimp Y y" using maxsimpD_maximal by (fast intro: SimplicialComplex.maxsimpI) lemma face_im: assumes "w ∈ X" "y ⊆ f`w" defines "u ≡ {a∈w. f a ∈ y}" shows "y ∈ f⊢X" using assms faces[of w u] image_eqI[of y "(`) f" u X] by fast lemma im_faces: "x ∈ f ⊢ X ⟹ y ⊆ x ⟹ y ∈ f ⊢ X" using faces face_im[of _ y] by (cases "y={}") auto lemma map_is_simplicial_morph: "SimplicialComplex (f⊢X)" proof show "∀x∈f⊢X. finite x" using finite_simplices by fast show "⋀x y. x ∈f⊢X ⟹ y⊆x ⟹ y∈f⊢X" using im_faces by fast qed lemma vertex_set_int: assumes "SimplicialComplex Y" shows "⋃(X∩Y) = ⋃X ∩ ⋃Y" proof have "⋀v. v ∈ ⋃X ∩ ⋃Y ⟹ v∈ ⋃(X∩Y)" using faces SimplicialComplex.faces[OF assms] by auto thus "⋃(X∩Y) ⊇ ⋃X ∩ ⋃Y" by fast qed auto end (* context SimplicialComplex *) subsection ‹Chains of maximal simplices› text ‹ Chains of maximal simplices (with respect to adjacency) will allow us to walk through chamber complexes. But there is much we can say about them in simplicial complexes. We will call a chain of maximal simplices proper (using the prefix ‹p› as a naming convention to denote proper) if no maximal simplex appears more than once in the chain. (Some sources elect to call improper chains prechains, and reserve the name chain to describe a proper chain. And usually a slightly weaker notion of proper is used, requiring only that no maximal simplex appear twice in succession. But it essentially makes no difference, and we found it easier to use @{const distinct} rather than @{term "binrelchain not_equal"}.) › context SimplicialComplex begin definition "maxsimpchain xs ≡ (∀x∈set xs. maxsimp x) ∧ adjacentchain xs" definition "pmaxsimpchain xs ≡ (∀x∈set xs. maxsimp x) ∧ padjacentchain xs" function min_maxsimpchain :: "'a set list ⇒ bool" where "min_maxsimpchain [] = True" | "min_maxsimpchain [x] = maxsimp x" | "min_maxsimpchain (x#xs@[y]) = (x≠y ∧ is_arg_min length (λzs. maxsimpchain (x#zs@[y])) xs)" by (auto, rule list_cases_Cons_snoc) termination by (relation "measure length") auto lemma maxsimpchain_snocI: "⟦ maxsimpchain (xs@[x]); maxsimp y; x∼y ⟧ ⟹ maxsimpchain (xs@[x,y])" using maxsimpchain_def binrelchain_snoc maxsimpchain_def by auto lemma maxsimpchainD_maxsimp: "maxsimpchain xs ⟹ x ∈ set xs ⟹ maxsimp x" using maxsimpchain_def by fast lemma maxsimpchainD_adj: "maxsimpchain xs ⟹ adjacentchain xs" using maxsimpchain_def by fast lemma maxsimpchain_CConsI: "⟦ maxsimp w; maxsimpchain (x#xs); w∼x ⟧ ⟹ maxsimpchain (w#x#xs)" using maxsimpchain_def by auto lemma maxsimpchain_Cons_reduce: "maxsimpchain (x#xs) ⟹ maxsimpchain xs" using adjacentchain_Cons_reduce maxsimpchain_def by fastforce lemma maxsimpchain_append_reduce1: "maxsimpchain (xs@ys) ⟹ maxsimpchain xs" using binrelchain_append_reduce1 maxsimpchain_def by auto lemma maxsimpchain_append_reduce2: "maxsimpchain (xs@ys) ⟹ maxsimpchain ys" using binrelchain_append_reduce2 maxsimpchain_def by auto lemma maxsimpchain_remdup_adj: "maxsimpchain (xs@[x,x]@ys) ⟹ maxsimpchain (xs@[x]@ys)" using maxsimpchain_def binrelchain_remdup_adj by auto lemma maxsimpchain_rev: "maxsimpchain xs ⟹ maxsimpchain (rev xs)" using maxsimpchainD_maxsimp adjacent_sym binrelchain_sym_rev[of adjacent] unfolding maxsimpchain_def by fastforce lemma maxsimpchain_overlap_join: "maxsimpchain (xs@[w]) ⟹ maxsimpchain (w#ys) ⟹ maxsimpchain (xs@w#ys)" using binrelchain_overlap_join maxsimpchain_def by auto lemma pmaxsimpchain: "pmaxsimpchain xs ⟹ maxsimpchain xs" using maxsimpchain_def pmaxsimpchain_def by fast lemma pmaxsimpchainI_maxsimpchain: "maxsimpchain xs ⟹ distinct xs ⟹ pmaxsimpchain xs" using maxsimpchain_def pmaxsimpchain_def by fast lemma pmaxsimpchain_CConsI: "⟦ maxsimp w; pmaxsimpchain (x#xs); w∼x; w ∉ set (x#xs) ⟧ ⟹ pmaxsimpchain (w#x#xs)" using pmaxsimpchain_def by auto lemmas pmaxsimpchainD_maxsimp = maxsimpchainD_maxsimp[OF pmaxsimpchain] lemmas pmaxsimpchainD_adj = maxsimpchainD_adj [OF pmaxsimpchain] lemma pmaxsimpchainD_distinct: "pmaxsimpchain xs ⟹ distinct xs" using pmaxsimpchain_def by fast lemma pmaxsimpchain_Cons_reduce: "pmaxsimpchain (x#xs) ⟹ pmaxsimpchain xs" using maxsimpchain_Cons_reduce pmaxsimpchain pmaxsimpchainD_distinct by (fastforce intro: pmaxsimpchainI_maxsimpchain) lemma pmaxsimpchain_append_reduce1: "pmaxsimpchain (xs@ys) ⟹ pmaxsimpchain xs" using maxsimpchain_append_reduce1 pmaxsimpchain pmaxsimpchainD_distinct by (fastforce intro: pmaxsimpchainI_maxsimpchain) lemma maxsimpchain_obtain_pmaxsimpchain: assumes "x≠y" "maxsimpchain (x#xs@[y])" shows "∃ys. set ys ⊆ set xs ∧ length ys ≤ length xs ∧ pmaxsimpchain (x#ys@[y])" proof- obtain ys where ys: "set ys ⊆ set xs" "length ys ≤ length xs" "padjacentchain (x#ys@[y])" using maxsimpchainD_adj[OF assms(2)] adjacentchain_obtain_proper[OF assms(1)] by auto from ys(1) assms(2) have "∀a∈set (x#ys@[y]). maxsimp a" using maxsimpchainD_maxsimp by auto with ys show ?thesis unfolding pmaxsimpchain_def by auto qed lemma min_maxsimpchainD_maxsimpchain: assumes "min_maxsimpchain xs" shows "maxsimpchain xs" proof (cases xs rule: list_cases_Cons_snoc) case Nil thus ?thesis using maxsimpchain_def by simp next case Single with assms show ?thesis using maxsimpchain_def by simp next case Cons_snoc with assms show ?thesis using is_arg_minD1 by fastforce qed lemma min_maxsimpchainD_min_betw: "min_maxsimpchain (x#xs@[y]) ⟹ maxsimpchain (x#ys@[y]) ⟹ length ys ≥ length xs" using is_arg_minD2 by fastforce lemma min_maxsimpchainI_betw: assumes "x≠y" "maxsimpchain (x#xs@[y])" "⋀ys. maxsimpchain (x#ys@[y]) ⟹ length xs ≤ length ys" shows "min_maxsimpchain (x#xs@[y])" using assms by (simp add: is_arg_min_linorderI) lemma min_maxsimpchainI_betw_compare: assumes "x≠y" "maxsimpchain (x#xs@[y])" "min_maxsimpchain (x#ys@[y])" "length xs = length ys" shows "min_maxsimpchain (x#xs@[y])" using assms min_maxsimpchainD_min_betw min_maxsimpchainI_betw by auto lemma min_maxsimpchain_pmaxsimpchain: assumes "min_maxsimpchain xs" shows "pmaxsimpchain xs" proof ( rule pmaxsimpchainI_maxsimpchain, rule min_maxsimpchainD_maxsimpchain, rule assms, cases xs rule: list_cases_Cons_snoc ) case (Cons_snoc x ys y) have "¬ distinct (x#ys@[y]) ⟹ False" proof (cases "x∈set ys" "y∈set ys" rule: two_cases) case both from both(1) obtain as bs where "ys = as@x#bs" using in_set_conv_decomp[of x ys] by fast with assms Cons_snoc show False using min_maxsimpchainD_maxsimpchain[OF assms] maxsimpchain_append_reduce2[of "x#as"] min_maxsimpchainD_min_betw[of x ys y] by fastforce next case one from one(1) obtain as bs where "ys = as@x#bs" using in_set_conv_decomp[of x ys] by fast with assms Cons_snoc show False using min_maxsimpchainD_maxsimpchain[OF assms] maxsimpchain_append_reduce2[of "x#as"] min_maxsimpchainD_min_betw[of x ys y] by fastforce next case other from other(2) obtain as bs where "ys = as@y#bs" using in_set_conv_decomp[of y ys] by fast with assms Cons_snoc show False using min_maxsimpchainD_maxsimpchain[OF assms] maxsimpchain_append_reduce1[of "x#as@[y]"] min_maxsimpchainD_min_betw[of x ys y] by fastforce next case neither moreover assume "¬ distinct (x # ys @ [y])" ultimately obtain as a bs cs where "ys = as@[a]@bs@[a]@cs" using assms Cons_snoc not_distinct_decomp[of ys] by auto with assms Cons_snoc show False using min_maxsimpchainD_maxsimpchain[OF assms] maxsimpchain_append_reduce1[of "x#as@[a]"] maxsimpchain_append_reduce2[of "x#as@[a]@bs" "a#cs@[y]"] maxsimpchain_overlap_join[of "x#as" a "cs@[y]"] min_maxsimpchainD_min_betw[of x ys y "as@a#cs"] by auto qed with Cons_snoc show "distinct xs" by fast qed auto lemma min_maxsimpchain_rev: assumes "min_maxsimpchain xs" shows "min_maxsimpchain (rev xs)" proof (cases xs rule: list_cases_Cons_snoc) case Single with assms show ?thesis using min_maxsimpchainD_maxsimpchain maxsimpchainD_maxsimp by simp next case (Cons_snoc x ys y) moreover have "min_maxsimpchain (y # rev ys @ [x])" proof (rule min_maxsimpchainI_betw) from Cons_snoc assms show "y≠x" using min_maxsimpchain_pmaxsimpchain pmaxsimpchainD_distinct by auto from Cons_snoc show "maxsimpchain (y # rev ys @ [x])" using min_maxsimpchainD_maxsimpchain[OF assms] maxsimpchain_rev by fastforce from Cons_snoc assms show "⋀zs. maxsimpchain (y#zs@[x]) ⟹ length (rev ys) ≤ length zs" using maxsimpchain_rev min_maxsimpchainD_min_betw[of x ys y] by fastforce qed ultimately show ?thesis by simp qed simp lemma min_maxsimpchain_adj: "⟦ maxsimp x; maxsimp y; x∼y; x≠y ⟧ ⟹ min_maxsimpchain [x,y]" using maxsimpchain_def min_maxsimpchainI_betw[of x y "[]"] by simp lemma min_maxsimpchain_betw_CCons_reduce: assumes "min_maxsimpchain (w#x#ys@[z])" shows "min_maxsimpchain (x#ys@[z])" proof (rule min_maxsimpchainI_betw) from assms show "x≠z" using min_maxsimpchain_pmaxsimpchain pmaxsimpchainD_distinct by fastforce show "maxsimpchain (x#ys@[z])" using min_maxsimpchainD_maxsimpchain[OF assms] maxsimpchain_Cons_reduce by fast next fix zs assume "maxsimpchain (x#zs@[z])" hence "maxsimpchain (w#x#zs@[z])" using min_maxsimpchainD_maxsimpchain[OF assms] maxsimpchain_def by fastforce with assms show "length ys ≤ length zs" using min_maxsimpchainD_min_betw[of w "x#ys" z "x#zs"] by simp qed lemma min_maxsimpchain_betw_uniform_length: assumes "min_maxsimpchain (x#xs@[y])" "min_maxsimpchain (x#ys@[y])" shows "length xs = length ys" using min_maxsimpchainD_min_betw[OF assms(1)] min_maxsimpchainD_min_betw[OF assms(2)] min_maxsimpchainD_maxsimpchain[OF assms(1)] min_maxsimpchainD_maxsimpchain[OF assms(2)] by fastforce lemma not_min_maxsimpchainI_betw: "⟦ maxsimpchain (x#ys@[y]); length ys < length xs ⟧ ⟹ ¬ min_maxsimpchain (x#xs@[y])" using min_maxsimpchainD_min_betw not_less by blast lemma maxsimpchain_in_subcomplex: "⟦ Subcomplex Y; set ys ⊆ Y; maxsimpchain ys ⟧ ⟹ SimplicialComplex.maxsimpchain Y ys" using maxsimpchain_def max_in_subcomplex SimplicialComplex.maxsimpchain_def by force end (* context SimplicialComplex *) subsection ‹Isomorphisms of simplicial complexes› text ‹ Here we develop the concept of isomorphism of simplicial complexes. Note that we have not bothered to first develop the concept of morphism of simplicial complexes, since every function on the vertex set of a simplicial complex can be considered a morphism of complexes (see lemma ‹map_is_simplicial_morph› above). › locale SimplicialComplexIsomorphism = SimplicialComplex X for X :: "'a set set" + fixes f :: "'a ⇒ 'b" assumes inj: "inj_on f (⋃X)" begin lemmas morph = map_is_simplicial_morph[of f] lemma iso_codim_map: "x ∈ X ⟹ y ∈ X ⟹ card (f`x - f`y) = card (x-y)" using inj inj_on_image_set_diff[of f _ x y] finite_simplex subset_inj_on[of f _ "x-y"] inj_on_iff_eq_card[of "x-y"] by fastforce lemma maxsimp_im_max: "maxsimp x ⟹ w ∈ X ⟹ f`x ⊆ f`w ⟹ f`w = f`x" using maxsimpD_simplex inj_onD[OF inj] maxsimpD_maximal[of x w] by blast lemma maxsimp_map: "maxsimp x ⟹ SimplicialComplex.maxsimp (f⊢X) (f`x)" using maxsimpD_simplex maxsimp_im_max morph SimplicialComplex.maxsimpI[of "f⊢X" "f`x"] by fastforce lemma iso_adj_int_im: assumes "maxsimp x" "maxsimp y" "x∼y" "x≠y" shows "(f`x ∩ f`y) ⊲ f`x" proof (rule facetrelI_card) from assms(1,2) have 1: "f ` x ⊆ f ` y ⟹ f ` y = f ` x" using maxsimp_map SimplicialComplex.maxsimpD_simplex[OF morph] SimplicialComplex.maxsimpD_maximal[OF morph] by simp thus "f`x ∩ f`y ⊆ f`x" by fast from assms(1) have "card (f`x - f`x ∩ f`y) ≤ card (f`x - f`(x∩y))" using finite_maxsimp card_mono[of "f`x - f`(x∩y)" "f`x - f`x ∩ f`y"] by fast moreover from assms(1,3,4) have "card (f`x - f`(x∩y)) = 1" using maxsimpD_simplex faces[of x] maxsimpD_simplex iso_codim_map adjacent_int_facet1[of x y] facetrel_card by fastforce ultimately have "card (f`x - f`x ∩ f`y) ≤ 1" by simp moreover from assms(1,2,4) have "card (f`x - f`x ∩ f`y) ≠ 0" using 1 maxsimpD_simplex finite_maxsimp inj_onD[OF induced_pow_fun_inj_on, OF inj, of x y] by auto ultimately show "card (f`x - f`x ∩ f`y) = 1" by simp qed lemma iso_adj_map: assumes "maxsimp x" "maxsimp y" "x∼y" "x≠y" shows "f`x ∼ f`y" using assms(3,4) iso_adj_int_im[OF assms] adjacent_sym iso_adj_int_im[OF assms(2) assms(1)] by (auto simp add: Int_commute intro: adjacentI) lemma pmaxsimpchain_map: "pmaxsimpchain xs ⟹ SimplicialComplex.pmaxsimpchain (f⊢X) (f⊨xs)" proof (induct xs rule: list_induct_CCons) case Nil show ?case using map_is_simplicial_morph SimplicialComplex.pmaxsimpchain_def by fastforce next case (Single x) thus ?case using map_is_simplicial_morph pmaxsimpchainD_maxsimp maxsimp_map SimplicialComplex.pmaxsimpchain_def by fastforce next case (CCons x y xs) have "SimplicialComplex.pmaxsimpchain (f ⊢ X) ( f`x # f`y # f⊨xs)" proof ( rule SimplicialComplex.pmaxsimpchain_CConsI, rule map_is_simplicial_morph ) from CCons(2) show "SimplicialComplex.maxsimp (f⊢X) (f`x)" using pmaxsimpchainD_maxsimp maxsimp_map by simp from CCons show "SimplicialComplex.pmaxsimpchain (f⊢X) (f`y # f⊨xs)" using pmaxsimpchain_Cons_reduce by simp from CCons(2) show "f`x ∼ f`y" using pmaxsimpchain_def iso_adj_map by simp from inj CCons(2) have "distinct (f⊨(x#y#xs))" using maxsimpD_simplex inj_on_distinct_setlistmapim unfolding pmaxsimpchain_def by blast thus "f`x ∉ set (f`y # f⊨xs)" by simp qed thus ?case by simp qed end (* context SimplicialComplexIsomorphism *) subsection ‹The complex associated to a poset› text ‹ A simplicial complex is naturally a poset under the subset relation. The following develops the reverse direction: constructing a simplicial complex from a suitable poset. › context ordering begin definition PosetComplex :: "'a set ⇒ 'a set set" where "PosetComplex P ≡ (⋃x∈P. { {y. pseudominimal_in (P.❙≤x) y} })" lemma poset_is_SimplicialComplex: assumes "∀x∈P. simplex_like (P.❙≤x)" shows "SimplicialComplex (PosetComplex P)" proof (rule SimplicialComplex.intro, rule ballI) fix a assume "a ∈ PosetComplex P" from this obtain x where "x∈P" "a = {y. pseudominimal_in (P.❙≤x) y}" unfolding PosetComplex_def by fast with assms show "finite a" using pseudominimal_inD1 simplex_likeD_finite finite_subset[of a "P.❙≤x"] by fast next fix a b assume ab: "a ∈ PosetComplex P" "b⊆a" from ab(1) obtain x where x: "x∈P" "a = {y. pseudominimal_in (P.❙≤x) y}" unfolding PosetComplex_def by fast from assms x(1) obtain f and A::"nat set" where fA: "OrderingSetIso less_eq less (⊆) (⊂) (P.❙≤x) f" "f`(P.❙≤x) = Pow A" using simplex_likeD_iso[of "P.❙≤x"] by auto define x' where x': "x' ≡ the_inv_into (P.❙≤x) f (⋃(f`b))" from fA x(2) ab(2) x' have x'_P: "x'∈P" using collect_pseudominimals_below_in_poset[of P x f] by simp moreover from x fA ab(2) x' have "b = {y. pseudominimal_in (P.❙≤x') y}" using collect_pseudominimals_below_in_eq[of x P f] by simp ultimately show "b ∈ PosetComplex P" unfolding PosetComplex_def by fast qed definition poset_simplex_map :: "'a set ⇒ 'a ⇒ 'a set" where "poset_simplex_map P x = {y. pseudominimal_in (P.❙≤x) y}" lemma poset_to_PosetComplex_OrderingSetMap: assumes "⋀x. x∈P ⟹ simplex_like (P.❙≤x)" shows "OrderingSetMap (❙≤) (❙<) (⊆) (⊂) P (poset_simplex_map P)" proof from assms show "⋀a b. ⟦ a∈P; b∈P; a❙≤b ⟧ ⟹ poset_simplex_map P a ⊆ poset_simplex_map P b" using simplex_like_has_bottom pseudominimal_in_below_in unfolding poset_simplex_map_def by fast qed end (* context ordering *) text ‹ When a poset affords a simplicial complex, there is a natural morphism of posets from the source poset into the poset of sets in the complex, as above. However, some further assumptions are necessary to ensure that this morphism is an isomorphism. These conditions are collected in the following locale. › locale ComplexLikePoset = ordering less_eq less for less_eq :: "'a⇒'a⇒bool" (infix "❙≤" 50) and less :: "'a⇒'a⇒bool" (infix "❙<" 50) + fixes P :: "'a set" assumes below_in_P_simplex_like: "x∈P ⟹ simplex_like (P.❙≤x)" and P_has_bottom : "has_bottom P" and P_has_glbs : "x∈P ⟹ y∈P ⟹ ∃b. glbound_in_of P x y b" begin abbreviation "smap ≡ poset_simplex_map P" lemma smap_onto_PosetComplex: "smap ` P = PosetComplex P" using poset_simplex_map_def PosetComplex_def by auto lemma ordsetmap_smap: "⟦ a∈P; b∈P; a❙≤b ⟧ ⟹ smap a ⊆ smap b" using OrderingSetMap.ordsetmap[ OF poset_to_PosetComplex_OrderingSetMap, OF below_in_P_simplex_like ] poset_simplex_map_def by simp lemma inj_on_smap: "inj_on smap P" proof (rule inj_onI) fix x y assume xy: "x∈P" "y∈P" "smap x = smap y" show "x = y" proof (cases "smap x = {}") case True with xy show ?thesis using poset_simplex_map_def below_in_P_simplex_like P_has_bottom simplex_like_no_pseudominimal_in_below_in_imp_singleton[of x P] simplex_like_no_pseudominimal_in_below_in_imp_singleton[of y P] below_in_singleton_is_bottom[of P x] below_in_singleton_is_bottom[of P y] by auto next case False from this obtain z where "z ∈ smap x" by fast with xy(3) have z1: "z ∈ P.❙≤x" "z ∈ P.❙≤y" using pseudominimal_inD1 poset_simplex_map_def by auto hence "lbound_of x y z" by (auto intro: lbound_ofI) with z1(1) obtain b where b: "glbound_in_of P x y b" using xy(1,2) P_has_glbs by fast moreover have "b ∈ P.❙≤x" "b ∈ P.❙≤y" using glbound_in_ofD_in[OF b] glbound_in_of_less_eq1[OF b] glbound_in_of_less_eq2[OF b] by auto ultimately show ?thesis using xy below_in_P_simplex_like pseudominimal_in_below_in_less_eq_glbound[of P x _ y b] simplex_like_below_in_above_pseudominimal_is_top[of x P] simplex_like_below_in_above_pseudominimal_is_top[of y P] unfolding poset_simplex_map_def by force qed qed lemma OrderingSetIso_smap: "OrderingSetIso (❙≤) (❙<) (⊆) (⊂) P smap" proof (rule OrderingSetMap.isoI) show "OrderingSetMap (❙≤) (❙<) (⊆) (⊂) P smap" using poset_simplex_map_def below_in_P_simplex_like poset_to_PosetComplex_OrderingSetMap by simp next fix x y assume xy: "x∈P" "y∈P" "smap x ⊆ smap y" from xy(2) have "simplex_like (P.❙≤y)" using below_in_P_simplex_like by fast from this obtain g and A::"nat set" where "OrderingSetIso (❙≤) (❙<) (⊆) (⊂) (P.❙≤y) g" "g`(P.❙≤y) = Pow A" using simplex_likeD_iso[of "P.❙≤y"] by auto with xy show "x❙≤y" using poset_simplex_map_def collect_pseudominimals_below_in_eq[of y P g] collect_pseudominimals_below_in_poset[of P y g] inj_onD[OF inj_on_smap, of "the_inv_into (P.❙≤y) g (⋃(g ` smap x))" x] collect_pseudominimals_below_in_less_eq_top[of P y g A "smap x"] by simp qed (rule inj_on_smap) lemmas rev_ordsetmap_smap = OrderingSetIso.rev_ordsetmap[OF OrderingSetIso_smap] end (* context ComplexLikePoset *) end (* theory *)