# Theory Simplicial

theory Simplicial
imports Prelim
```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

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"

lemma empty_not_adjacent: "¬ {} ∼ x"

lemma adjacent_sym: "x ∼ y ⟹ y ∼ x"

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"

lemma adjacent_conv_insert: "x ∼ y ⟹ v ∈ x - y ⟹ x = insert v (x∩y)"

"x ∼ y ⟹ x ≠ y ⟹ ∃v. v ∉ y ∧ x = insert v (x∩y)"
using adjacent_int_facet1 unfolding facetrel_def by fast

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)"
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

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)"
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

"⟦ C ∼ D; f`C ∼ f`D; f`C ≠ f`D ⟧ ⟹ f`(C∩D) = f`C ∩ f`D"

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 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

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"

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

"maxsimpchain (xs@[x,x]@ys) ⟹ maxsimpchain (xs@[x]@ys)"

lemma maxsimpchain_rev: "maxsimpchain xs ⟹ maxsimpchain (rev xs)"
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]

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])"
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

"⟦ 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

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
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

assumes "maxsimp x" "maxsimp y" "x∼y" "x≠y"
shows   "f`x ∼ f`y"

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"
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 *)
```