Theory Simplicial

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