Theory Chamber

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 chambers_share_facet:
  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_shared_facet: "⟦ 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_adjacent_shared_facet:
  "⟦ 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) thinish_image_shared_facet:
  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) thin_image_shared_facet =
  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