# 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 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_obtain_pgallery   = maxsimpchain_obtain_pmaxsimpchain
lemmas pgallery_def              = pmaxsimpchain_def
lemmas pgalleryI_gallery         = pmaxsimpchainI_maxsimpchain
lemmas pgalleryD_chamber         = pmaxsimpchainD_maxsimp
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 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"
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)

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 chamber_shared_facet: "⟦ chamber C; z⊲C; D∈X; z⊲D ⟧ ⟹ chamber D"

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
with False obtain v where v: "v∉D" "C = insert v (C∩D)"
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}) ⟹
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

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
inj_on_insert[of f w "C∩D"]
bij_betw_imp_inj_on[OF label_wrtD', OF assms(1,3)]
qed

"⟦ label_wrt B f; chamber (insert v z); chamber (insert w z); v∉z; w∉z ⟧ ⟹
f v = f w"

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
)

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)

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

assumes "domain.chamber C" "domain.chamber D" "C ∼ D" "f`C ≠ f`D"
shows   "f`C ∼ f`D"

"⟦ domain.chamber C; domain.chamber D; C ∼ D ⟧ ⟹ f`C ∼ f`D"

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

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"
by    fastforce
qed
thus ?case by simp

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

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

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)"
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))"
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"
moreover from assms(4) fC fCfD False have "f w ∈ f`C - f`D"
ultimately show ?thesis
using assms(4) fD fCfD False adjacent_sym
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

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
by    force
next
case (snoc E Es)
with assms(2) show ?case
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
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]
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
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

assumes "chamber 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
qed

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

"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

"chamber C ⟹ z⊲C ⟹ C ∼ the_adj_chamber C z"

"chamber C ⟹ z ⊲ C ⟹ chamber (the_adj_chamber C z)"

"chamber C ⟹ z ⊲ C ⟹ the_adj_chamber C z ≠ C"
using theI'[OF thin] by fast

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"
with F_def chambers(4) have F_facet: "F⊲f`C" "F⊲f`D"

from F_def G_def chambers have "G = F"
by    force
with G_def morph(2) chambers have F_facet': "F⊲g`D"
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)"
from chambers(4) obtain w where w: "w ∉ f`C" "w ∈ f`D"
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)]
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)]
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"

assumes chambers: "C ∈ f⊢𝒞" "D ∈ 𝒞-f⊢𝒞"
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

"⟦ C ∈ f⊢𝒞; D ∈ 𝒞-f⊢𝒞; C∼D ⟧ ⟹ opp_chamber 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"
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]"]
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])"