# Theory Chamber

theory Chamber
imports Algebra Simplicial
```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])"
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]

lemma gallery_double_cross_not_minimal1:
"⟦ B∈f⊢𝒞; C∈𝒞-f⊢𝒞; D∈f⊢𝒞; gallery (B#Bs@C#Cs@[D]) ⟧ ⟹
¬ min_gallery (B#Bs@C#Cs@[D])"
proof (induct Bs arbitrary: B)
case Nil thus ?case using gallery_double_cross_not_minimal_Cons1 by simp
next
case (Cons E Es)
show ?case
proof (cases "E∈f⊢𝒞")
case True
with Cons(1,3-5) show ?thesis
using gallery_Cons_reduce[of B "E#Es@C#Cs@[D]"]
min_gallery_betw_CCons_reduce[of B E "Es@C#Cs" D]
by    auto
next
case False with Cons(2,4,5) show ?thesis
using gallery_chamber_system
gallery_double_cross_not_minimal_Cons1[of B E D "Es@C#Cs"]
by    force
qed
qed

end (* ThinishChamberComplexFolding *)

locale ThinChamberComplexFolding =
ThinChamberComplex X + folding: ChamberComplexFolding X f
for X :: "'a set set"
and f :: "'a⇒'a"

sublocale ThinChamberComplexFolding < ThinishChamberComplexFolding ..

context ThinChamberComplexFolding
begin

abbreviation "flop ≡ folding.flop"

lemmas gallery_double_cross_not_minimal1  = gallery_double_cross_not_minimal1
lemmas gallery_double_cross_not_minimal_Cons1 =
gallery_double_cross_not_minimal_Cons1

assumes chambers: "C ∈ 𝒞-f⊢𝒞" "D ∈ 𝒞-f⊢𝒞"
shows "C ∼ D"
proof (cases "f`C=f`D")
case True
with chambers show "C ∼ D"
using folding.inj_on_opp_chambers''[of C D] adjacent_refl[of C] by auto
next
case False
from chambers have CD: "chamber C" "chamber D"
using chamber_system_def by auto
hence ch_fCD: "chamber (f`C)" "chamber (f`D)"
using chamber_system_def folding.chamber_map by auto
from adjacent obtain z where z: "z ⊲ f`C" "z ⊲ f`D"
from chambers(1) z(1) obtain y where y: "y ⊲ C" "f`y = z"
using chamber_system_def folding.inj_on_chamber[of C]
inj_on_pullback_facet[of f C z]
by    auto
define B where "B = the_adj_chamber C y"
with CD(1) y(1) have B: "chamber B" "y⊲B" "B≠C"
have "f`B ≠ f`C"
proof (cases "B ∈ f⊢𝒞")
case False with chambers(1) show ?thesis
using B(1,3) chamber_system_def folding.inj_on_opp_chambers''[of B]
by    auto
next
case True show ?thesis
proof
assume fB_fC: "f`B = f`C"
with True have "B = f`C" using folding.chamber_retraction2 by auto
with z(1) y(2) B(2) chambers(1) have "y = z"
using facetrel_subset[of y B] chamber_system_def chamberD_simplex face_im
folding.simplex_retraction2[of y]
by    force
with chambers y(1) z(2) have "f`D = B"
using CD(1) ch_fCD(2) B facet_unique_other_chamber[of C y] by auto
with z(2) chambers fB_fC False show False
using folding.chamber_retraction2 by force
qed
qed
with False z y(2) have fB_fD: "f`B = f`D"
using ch_fCD B(1,2) folding.chamber_map folding.facet_map
facet_unique_other_chamber[of "f`C" z]
by    force
have "B = D"
proof (cases "B ∈ f⊢𝒞")
case False
with B(1) chambers(2) show ?thesis
using chamber_system_def fB_fD folding.inj_on_opp_chambers'' by simp
next
case True
with fB_fD have "B = f`D" using folding.chamber_retraction2 by auto
moreover with z(1) y(2) B(2) chambers(2) have "y = z"
using facetrel_subset[of y B] chamber_system_def chamberD_simplex face_im
folding.simplex_retraction2[of y]
by    force
ultimately show ?thesis
using CD y(1) B ch_fCD(1) z(1) False chambers(1)
facet_unique_other_chamber[of B y C "f`C"]
by    auto
qed
with y(1) B(2) show ?thesis using adjacentI by fast
qed

"⟦ C∈f⊢𝒞; D∈f⊢𝒞; C∼D ⟧ ⟹ opp_chamber C ∼ opp_chamber D"
using folding.opp_chamberD1 folding.opp_chamberD2 adjacent_preimage by simp

using adjacent_preimage by (induct Cs rule: list_induct_CCons) auto

lemma gallery_preimage: "set Cs ⊆ 𝒞-f⊢𝒞 ⟹ gallery (f⊨Cs) ⟹ gallery Cs"
by    fast

lemma chambercomplex_opp_half_apartment: "ChamberComplex folding.Y"
proof (intro_locales, rule folding.simplicialcomplex_opp_half_apartment, unfold_locales)
define Y where "Y = folding.Y"
fix y assume "y∈Y"
with Y_def obtain C where "C∈𝒞-f⊢𝒞" "y⊆C"
using folding.opp_half_apartment_def by auto
with Y_def show "∃x. SimplicialComplex.maxsimp Y x ∧ y ⊆ x"
using folding.subcomplex_opp_half_apartment
folding.opp_chambers_subset_opp_half_apartment
chamber_system_def max_in_subcomplex[of Y]
by    force
next
define Y where "Y = folding.Y"
fix C D
assume CD:  "SimplicialComplex.maxsimp Y C" "SimplicialComplex.maxsimp Y D"
"C≠D"
from CD(1,2) Y_def have CD': "C ∈ 𝒞-f⊢𝒞" "D ∈ 𝒞-f⊢𝒞"
using folding.maxsimp_in_opp_half_apartment by auto
with CD(3) obtain Ds
where Ds: "ChamberComplex.gallery (f⊢X) ((f`C)#Ds@[f`D])"
using folding.inj_on_opp_chambers''[of C D] chamber_system_def
folding.maxsimp_map_into_image folding.chambercomplex_image
ChamberComplex.maxsimp_connect[of "f⊢X" "f`C" "f`D"]
by    auto
define Cs where "Cs = map opp_chamber Ds"
from Ds have Ds': "gallery ((f`C)#Ds@[f`D])"
using folding.chambersubcomplex_image subcomplex_gallery by fast
with Ds have Ds'': "set Ds ⊆ f⊢𝒞"
using folding.chambercomplex_image folding.chamber_system_image
ChamberComplex.galleryD_chamber ChamberComplex.chamberD_simplex
gallery_chamber_system
by    fastforce
have *: "set Cs ⊆ 𝒞-f⊢𝒞"
proof
fix B assume "B ∈ set Cs"
with Cs_def obtain A where "A∈set Ds" "B = opp_chamber A" by auto
with Ds'' show "B ∈ 𝒞-f⊢𝒞" using folding.opp_chamberD1[of A] by auto
qed
moreover from Cs_def CD' Ds' Ds'' * have "gallery (C#Cs@[D])"
using folding.f_opp_chamber_list gallery_preimage[of "C#Cs@[D]"] by simp
ultimately show "∃Cs. SimplicialComplex.maxsimpchain Y (C # Cs @ [D])"
using Y_def CD' folding.subcomplex_opp_half_apartment
folding.opp_chambers_subset_opp_half_apartment
maxsimpchain_in_subcomplex[of Y "C#Cs@[D]"]
by    fastforce
qed

assumes "chamber C" "chamber D" "C∼D"
shows   "flop C ∼ flop D"
proof (cases "C∈f⊢𝒞" "D∈f⊢𝒞" rule: two_cases)
case both
with assms(3) show ?thesis using adjacent_opp_chamber by simp
next
case one
with assms(2,3) show ?thesis
by    simp
next
case other
with assms(1) show ?thesis
by    auto

lemma flop_gallery: "gallery Cs ⟹ gallery (map flop Cs)"
proof (induct Cs rule: list_induct_CCons)
case (CCons B C Cs)
have "gallery (flop B # (flop C) # map flop Cs)"
proof (rule gallery_CConsI)
from CCons(2) show "chamber (flop B)"
using galleryD_chamber folding.flop_chamber by simp
from CCons(1) show "gallery (flop C # map flop Cs)"
using gallery_Cons_reduce[OF CCons(2)] by simp
from CCons(2) show "flop B ∼ flop C"
qed
thus ?case by simp
qed (auto simp add: galleryD_chamber folding.flop_chamber gallery_def)

lemma morphism_half_apartments: "ChamberComplexMorphism folding.Y (f⊢X) f"
proof (
rule ChamberComplexMorphism.intro, rule chambercomplex_opp_half_apartment,
rule folding.chambercomplex_image, unfold_locales
)
show
"⋀C. SimplicialComplex.maxsimp folding.Y C ⟹
SimplicialComplex.maxsimp (f⊢X) (f`C)"
"⋀C. SimplicialComplex.maxsimp folding.Y C ⟹ card (f`C) = card C"
using folding.chamber_in_opp_half_apartment folding.chamber_map
folding.chambersubcomplex_image chamber_in_subcomplex
chamberD_simplex folding.dim_map
by    auto
qed

lemma chamber_image_complement_closer:
"⟦ D∈𝒞-f⊢𝒞; B∈𝒞-f⊢𝒞; B≠D; gallery (B#Cs@[f`D]) ⟧ ⟹
∃Ds. gallery (B#Ds@[D]) ∧ length Ds < length Cs"
using flop_gallery chamber_image_closer[of D "f`B" "map flop Cs"]
folding.opp_chamber_reverse folding.inj_on_opp_chambers''[of B D]
by    force

lemma chamber_image_complement_subset:
assumes D: "D∈𝒞-f⊢𝒞"
defines C: "C ≡ f`D"
defines "closerToD ≡ {B∈𝒞. chamber_distance B D < chamber_distance B C}"
shows   "𝒞-f⊢𝒞 ⊆ closerToD"
proof
fix B assume B: "B∈𝒞-f⊢𝒞"
show "B ∈ closerToD"
proof (cases "B=D")
case True with B C closerToD_def show ?thesis
using chamber_distance_def by auto
next
case False
define Cs where "Cs = (ARG_MIN length Cs. gallery (B#Cs@[C]))"
with B C D False closerToD_def show ?thesis
using chamber_system_def folding.chamber_map[of D]
gallery_least_length[of B C] chamber_distance_le
chamber_image_complement_closer[of D B Cs]
chamber_distance_def[of B C]
by    fastforce
qed
qed

lemma chamber_image_and_complement:
assumes D: "D∈𝒞-f⊢𝒞"
defines C: "C ≡ f`D"
defines "closerToC ≡ {B∈𝒞. chamber_distance B C < chamber_distance B D}"
and     "closerToD ≡ {B∈𝒞. chamber_distance B D < chamber_distance B C}"
shows "f⊢𝒞 = closerToC" "𝒞-f⊢𝒞 = closerToD"
proof-
from closerToC_def closerToD_def have "closerToC ∩ closerToD = {}" by auto
moreover from C D closerToC_def closerToD_def
have "𝒞 = f ⊢ 𝒞 ∪ (𝒞-f⊢𝒞)" "closerToC ⊆ 𝒞" "closerToD ⊆ 𝒞"
using folding.chamber_system_into
by    auto
moreover from assms have "f⊢𝒞 ⊆ closerToC" "𝒞-f⊢𝒞 ⊆ closerToD"
using chamber_image_subset chamber_image_complement_subset by auto
ultimately show "f⊢𝒞 = closerToC" "𝒞-f⊢𝒞 = closerToD"
using set_decomp_subset[of 𝒞 "f⊢𝒞"] set_decomp_subset[of 𝒞 "𝒞-f⊢𝒞"] by auto
qed

end (* context ThinChamberComplexFolding *)

subsubsection ‹Pairs of opposed foldings›

text ‹
A pair of foldings of a thin chamber complex are opposed or opposite if there is a corresponding
pair of adjacent chambers, where each folding sends its corresponding chamber to the other
chamber.
›

locale OpposedThinChamberComplexFoldings =
ThinChamberComplex X
+ folding_f: ChamberComplexFolding X f
+ folding_g: ChamberComplexFolding X g
for X :: "'a set set"
and f :: "'a⇒'a"
and g :: "'a⇒'a"
+ fixes C0 :: "'a set"
assumes chambers: "chamber C0" "C0∼g`C0" "C0≠g`C0" "f`g`C0 = C0"
begin

abbreviation "D0 ≡ g`C0"

lemmas chamber_D0 = folding_g.chamber_map[OF chambers(1)]

lemma ThinChamberComplexFolding_f: "ThinChamberComplexFolding X f" ..
lemma ThinChamberComplexFolding_g: "ThinChamberComplexFolding X g" ..

lemmas foldf = ThinChamberComplexFolding_f
lemmas foldg = ThinChamberComplexFolding_g

lemma fg_symmetric: "OpposedThinChamberComplexFoldings X g f D0"
using chambers(2-4) chamber_D0 adjacent_sym by unfold_locales auto

lemma basechambers_half_chamber_systems: "C0∈f⊢𝒞" "D0∈g⊢𝒞"
using chambers(1,4) chamber_D0 chamber_system_def by auto

lemmas basech_halfchsys =
basechambers_half_chamber_systems

lemma f_trivial_C0: "v∈C0 ⟹ f v = v"
using chambers(4) chamber_D0 chamberD_simplex[of D0]
folding_f.vertex_retraction
by    fast

lemmas g_trivial_D0 =
OpposedThinChamberComplexFoldings.f_trivial_C0[OF fg_symmetric]

lemma double_fold_D0:
assumes "v ∈ D0 - C0"
shows   "g (f v) = v"
proof-
from assms chambers(2) have 1: "D0 = insert v (C0∩D0)"
hence "f`D0 = insert (f v) (f`(C0∩D0))" by fast
moreover have "f`(C0∩D0) = C0∩D0" using f_trivial_C0 by force
ultimately have "C0 = insert (f v) (C0∩D0)" using chambers(4) by simp
hence "g`C0 = insert (g (f v)) (g`(C0∩D0))" by force
moreover have "g`(C0∩D0) = C0∩D0"
using g_trivial_D0 fixespointwise_im[of g D0 "C0∩D0"]
by    (fastforce intro: fixespointwiseI)
ultimately have "D0 = insert (g (f v)) (C0∩D0)" by simp
with assms show ?thesis using 1 by force
qed

lemmas double_fold_C0 =
OpposedThinChamberComplexFoldings.double_fold_D0[OF fg_symmetric]

lemma flopped_half_chamber_systems_fg: "𝒞-f⊢𝒞 = g⊢𝒞"
proof-
from chambers(1,3,4) have "D0∈𝒞-f⊢𝒞" "C0∈𝒞-g⊢𝒞"
using chamber_system_def chamber_D0 folding_f.chamber_retraction2[of D0]
folding_g.chamber_retraction2[of C0]
by    auto
with chambers(2,4) show ?thesis
using ThinChamberComplexFolding.chamber_image_and_complement[
OF ThinChamberComplexFolding_g, of C0
]
ThinChamberComplexFolding.chamber_image_and_complement[
OF ThinChamberComplexFolding_f, of D0
]
by    force
qed

lemmas flopped_half_chamber_systems_gf =
OpposedThinChamberComplexFoldings.flopped_half_chamber_systems_fg[
OF fg_symmetric
]

lemma flopped_half_apartments_fg: "folding_f.opp_half_apartment = g⊢X"
proof (rule seteqI)
fix a assume "a ∈ folding_f.Y"
from this obtain C where "C∈g⊢𝒞" "a⊆C"
using folding_f.opp_half_apartment_def flopped_half_chamber_systems_fg by auto
thus "a∈g⊢X"
using chamber_system_simplices
ChamberComplex.faces[OF folding_g.chambercomplex_image, of C]
by    auto
next
fix b assume b: "b ∈ g⊢X"
from this obtain C where C: "C∈𝒞" "b ⊆ g`C"
using simplex_in_max chamber_system_def by fast
from C(1) have "g`C ∈ g⊢𝒞" by fast
hence "g`C ∈ 𝒞-f⊢𝒞" using flopped_half_chamber_systems_fg by simp
with C(2) have "∃C∈𝒞-f⊢𝒞. b⊆C" by auto
moreover from b have "b∈X" using folding_g.simplex_map by fast
ultimately show "b ∈ folding_f.Y"
unfolding folding_f.opp_half_apartment_def by simp
qed

lemmas flopped_half_apartments_gf =
OpposedThinChamberComplexFoldings.flopped_half_apartments_fg[
OF fg_symmetric
]

lemma vertex_set_split: "⋃X = f`(⋃X) ∪ g`(⋃X)"
― ‹@{term f} and @{term g} will both be the identity on the intersection›
proof
show "⋃X ⊇ f`(⋃X) ∪ g`(⋃X)"
using folding_f.simplex_map folding_g.simplex_map by auto
show "⋃X ⊆ f`(⋃X) ∪ g`(⋃X)"
proof
fix a assume "a∈⋃X"
from this obtain C where C: "chamber C" "a∈C"
using simplex_in_max by fast
from C(1) have "C∈f⊢𝒞 ∨ C∈g⊢𝒞"
using chamber_system_def flopped_half_chamber_systems_fg by auto
with C(2) show "a ∈ (f`⋃X) ∪ (g`⋃X)"
using chamber_system_simplices by fast
qed
qed

lemma half_chamber_system_disjoint_union:
"𝒞 = f⊢𝒞 ∪ g⊢𝒞" "(f⊢𝒞) ∩ (g⊢𝒞) = {}"
using folding_f.chamber_system_into
flopped_half_chamber_systems_fg[THEN sym]
by    auto

lemmas halfchsys_decomp =
half_chamber_system_disjoint_union

lemma chamber_in_other_half_fg: "chamber C ⟹ C∉f⊢𝒞 ⟹ C∈g⊢𝒞"
using chamber_system_def half_chamber_system_disjoint_union(1) by blast

"C∈f⊢𝒞 ⟹ D∈g⊢𝒞 ⟹ C∼D ⟹ f`D = C"
OF ThinChamberComplexFolding_f
]

OF fg_symmetric
]

lemma switch_basechamber:
assumes "C∈f⊢𝒞" "C∼g`C"
shows   "OpposedThinChamberComplexFoldings X f g C"
proof
from assms(1) have "C∈𝒞-g⊢𝒞" using flopped_half_chamber_systems_gf by simp
with assms show "chamber C" "C ≠ g`C" "f`g`C = C"
by    auto
qed (rule assms(2))

lemma unique_half_chamber_system_f:
assumes "OpposedThinChamberComplexFoldings X f' g' C0" "g'`C0 = D0"
shows   "f'⊢𝒞 = f⊢𝒞"
proof-
have 1: "OpposedThinChamberComplexFoldings X f g' C0"
proof (rule OpposedThinChamberComplexFoldings.intro)
show "ChamberComplexFolding X f" "ThinChamberComplex X" ..
from assms(1) show "ChamberComplexFolding X g'"
using OpposedThinChamberComplexFoldings.axioms(3) by fastforce
from assms(2) chambers
show  "OpposedThinChamberComplexFoldings_axioms X f g' C0"
by    unfold_locales auto
qed
define a b where "a = f'⊢𝒞" and "b = f⊢𝒞"
hence "a⊆𝒞" "b⊆𝒞" "𝒞-a = 𝒞-b"
using OpposedThinChamberComplexFoldings.axioms(2)[OF assms(1)]
OpposedThinChamberComplexFoldings.axioms(2)[OF 1]
ChamberComplexFolding.chamber_system_into[of X f]
ChamberComplexFolding.chamber_system_into[of X f']
OpposedThinChamberComplexFoldings.flopped_half_chamber_systems_fg[
OF assms(1)
]
OpposedThinChamberComplexFoldings.flopped_half_chamber_systems_fg[
OF 1
]
by    auto
hence "a=b" by fast
with a_def b_def show ?thesis by simp
qed

lemma unique_half_chamber_system_g:
"OpposedThinChamberComplexFoldings X f' g' C0 ⟹ g'`C0 = D0 ⟹
g'⊢𝒞 = g⊢𝒞"
using unique_half_chamber_system_f flopped_half_chamber_systems_fg
OpposedThinChamberComplexFoldings.flopped_half_chamber_systems_fg[
of X f' g'
]
by    simp

lemma split_gallery_fg:
"⟦ C∈f⊢𝒞; D∈g⊢𝒞; gallery (C#Cs@[D]) ⟧ ⟹
∃As A B Bs. A∈f⊢𝒞 ∧ B∈g⊢𝒞 ∧ C#Cs@[D] = As@A#B#Bs"
using folding_f.split_gallery flopped_half_chamber_systems_fg by simp

lemmas split_gallery_gf =
OpposedThinChamberComplexFoldings.split_gallery_fg[OF fg_symmetric]

end (* context OpposedThinChamberComplexFoldings *)

subsubsection ‹The automorphism induced by a pair of opposed foldings›

text ‹
Recall that a folding of a chamber complex is a special kind of chamber complex retraction, and
so is the identity on its image. Hence a pair of opposed foldings will be the identity on the
intersection of their images and so we can stitch them together to create an automorphism of the
chamber complex, by allowing each folding to act on the complement of its image.
This automorphism will be of order two, and will be the unique automorphism of the chamber
complex that fixes pointwise the facet shared by the pair of adjacent chambers associated to the
opposed foldings.
›

context OpposedThinChamberComplexFoldings
begin

definition induced_automorphism :: "'a⇒'a"
where "induced_automorphism v ≡
if v∈f`(⋃X) then g v else if v∈g`(⋃X) then f v else v"
― ‹@{term f} and @{term g} will both be the identity on the intersection of their images›
abbreviation "𝗌 ≡ induced_automorphism"

lemma induced_automorphism_fg_symmetric:
"𝗌 = OpposedThinChamberComplexFoldings.𝗌 X g f"
folding_f.vertex_retraction folding_g.vertex_retraction
induced_automorphism_def
OpposedThinChamberComplexFoldings.induced_automorphism_def[
OF fg_symmetric
]
)

lemma induced_automorphism_on_simplices_fg: "x∈f⊢X ⟹ v∈x ⟹ 𝗌 v = g v"
using induced_automorphism_def by auto

lemma induced_automorphism_eq_foldings_on_chambers_fg:
"C∈f⊢𝒞 ⟹ fun_eq_on 𝗌 g C"
using chamber_system_simplices induced_automorphism_on_simplices_fg[of C]
by    (fast intro: fun_eq_onI)

lemmas indaut_eq_foldch_fg =
induced_automorphism_eq_foldings_on_chambers_fg

lemma induced_automorphism_eq_foldings_on_chambers_gf:
"C∈g⊢𝒞 ⟹ fun_eq_on 𝗌 f C"
OpposedThinChamberComplexFoldings.indaut_eq_foldch_fg[
OF fg_symmetric
]
induced_automorphism_fg_symmetric
)

lemma induced_automorphism_on_chamber_vertices_f:
"chamber C ⟹ v∈C ⟹ 𝗌 v = (if C∈f⊢𝒞 then g v else f v)"
using chamber_system_def induced_automorphism_eq_foldings_on_chambers_fg
induced_automorphism_eq_foldings_on_chambers_gf
flopped_half_chamber_systems_fg[THEN sym]
fun_eq_onD[of 𝗌 g C] fun_eq_onD[of 𝗌 f C]
by    auto

lemma induced_automorphism_simplex_image:
"C∈f⊢𝒞 ⟹ x⊆C ⟹ 𝗌`x = g`x" "C∈g⊢𝒞 ⟹ x⊆C ⟹ 𝗌`x = f`x"
using fun_eq_on_im[of 𝗌 g C] fun_eq_on_im[of 𝗌 f C]
induced_automorphism_eq_foldings_on_chambers_fg
induced_automorphism_eq_foldings_on_chambers_gf
by    auto

lemma induced_automorphism_chamber_list_image_fg:
"set Cs ⊆ f⊢𝒞 ⟹ 𝗌⊨Cs = g⊨Cs"
proof (induct Cs)
case (Cons C Cs) thus ?case
using induced_automorphism_simplex_image(1)[of C] by simp
qed simp

lemma induced_automorphism_chamber_image_fg:
"chamber C ⟹ 𝗌`C = (if C∈f⊢𝒞 then g`C else f`C)"
using chamber_system_def induced_automorphism_simplex_image
flopped_half_chamber_systems_fg[THEN sym]
by    auto

lemma induced_automorphism_C0: "𝗌`C0 = D0"
using chambers(1,4) basechambers_half_chamber_systems(1)
induced_automorphism_chamber_image_fg
by    auto

lemma induced_automorphism_fixespointwise_C0_int_D0:
"fixespointwise 𝗌 (C0∩D0)"
using fun_eq_on_trans[of 𝗌 g] fun_eq_on_subset[of 𝗌 g C0]
fixespointwise_subset[of g D0]
induced_automorphism_eq_foldings_on_chambers_fg
basechambers_half_chamber_systems
folding_g.chamber_retraction1
by    auto

lemmas indaut_fixes_fundfacet =
induced_automorphism_fixespointwise_C0_int_D0

"⟦ C∈f⊢𝒞; D∈g⊢𝒞; C∼D ⟧ ⟹ 𝗌`D = C"
induced_automorphism_simplex_image(2)
by    auto

lemma induced_automorphism_chamber_map: "chamber C ⟹ chamber (𝗌`C)"
using induced_automorphism_chamber_image_fg folding_f.chamber_map
folding_g.chamber_map
by    auto

lemmas indaut_chmap = induced_automorphism_chamber_map

lemma induced_automorphism_ntrivial: "𝗌 ≠ id"
proof
assume 𝗌: "𝗌 = id"
from chambers(2,3) obtain v where v: "v ∉ D0" "C0 = insert v (C0∩D0)"
using adjacent_int_decomp[of C0 D0] by fast
from chambers(4) 𝗌 v(2) have gv: "g v = v"
using chamberD_simplex[OF chamber_D0]
induced_automorphism_on_simplices_fg[of C0 v, THEN sym]
by    auto
have "g`C0 = C0"
proof (rule seteqI)
from v(2) gv show "⋀x. x∈C0 ⟹ x∈g`C0" using g_trivial_D0 by force
next
fix x assume "x∈g`C0"
from this obtain y where y: "y∈C0" "x = g y" by fast
moreover from y(1) v(2) gv have "g y = y"
using g_trivial_D0[of y] by (cases "y=v") auto
ultimately show "x∈C0" using y by simp
qed
with chambers(3) show False by fast
qed

lemma induced_automorphism_bij_between_half_chamber_systems_f:
"bij_betw ((`) 𝗌) (𝒞-f⊢𝒞) (f⊢𝒞)"
using induced_automorphism_simplex_image(2)
flopped_half_chamber_systems_fg
folding_f.opp_chambers_bij bij_betw_cong[of "𝒞-f⊢𝒞" "(`) 𝗌"]
by    auto

lemmas indaut_bij_btw_halfchsys_f =
induced_automorphism_bij_between_half_chamber_systems_f

lemma induced_automorphism_bij_between_half_chamber_systems_g:
"bij_betw ((`) 𝗌) (𝒞-g⊢𝒞) (g⊢𝒞)"
using induced_automorphism_fg_symmetric
OpposedThinChamberComplexFoldings.indaut_bij_btw_halfchsys_f[
OF fg_symmetric
]
by    simp

lemma induced_automorphism_halfmorphism_fopp_to_fimage:
"ChamberComplexMorphism folding_f.opp_half_apartment (f⊢X) 𝗌"
proof (
rule ChamberComplexMorphism.cong,
rule ThinChamberComplexFolding.morphism_half_apartments,
rule ThinChamberComplexFolding_f, rule fun_eq_onI
)
show "⋀v. v ∈ ⋃folding_f.Y ⟹ 𝗌 v = f v"
using folding_f.opp_half_apartment_def chamber_system_simplices
flopped_half_chamber_systems_fg
induced_automorphism_fg_symmetric
OpposedThinChamberComplexFoldings.induced_automorphism_def[
OF fg_symmetric
]
)
qed

lemmas indaut_halfmorph_fopp_fim =
induced_automorphism_halfmorphism_fopp_to_fimage

lemma induced_automorphism_half_chamber_system_gallery_map_f:
"set Cs ⊆ f⊢𝒞 ⟹ gallery Cs ⟹ gallery (𝗌⊨Cs)"
using folding_g.gallery_map[of Cs]
induced_automorphism_chamber_list_image_fg[THEN sym]
by    auto

lemma induced_automorphism_half_chamber_system_pgallery_map_f:
"set Cs ⊆ f⊢𝒞 ⟹ pgallery Cs ⟹ pgallery (𝗌⊨Cs)"
using induced_automorphism_half_chamber_system_gallery_map_f pgallery
flopped_half_chamber_systems_gf pgalleryD_distinct
folding_g.opp_chambers_distinct_map
induced_automorphism_chamber_list_image_fg[THEN sym]
by    (auto intro: pgalleryI_gallery)

lemmas indaut_halfchsys_pgal_map_f =
induced_automorphism_half_chamber_system_pgallery_map_f

lemma induced_automorphism_half_chamber_system_pgallery_map_g:
"set Cs ⊆ g⊢𝒞 ⟹ pgallery Cs ⟹ pgallery (𝗌⊨Cs)"
using induced_automorphism_fg_symmetric
OpposedThinChamberComplexFoldings.indaut_halfchsys_pgal_map_f[
OF fg_symmetric
]
by    simp

lemma induced_automorphism_halfmorphism_fimage_to_fopp:
"ChamberComplexMorphism (f⊢X) folding_f.opp_half_apartment 𝗌"
using OpposedThinChamberComplexFoldings.indaut_halfmorph_fopp_fim[
OF fg_symmetric
]
flopped_half_apartments_gf flopped_half_apartments_fg
induced_automorphism_fg_symmetric
)

lemma induced_automorphism_selfcomp_halfmorphism_f:
"ChamberComplexMorphism (f⊢X) (f⊢X) (𝗌∘𝗌)"
using induced_automorphism_halfmorphism_fimage_to_fopp
induced_automorphism_halfmorphism_fopp_to_fimage
by    (auto intro: ChamberComplexMorphism.comp)

lemma induced_automorphism_selfcomp_halftrivial_f: "fixespointwise (𝗌∘𝗌) (⋃(f⊢X))"
proof (
rule standard_uniqueness, rule ChamberComplexMorphism.expand_codomain,
rule induced_automorphism_selfcomp_halfmorphism_f
)
show "ChamberComplexMorphism (f⊢X) X id"
using folding_f.chambersubcomplex_image inclusion_morphism by fast
show "SimplicialComplex.maxsimp (f⊢X) C0"
using chambers(1,4) chamberD_simplex[OF chamber_D0]
chamber_in_subcomplex[OF folding_f.chambersubcomplex_image, of C0]
by    auto
show "fixespointwise (𝗌∘𝗌) C0"
proof (rule fixespointwiseI)
fix v assume v: "v∈C0"
with chambers(4) have "v∈f`(⋃X)"
using chamber_D0 chamberD_simplex by fast
hence 1: "𝗌 v = g v" using induced_automorphism_def by simp
show "(𝗌∘𝗌) v = id v"
proof (cases "v∈D0")
case True with v show ?thesis using 1 g_trivial_D0 by simp
next
case False
from v chambers(1,4) have "𝗌 (g v) = f (g v)"
using chamberD_simplex induced_automorphism_fg_symmetric
OpposedThinChamberComplexFoldings.induced_automorphism_def[
OF fg_symmetric, of "g v"
]
by    force
with v False chambers(4) show ?thesis using double_fold_C0 1 by simp
qed
qed
next
fix Cs assume "ChamberComplex.min_gallery (f⊢X) (C0#Cs)"
hence Cs: "ChamberComplex.pgallery (f⊢X) (C0#Cs)"
using ChamberComplex.min_gallery_pgallery folding_f.chambercomplex_image
by    fast
hence pCs: "pgallery (C0#Cs)"
using folding_f.chambersubcomplex_image subcomplex_pgallery by auto
thus "pgallery (id⊨(C0#Cs))" by simp
have set_Cs: "set (C0#Cs) ⊆ f⊢𝒞"
using Cs pCs folding_f.chambersubcomplex_image
ChamberSubcomplexD_complex ChamberComplex.pgalleryD_chamber
ChamberComplex.chamberD_simplex pgallery_chamber_system
folding_f.chamber_system_image
by    fastforce
hence "pgallery (𝗌⊨(C0#Cs))"
using pCs induced_automorphism_half_chamber_system_pgallery_map_f[of "C0#Cs"]
by    auto
moreover have "set (𝗌⊨(C0#Cs)) ⊆ g⊢𝒞"
proof-
have "set (𝗌⊨(C0#Cs)) ⊆ 𝗌⊢(𝒞-g⊢𝒞)"
using set_Cs flopped_half_chamber_systems_gf by auto
thus ?thesis
using bij_betw_imp_surj_on[
OF induced_automorphism_bij_between_half_chamber_systems_g
]
by    simp
qed
ultimately have "pgallery (𝗌⊨(𝗌⊨(C0#Cs)))"
using induced_automorphism_half_chamber_system_pgallery_map_g[
of "𝗌⊨(C0#Cs)"
]
by    auto
thus "pgallery ((𝗌∘𝗌)⊨(C0#Cs))"
using ssubst[OF setlistmapim_comp, of pgallery, of 𝗌 𝗌 "C0#Cs"] by fast
qed (unfold_locales, rule folding_f.chambersubcomplex_image)

lemmas indaut_selfcomp_halftriv_f =
induced_automorphism_selfcomp_halftrivial_f

lemma induced_automorphism_selfcomp_halftrivial_g: "fixespointwise (𝗌∘𝗌) (⋃(g⊢X))"
using induced_automorphism_fg_symmetric
OpposedThinChamberComplexFoldings.indaut_selfcomp_halftriv_f[
OF fg_symmetric
]
by    simp

lemma induced_automorphism_trivial_outside:
assumes "v∉⋃X"
shows   "𝗌 v = v"
proof-
from assms have "v ∉ f`(⋃X) ∧ v ∉ g`(⋃X)" using vertex_set_split by fast
thus "𝗌 v = v" using induced_automorphism_def by simp
qed

lemma induced_automorphism_morphism: "ChamberComplexEndomorphism X 𝗌"
proof (unfold_locales, rule induced_automorphism_chamber_map, simp)
fix C assume "chamber C"
thus "card (𝗌`C) = card C"
using induced_automorphism_chamber_image_fg folding_f.dim_map
folding_g.dim_map
flopped_half_chamber_systems_fg[THEN sym]
by    (cases "C∈f⊢𝒞") auto
qed (rule induced_automorphism_trivial_outside)

lemmas indaut_morph = induced_automorphism_morphism

lemma induced_automorphism_morphism_order2: "𝗌∘𝗌 = id"
proof
fix v
show "(𝗌∘𝗌) v = id v"
proof (cases "v∈f`(⋃X)" "v∈g`(⋃X)" rule: two_cases)
case both
from both(1) show ?thesis
using induced_automorphism_selfcomp_halftrivial_f fixespointwiseD[of "𝗌∘𝗌"]
by    auto
next
case one thus ?thesis
using induced_automorphism_selfcomp_halftrivial_f fixespointwiseD[of "𝗌∘𝗌"]
by    fastforce
next
case other thus ?thesis
using induced_automorphism_selfcomp_halftrivial_g fixespointwiseD[of "𝗌∘𝗌"]
by    fastforce
qed

lemmas indaut_order2 = induced_automorphism_morphism_order2

lemmas induced_automorphism_bij =
o_bij[OF
induced_automorphism_morphism_order2
induced_automorphism_morphism_order2
]

lemma induced_automorphism_surj_on_vertexset: "𝗌`(⋃X) = ⋃X"
proof
show "𝗌`(⋃X) ⊆ ⋃X"
using induced_automorphism_morphism
ChamberComplexEndomorphism.vertex_map
by    fast
hence "(𝗌∘𝗌)`(⋃X) ⊆ 𝗌`(⋃X)" by fastforce
thus "⋃X ⊆ 𝗌`(⋃X)" using induced_automorphism_morphism_order2 by simp
qed

lemma induced_automorphism_bij_betw_vertexset: "bij_betw 𝗌 (⋃X) (⋃X)"
using induced_automorphism_bij induced_automorphism_surj_on_vertexset
by    (auto intro: bij_betw_subset)

lemma induced_automorphism_surj_on_simplices: "𝗌⊢X = X"
proof
show "𝗌⊢X ⊆ X"
using induced_automorphism_morphism
ChamberComplexEndomorphism.simplex_map
by    fast
hence "𝗌⊢(𝗌⊢X) ⊆ 𝗌⊢X" by auto
thus "X ⊆ 𝗌⊢X"
setsetmapim_comp[THEN sym] induced_automorphism_morphism_order2
)
qed

lemma induced_automorphism_automorphism:
"ChamberComplexAutomorphism X 𝗌"
using induced_automorphism_chamber_map
ChamberComplexEndomorphism.dim_map
induced_automorphism_morphism
induced_automorphism_bij_betw_vertexset
induced_automorphism_surj_on_simplices
induced_automorphism_trivial_outside
by    (intro_locales, unfold_locales, fast)

lemmas indaut_aut = induced_automorphism_automorphism

lemma induced_automorphism_unique_automorphism':
assumes "ChamberComplexAutomorphism X s" "s≠id" "fixespointwise s (C0∩D0)"
shows   "fun_eq_on s 𝗌 C0"
proof (rule fun_eq_on_subset_and_diff_imp_eq_on)
from assms(3) show "fun_eq_on s 𝗌 (C0∩D0)"
using induced_automorphism_fixespointwise_C0_int_D0
fixespointwise2_imp_eq_on
by    fast
show "fun_eq_on s 𝗌 (C0 - (C0∩D0))"
proof (rule fun_eq_onI)
fix v assume v: "v ∈ C0 - C0∩D0"
with chambers(2) have C0_insert: "C0 = insert v (C0∩D0)"
hence "s`C0 = insert (s v) (s`(C0∩D0))" "𝗌`C0 = insert (𝗌 v) (𝗌`(C0∩D0))"
by auto
with assms(3)
have  insert: "s`C0 = insert (s v) (C0∩D0)" "D0 = insert (𝗌 v) (C0∩D0)"
using basechambers_half_chamber_systems
induced_automorphism_fixespointwise_C0_int_D0
induced_automorphism_simplex_image(1)

from chambers(2,3) have C0D0_C0: "(C0∩D0) ⊲ C0"
with assms(1) chambers(1) have "s`(C0∩D0) ⊲ s`C0"
using ChamberComplexAutomorphism.facet_map by fast
with assms(3) have C0D0_sC0: "(C0∩D0) ⊲ s`C0"
hence sv_nin_C0D0: "s v ∉ C0∩D0" using insert(1) facetrel_psubset by auto

from assms(1) chambers(1) have "chamber (s`C0)"
using ChamberComplexAutomorphism.chamber_map by fast
moreover from chambers(2,3) have C0D0_D0: "(C0∩D0) ⊲ D0"
ultimately have "s`C0 = C0 ∨ s`C0 = D0"
using chambers(1,3) chamber_D0 C0D0_C0 C0D0_sC0
facet_unique_other_chamber[of "s`C0" "C0∩D0" C0 D0]
by    auto
moreover have "¬ s`C0 = C0"
proof
assume sC0: "s`C0 = C0"
have "s = id"
proof (
rule standard_uniqueness_automorphs, rule assms(1),
rule trivial_automorphism, rule chambers(1),
rule fixespointwise_subset_and_diff_imp_eq_on,
rule Int_lower1, rule assms(3), rule fixespointwiseI
)
fix a assume "a ∈ C0-(C0∩D0)"
with v have "a = v" using C0_insert by fast
with sC0 show "s a = id a" using C0_insert sv_nin_C0D0 by auto
qed
with assms(1,2) show False by fast
qed
ultimately have sC0_D0: "s`C0 = D0" by fast

have "𝗌 v ∉ C0∩D0" using insert(2) C0D0_D0 facetrel_psubset by force
thus "s v = 𝗌 v" using insert sC0_D0 sv_nin_C0D0 by auto
qed
qed simp

lemma induced_automorphism_unique_automorphism:
"⟦ ChamberComplexAutomorphism X s; s≠id; fixespointwise s (C0∩D0) ⟧
⟹ s = 𝗌"
using chambers(1) induced_automorphism_unique_automorphism'
standard_uniqueness_automorphs induced_automorphism_automorphism
by    fastforce

lemmas indaut_uniq_aut =
induced_automorphism_unique_automorphism

lemma induced_automorphism_unique:
"OpposedThinChamberComplexFoldings X f' g' C0 ⟹ g'`C0 = g`C0 ⟹
OpposedThinChamberComplexFoldings.induced_automorphism X f' g' = 𝗌"
using induced_automorphism_automorphism induced_automorphism_ntrivial
induced_automorphism_fixespointwise_C0_int_D0
by    (auto intro:
OpposedThinChamberComplexFoldings.indaut_uniq_aut[
THEN sym
]
)

lemma induced_automorphism_sym:
"OpposedThinChamberComplexFoldings.induced_automorphism X g f = 𝗌"
using OpposedThinChamberComplexFoldings.indaut_aut[
OF fg_symmetric
]
OpposedThinChamberComplexFoldings.induced_automorphism_ntrivial[
OF fg_symmetric
]
OpposedThinChamberComplexFoldings.indaut_fixes_fundfacet[
OF fg_symmetric
]
induced_automorphism_unique_automorphism

lemma induced_automorphism_respects_labels:
assumes "label_wrt B φ" "v∈(⋃X)"
shows   "φ (𝗌 v) = φ v"
proof-
from assms(2) obtain C where "chamber C" "v∈C" using simplex_in_max by fast
with assms show ?thesis
induced_automorphism_on_chamber_vertices_f folding_f.respects_labels
folding_g.respects_labels
)
qed

lemmas indaut_resplabels =
induced_automorphism_respects_labels

end (* context OpposedThinChamberComplexFoldings *)

subsubsection ‹Walls›

text ‹
A pair of opposed foldings of a thin chamber complex defines a decomposition of the chamber
system into the two disjoint chamber system images. Call such a decomposition a wall, as we image
that disjointness erects a wall between the two half chamber systems. By considering the
collection of all possible opposed folding pairs, and their associated walls, we can obtain
information about minimality of galleries by considering the walls they cross.
›

context ThinChamberComplex
begin

definition foldpairs :: "(('a⇒'a) × ('a⇒'a)) set"
where "foldpairs ≡ {(f,g). ∃C. OpposedThinChamberComplexFoldings X f g C}"

abbreviation "walls ≡ ⋃(f,g)∈foldpairs. {{f⊢𝒞,g⊢𝒞}}"
abbreviation "the_wall_betw C D ≡
THE_default {} (λH. H∈walls ∧ separated_by H C D)"

definition walls_betw :: "'a set ⇒ 'a set ⇒ 'a set set set set"
where "walls_betw C D ≡ {H∈walls. separated_by H C D}"

fun wall_crossings :: "'a set list ⇒ 'a set set set list"
where "wall_crossings [] = []"
|     "wall_crossings [C] = []"
|     "wall_crossings (B#C#Cs) = the_wall_betw B C # wall_crossings (C#Cs)"

lemma foldpairs_sym: "(f,g)∈foldpairs ⟹ (g,f)∈foldpairs"
using foldpairs_def OpposedThinChamberComplexFoldings.fg_symmetric by fastforce

lemma not_self_separated_by_wall: "H∈walls ⟹ ¬ separated_by H C C"
using foldpairs_def OpposedThinChamberComplexFoldings.halfchsys_decomp(2)
not_self_separated_by_disjoint
by    force

lemma the_wall_betw_nempty:
assumes "the_wall_betw C D ≠ {}"
shows   "the_wall_betw C D ∈ walls" "separated_by (the_wall_betw C D) C D"
proof-
from assms have 1: "∃!H'∈walls. separated_by H' C D"
using THE_default_none[of "λH. H∈walls ∧ separated_by H C D" "{}"] by fast
show "the_wall_betw C D ∈ walls" "separated_by (the_wall_betw C D) C D"
using THE_defaultI'[OF 1] by auto
qed

lemma the_wall_betw_self_empty: "the_wall_betw C C = {}"
proof-
{
assume *: "the_wall_betw C C ≠ {}"
then obtain f g
where "(f,g)∈foldpairs" "the_wall_betw C C = {f⊢𝒞,g⊢𝒞}"
using the_wall_betw_nempty(1)[of C C]
by    blast
with * have False
using the_wall_betw_nempty(2)[of C C] foldpairs_def
OpposedThinChamberComplexFoldings.halfchsys_decomp(2)[
of X
]
not_self_separated_by_disjoint[of "f⊢𝒞" "g⊢𝒞"]
by    auto
}
thus ?thesis by fast
qed

lemma length_wall_crossings: "length (wall_crossings Cs) = length Cs - 1"
by (induct Cs rule: list_induct_CCons) auto

lemma wall_crossings_snoc:
"wall_crossings (Cs@[D,E]) = wall_crossings (Cs@[D]) @ [the_wall_betw D E]"
by (induct Cs rule: list_induct_CCons) auto

lemma wall_crossings_are_walls:
"H∈set (wall_crossings Cs) ⟹ H≠{} ⟹ H∈walls"
proof (induct Cs arbitrary: H rule: list_induct_CCons)
case (CCons B C Cs) thus ?case
using the_wall_betw_nempty(1)
by    (cases "H∈set (wall_crossings (C#Cs))") auto
qed auto

lemma in_set_wall_crossings_decomp:
"H∈set (wall_crossings Cs) ⟹
∃As A B Bs. Cs = As@[A,B]@Bs ∧ H = the_wall_betw A B"
proof (induct Cs rule: list_induct_CCons)
case (CCons C D Ds)
show ?case
proof (cases "H ∈ set (wall_crossings (D#Ds))")
case True
with CCons(1) obtain As A B Bs
where "C#(D#Ds) = (C#As)@[A,B]@Bs" "H = the_wall_betw A B"
by    fastforce
thus ?thesis by fast
next
case False
with CCons(2) have "C#(D#Ds) = []@[C,D]@Ds" "H = the_wall_betw C D"
by auto
thus ?thesis by fast
qed
qed auto

end (* context ThinChamberComplex *)

context OpposedThinChamberComplexFoldings
begin

lemma foldpair: "(f,g)∈foldpairs"
unfolding foldpairs_def
proof-
have "OpposedThinChamberComplexFoldings X f g C0" ..
thus "(f, g) ∈ {(f, g).
∃C. OpposedThinChamberComplexFoldings X f g C}"
by fast
qed

lemma separated_by_this_wall_fg:
"separated_by {f⊢𝒞,g⊢𝒞} C D ⟹ C∈f⊢𝒞 ⟹ D∈g⊢𝒞"
using separated_by_disjoint[
OF _ half_chamber_system_disjoint_union(2), of C D
]
by    fast

lemmas separated_by_this_wall_gf =
OpposedThinChamberComplexFoldings.separated_by_this_wall_fg[
OF fg_symmetric
]

lemma induced_automorphism_this_wall_vertex:
assumes "C∈f⊢𝒞" "D∈g⊢𝒞" "v∈C∩D"
shows   "𝗌 v = v"
proof-
from assms have "𝗌 v = g v"
using chamber_system_simplices induced_automorphism_on_simplices_fg
by    auto
with assms(2,3) show "𝗌 v = v"
using chamber_system_simplices folding_g.retraction by auto
qed

lemmas indaut_wallvertex =
induced_automorphism_this_wall_vertex

lemma unique_wall:
assumes opp'    : "OpposedThinChamberComplexFoldings X f' g' C'"
and     chambers: "A∈f⊢𝒞" "A∈f'⊢𝒞" "B∈g⊢𝒞" "B∈g'⊢𝒞" "A∼B"
shows   "{f⊢𝒞,g⊢𝒞} = {f'⊢𝒞,g'⊢𝒞}"
proof-
from chambers have B: "B=g`A" "B=g'`A"
OF opp'
]
by    auto
with chambers(1,2,5)
have  A : "OpposedThinChamberComplexFoldings X f g A"
and   A': "OpposedThinChamberComplexFoldings X f' g' A"
using switch_basechamber[of A]
OpposedThinChamberComplexFoldings.switch_basechamber[
OF opp', of A
]
by    auto
with B show ?thesis
using OpposedThinChamberComplexFoldings.unique_half_chamber_system_f[
OF A A'
]
OpposedThinChamberComplexFoldings.unique_half_chamber_system_g[
OF A A'
]
by    auto
qed

end (* context OpposedThinChamberComplexFoldings *)

context ThinChamberComplex
begin

lemma separated_by_wall_ex_foldpair:
assumes "H∈walls" "separated_by H C D"
shows   "∃(f,g)∈foldpairs. H = {f⊢𝒞,g⊢𝒞} ∧ C∈f⊢𝒞 ∧ D∈g⊢𝒞"
proof-
from assms(1) obtain f g where fg: "(f,g)∈foldpairs" "H = {f⊢𝒞,g⊢𝒞}" by auto
show ?thesis
proof (cases "C∈f⊢𝒞")
case True
moreover with fg assms(2) have "D∈g⊢𝒞"
using foldpairs_def
OpposedThinChamberComplexFoldings.separated_by_this_wall_fg[
of X f g _ C D
]
by    auto
ultimately show ?thesis using fg by auto
next
case False with assms(2) fg show ?thesis
using foldpairs_sym[of f g] separated_by_in_other[of "f⊢𝒞" "g⊢𝒞" C D] by auto
qed
qed

lemma not_separated_by_wall_ex_foldpair:
assumes chambers: "chamber C" "chamber D"
and     wall    : "H∈walls" "¬ separated_by H C D"
shows   "∃(f,g)∈foldpairs. H = {f⊢𝒞,g⊢𝒞} ∧ C∈f⊢𝒞 ∧ D∈f⊢𝒞"
proof-
from wall(1) obtain f g where fg: "(f,g)∈foldpairs" "H = {f⊢𝒞,g⊢𝒞}" by auto
from fg(1) obtain A where A: "OpposedThinChamberComplexFoldings X f g A"
using foldpairs_def by fast
from chambers have chambers': "C∈f⊢𝒞 ∨ C∈g⊢𝒞" "D∈f⊢𝒞 ∨ D∈g⊢𝒞"
using chamber_system_def
OpposedThinChamberComplexFoldings.halfchsys_decomp(1)[
OF A
]
by    auto
show ?thesis
proof (cases "C∈f⊢𝒞")
case True
moreover with chambers'(2) fg(2) wall(2) have "D∈f⊢𝒞"
unfolding separated_by_def by auto
ultimately show ?thesis using fg by auto
next
case False
with chambers'(1) have "C∈g⊢𝒞" by simp
moreover with chambers'(2) fg(2) wall(2) have "D∈g⊢𝒞"
using insert_commute[of "f⊢𝒞" "g⊢𝒞" "{}"] unfolding separated_by_def by auto
ultimately show ?thesis using fg foldpairs_sym[of f g] by auto
qed
qed

and     wall: "H0∈walls" "separated_by H0 C D"
shows "∃!H∈walls. separated_by H C D"
proof (rule ex1I, rule conjI, rule wall(1), rule wall(2))
fix H assume H: "H∈walls ∧ separated_by H C D"
from this obtain f g
where fg: "(f,g)∈foldpairs" "H={f⊢𝒞,g⊢𝒞}" "C∈f⊢𝒞" "D∈g⊢𝒞"
using separated_by_wall_ex_foldpair[of H C D]
by    auto
from wall obtain f0 g0
where f0g0: "(f0,g0)∈foldpairs" "H0={f0⊢𝒞,g0⊢𝒞}" "C∈f0⊢𝒞" "D∈g0⊢𝒞"
using separated_by_wall_ex_foldpair[of H0 C D]
by    auto
from fg(1) f0g0(1) obtain A A0
where A : "OpposedThinChamberComplexFoldings X f  g  A"
and   A0: "OpposedThinChamberComplexFoldings X f0 g0 A0"
using foldpairs_def
by    auto
from fg(2-4) f0g0(2-4) adj show "H = H0"
using OpposedThinChamberComplexFoldings.unique_wall[OF A0 A] by auto
qed

end (* context ThinChamberComplex *)

context OpposedThinChamberComplexFoldings
begin

lemma this_wall_betwI:
assumes "C∈f⊢𝒞" "D∈g⊢𝒞" "C∼D"
shows   "the_wall_betw C D = {f⊢𝒞,g⊢𝒞}"
have "OpposedThinChamberComplexFoldings X f g C0" ..
thus "{f⊢𝒞,g⊢𝒞}∈walls" using foldpairs_def by auto
moreover from assms(1,2) show "separated_by {f⊢𝒞,g⊢𝒞} C D"
by (auto intro: separated_byI)
ultimately show "{f⊢𝒞,g⊢𝒞}∈walls ∧ separated_by {f⊢𝒞,g⊢𝒞} C D" by simp
qed (rule assms(3))

lemma this_wall_betw_basechambers:
"the_wall_betw C0 D0 = {f⊢𝒞,g⊢𝒞}"
using basechambers_half_chamber_systems chambers(2) this_wall_betwI by auto

lemma this_wall_in_crossingsI_fg:
defines H: "H ≡ {f⊢𝒞,g⊢𝒞}"
assumes D: "D∈g⊢𝒞"
shows   "C∈f⊢𝒞 ⟹ gallery (C#Cs@[D]) ⟹ H ∈ set (wall_crossings (C#Cs@[D]))"
proof (induct Cs arbitrary: C)
case Nil
from Nil(1) assms have "H∈walls" "separated_by H C D"
using foldpair by (auto intro: separated_byI)
thus ?case
by    auto
next
case (Cons B Bs)
show ?case
proof (cases "B∈f⊢𝒞")
case True with Cons(1,3) show ?thesis using gallery_Cons_reduce by simp
next
case False
with Cons(2,3) H have "H∈walls" "separated_by H C B"
using galleryD_chamber[OF Cons(3)] chamber_in_other_half_fg[of B] foldpair
by    (auto intro: separated_byI)
thus ?thesis
by    auto
qed
qed

end (* context OpposedThinChamberComplexFoldings *)

lemma (in ThinChamberComplex) walls_betw_subset_wall_crossings:
assumes "gallery (C#Cs@[D])"
shows   "walls_betw C D ⊆ set (wall_crossings (C#Cs@[D]))"
proof
fix H assume "H ∈ walls_betw C D"
hence H: "H∈walls" "separated_by H C D" using walls_betw_def by auto
from this obtain f g
where fg: "(f,g)∈foldpairs" "H = {f⊢𝒞,g⊢𝒞}" "C∈f⊢𝒞" "D∈g⊢𝒞"
using separated_by_wall_ex_foldpair[of H C D]
by    auto
from fg(1) obtain Z where Z: "OpposedThinChamberComplexFoldings X f g Z"
using foldpairs_def by fast
from assms H(2) fg(2-4) show "H ∈ set (wall_crossings (C#Cs@[D]))"
using OpposedThinChamberComplexFoldings.this_wall_in_crossingsI_fg[OF Z]
by    auto
qed

context OpposedThinChamberComplexFoldings
begin

lemma same_side_this_wall_wall_crossings_not_distinct_f:
"gallery (C#Cs@[D]) ⟹ C∈f⊢𝒞 ⟹ D∈f⊢𝒞 ⟹
{f⊢𝒞,g⊢𝒞}∈set (wall_crossings (C#Cs@[D])) ⟹
¬ distinct (wall_crossings (C#Cs@[D]))"
proof (induct Cs arbitrary: C)
case Nil
hence "{f⊢𝒞,g⊢𝒞} = the_wall_betw C D" by simp
moreover hence "the_wall_betw C D ≠ {}" by fast
ultimately show ?case
using Nil(2,3) the_wall_betw_nempty(2) separated_by_this_wall_fg[of C D]
half_chamber_system_disjoint_union(2)
by    auto
next
case (Cons E Es)
show ?case
proof
assume 1: "distinct (wall_crossings (C # (E # Es) @ [D]))"
show False
proof (
cases "E∈f⊢𝒞" "{f⊢𝒞,g⊢𝒞} ∈ set (wall_crossings (E#Es@[D]))"
rule: two_cases
)
case both with Cons(1,2,4) 1 show False
using gallery_Cons_reduce by simp
next
case one
from one(2) Cons(5) have "{f⊢𝒞,g⊢𝒞} = the_wall_betw C E" by simp
moreover hence "the_wall_betw C E ≠ {}" by fast
ultimately show False
using Cons(3) one(1) the_wall_betw_nempty(2)
separated_by_this_wall_fg[of C E]
half_chamber_system_disjoint_union(2)
by    auto
next
case other with Cons(3) show False
using 1 galleryD_chamber[OF Cons(2)] galleryD_adj[OF Cons(2)]
chamber_in_other_half_fg this_wall_betwI
by    force
next
case neither
from Cons(2) neither(1) have "E∈g⊢𝒞"
using galleryD_chamber chamber_in_other_half_fg by auto
with Cons(4) have "separated_by {g⊢𝒞,f⊢𝒞} E D"
by (blast intro: separated_byI)
hence "{f⊢𝒞,g⊢𝒞} ∈ walls_betw E D"
using foldpair walls_betw_def by (auto simp add: insert_commute)
with neither(2) show False
using gallery_Cons_reduce[OF Cons(2)] walls_betw_subset_wall_crossings
by    auto
qed
qed
qed

lemmas sside_wcrossings_ndistinct_f =
same_side_this_wall_wall_crossings_not_distinct_f

lemma separated_by_this_wall_chain3_fg:
assumes "B∈f⊢𝒞" "chamber C" "chamber D"
"separated_by {f⊢𝒞,g⊢𝒞} B C" "separated_by {f⊢𝒞,g⊢𝒞} C D"
shows   "C∈g⊢𝒞" "D∈f⊢𝒞"
using   assms separated_by_this_wall_fg separated_by_this_wall_gf

lemmas sepwall_chain3_fg =
separated_by_this_wall_chain3_fg

end (* context OpposedThinChamberComplexFoldings *)

context ThinChamberComplex
begin

lemma wall_crossings_min_gallery_betwI:
assumes "gallery (C#Cs@[D])"
"distinct (wall_crossings (C#Cs@[D]))"
"∀H∈set (wall_crossings (C#Cs@[D])). separated_by H C D"
shows   "min_gallery (C#Cs@[D])"
proof (rule min_galleryI_betw)
obtain B Bs where BBs: "Cs@[D] = B#Bs" using snoc_conv_cons by fast
define H where "H = the_wall_betw C B"
with BBs assms(3) have 1: "separated_by H C D" by simp
show "C≠D"
proof (cases "H={}")
case True thus ?thesis
using 1 unfolding separated_by_def by simp
next
case False
with H_def have "H ∈ walls" using the_wall_betw_nempty(1) by simp
from this obtain f g
where fg: "(f,g)∈foldpairs" "H = {f⊢𝒞,g⊢𝒞}" "C∈f⊢𝒞" "D∈g⊢𝒞"
using 1 separated_by_wall_ex_foldpair[of H C D]
by    auto
thus ?thesis
using foldpairs_def
OpposedThinChamberComplexFoldings.halfchsys_decomp(2)[
of X f g
]
by    auto
qed
next
fix Ds assume Ds: "gallery (C # Ds @ [D])"
have "Suc (length Cs) = card (walls_betw C D)"
proof-
from assms(1,3) have "set (wall_crossings (C#Cs@[D])) = walls_betw C D"
using     separated_by_not_empty wall_crossings_are_walls[of _ "C#Cs@[D]"]
walls_betw_def
walls_betw_subset_wall_crossings[OF assms(1)]
unfolding separated_by_def
by        auto
with assms(2) show ?thesis
using distinct_card[THEN sym] length_wall_crossings by fastforce
qed
moreover have "card (walls_betw C D) ≤ Suc (length Ds)"
proof-
from Ds have "card (walls_betw C D) ≤ card (set (wall_crossings (C#Ds@[D])))"
using walls_betw_subset_wall_crossings finite_set card_mono by force
also have "… ≤ length (wall_crossings (C#Ds@[D]))"
using card_length by auto
finally show ?thesis using length_wall_crossings by simp
qed
ultimately show "length Cs ≤ length Ds" by simp
qed (rule assms(1))

lemma ex_nonseparating_wall_imp_wall_crossings_not_distinct:
assumes gal : "gallery (C#Cs@[D])"
and     wall: "H∈set (wall_crossings (C#Cs@[D]))" "H≠{}"
"¬ separated_by H C D"
shows   "¬ distinct (wall_crossings (C#Cs@[D]))"
proof-
from assms obtain f g
where fg: "(f,g)∈foldpairs" "H = {f⊢𝒞,g⊢𝒞}" "C∈f⊢𝒞" "D∈f⊢𝒞"
using wall_crossings_are_walls[of H]
not_separated_by_wall_ex_foldpair[of C D H]
galleryD_chamber
by    auto
from fg(1) obtain Z where Z: "OpposedThinChamberComplexFoldings X f g Z"
using foldpairs_def by fast
from wall fg(2-4) show ?thesis
using OpposedThinChamberComplexFoldings.sside_wcrossings_ndistinct_f [
OF Z gal
]
by    blast
qed

lemma not_min_gallery_double_crosses_wall:
assumes "gallery Cs" "¬ min_gallery Cs" "{} ∉ set (wall_crossings Cs)"
shows   "¬ distinct (wall_crossings Cs)"
proof (cases Cs rule: list_cases_Cons_snoc)
case Nil with assms(2) show ?thesis by simp
next
case Single with assms(1,2) show ?thesis using galleryD_chamber by simp
next
case (Cons_snoc B Bs C)
show ?thesis
proof (cases "B=C")
case True show ?thesis
proof (cases Bs)
case Nil with True Cons_snoc assms(3) show ?thesis
using the_wall_betw_self_empty by simp
next
case (Cons E Es)
define H where "H = the_wall_betw B E"
with Cons have *: "H ∈ set (wall_crossings (B#Bs@[C]))" by simp
moreover from assms(3) Cons_snoc * have "H ≠ {}" by fast
ultimately show ?thesis
using assms(1) Cons_snoc Cons True H_def
the_wall_betw_nempty(1)[of B E] not_self_separated_by_wall[of H B]
ex_nonseparating_wall_imp_wall_crossings_not_distinct[of B Bs C H]
by    fast
qed
next
case False
with assms Cons_snoc
have  1: "¬ distinct (wall_crossings Cs) ∨
¬ (∀H∈set (wall_crossings Cs). separated_by H B C)"
using wall_crossings_min_gallery_betwI
by    force
moreover {
assume "¬ (∀H∈set (wall_crossings Cs). separated_by H B C)"
from this obtain H
where H: "H∈set (wall_crossings Cs)" "¬ separated_by H B C"
by    auto
moreover from H(1) assms(3) have "H≠{}" by fast
ultimately have ?thesis
using assms(1) Cons_snoc
ex_nonseparating_wall_imp_wall_crossings_not_distinct
by    simp
}
ultimately show ?thesis by fast
qed
qed

lemma not_distinct_crossings_split_gallery:
"⟦ gallery Cs; {} ∉ set (wall_crossings Cs); ¬ distinct (wall_crossings Cs) ⟧ ⟹
∃f g As A B Bs E F Fs.
(f,g)∈foldpairs ∧ A∈f⊢𝒞 ∧ B∈g⊢𝒞 ∧ E∈g⊢𝒞 ∧ F∈f⊢𝒞 ∧
( Cs = As@[A,B,F]@Fs ∨ Cs = As@[A,B]@Bs@[E,F]@Fs )"
proof (induct Cs rule: list_induct_CCons)
case (CCons C J Js)
show ?case
proof (cases "distinct (wall_crossings (J#Js))")
case False
moreover from CCons(2) have "gallery (J#Js)"
using gallery_Cons_reduce by simp
moreover from CCons(3) have "{} ∉ set (wall_crossings (J#Js))" by simp
ultimately obtain f g As A B Bs E F Fs where split:
"(f,g)∈foldpairs" "A∈f⊢𝒞" "B∈g⊢𝒞" "E∈g⊢𝒞" "F∈f⊢𝒞"
"J#Js = As@[A,B,F]@Fs ∨ J#Js = As@[A,B]@Bs@[E,F]@Fs"
using CCons(1)
by    blast
from split(6)
have "C#J#Js = (C#As)@[A,B,F]@Fs ∨
C#J#Js = (C#As)@[A,B]@Bs@[E,F]@Fs"
by   simp
with split(1-5) show ?thesis by blast
next
case True
define H where "H = the_wall_betw C J"
with True CCons(4) have "H∈set (wall_crossings (J#Js))" by simp
from this obtain Bs E F Fs
where split1: "J#Js = Bs@[E,F]@Fs" "H = the_wall_betw E F"
using in_set_wall_crossings_decomp
by    fast
from H_def split1(2) CCons(3)
have  Hwall: "H ∈ walls" "separated_by H C J" "separated_by H E F"
using the_wall_betw_nempty[of C J] the_wall_betw_nempty[of E F]
by    auto
from Hwall(1,2) obtain f g
where fg: "(f,g)∈foldpairs" "H={f⊢𝒞,g⊢𝒞}" "C∈f⊢𝒞" "J∈g⊢𝒞"
using separated_by_wall_ex_foldpair[of H C J]
by    auto
from fg(1) obtain Z
where Z: "OpposedThinChamberComplexFoldings X f g Z"
using foldpairs_def
by    fast
show ?thesis
proof (cases Bs)
case Nil
with CCons(2) Hwall(2,3) fg(2-4) split1(1)
have "F∈f⊢𝒞" "C#J#Js = []@[C,J,F]@Fs"
using galleryD_chamber
OpposedThinChamberComplexFoldings.sepwall_chain3_fg(2)[
OF Z, of C J F
]
by    auto
with fg(1,3,4) show ?thesis by blast
next
case (Cons K Ks) have Bs: "Bs = K#Ks" by fact
show ?thesis
proof (cases "E∈f⊢𝒞")
case True
from CCons(2) split1(1) Bs have "gallery (J#Ks@[E])"
using gallery_Cons_reduce[of C "J#Ks@E#F#Fs"]
gallery_append_reduce1[of "J#Ks@[E]" "F#Fs"]
by    simp
with fg(4) True obtain Ls L M Ms
where LsLMMs: "L∈g⊢𝒞" "M∈f⊢𝒞" "J#Ks@[E] = Ls@L#M#Ms"
using OpposedThinChamberComplexFoldings.split_gallery_gf[
OF Z, of J E Ks
]
by    blast
show ?thesis
proof (cases Ls)
case Nil
with split1(1) Bs LsLMMs(3)
have "C#J#Js = []@[C,J,M]@(Ms@F#Fs)"
by   simp
with fg(1,3,4) LsLMMs(2) show ?thesis by blast
next
case (Cons N Ns)
with split1(1) Bs LsLMMs(3)
have "C#J#Js = []@[C,J]@Ns@[L,M]@(Ms@F#Fs)"
by   simp
with fg(1,3,4) LsLMMs(1,2) show ?thesis by blast
qed
next
case False
with Hwall(2,3) fg(2) split1(1) Cons
have  "E∈g⊢𝒞" "F∈f⊢𝒞" "C#J#Js = []@[C,J]@Ks@[E,F]@Fs"
using OpposedThinChamberComplexFoldings.separated_by_this_wall_fg[
OF Z
]
separated_by_in_other[of "f⊢𝒞" "g⊢𝒞"]
by    auto
with fg(1,3,4) show ?thesis by blast
qed
qed
qed
qed auto

lemma not_min_gallery_double_split:
"⟦ gallery Cs; ¬ min_gallery Cs; {} ∉ set (wall_crossings Cs) ⟧ ⟹
∃f g As A B Bs E F Fs.
(f,g)∈foldpairs ∧ A∈f⊢𝒞 ∧ B∈g⊢𝒞 ∧ E∈g⊢𝒞 ∧ F∈f⊢𝒞 ∧
( Cs = As@[A,B,F]@Fs ∨ Cs = As@[A,B]@Bs@[E,F]@Fs )"
using not_min_gallery_double_crosses_wall not_distinct_crossings_split_gallery
by    simp

end (* context ThinChamberComplex *)

subsection ‹Thin chamber complexes with many foldings›

text ‹
Here we begin to examine thin chamber complexes in which every pair of adjacent chambers affords a
pair of opposed foldings of the complex. This condition will ultimately be shown to be sufficient
to ensure that a thin chamber complex is isomorphic to some Coxeter complex.
›

subsubsection ‹Locale definition and basic facts›

locale ThinChamberComplexManyFoldings = ThinChamberComplex X
for   X  :: "'a set set"
+ fixes C0 :: "'a set"
assumes fundchamber: "chamber C0"
and     ex_walls   :
"⟦ chamber C; chamber D; C∼D; C≠D ⟧ ⟹
∃f g. OpposedThinChamberComplexFoldings X f g C ∧ D=g`C"

lemma (in ThinChamberComplex) ThinChamberComplexManyFoldingsI:
assumes "chamber C0"
and     "⋀C D. ⟦ chamber C; chamber D; C∼D; C≠D ⟧ ⟹
∃f g. OpposedThinChamberComplexFoldings X f g C ∧ D=g`C"
shows   "ThinChamberComplexManyFoldings X C0"
using   assms
by      (intro_locales, unfold_locales, fast)

lemma (in ThinChamberComplexManyFoldings) wall_crossings_subset_walls_betw:
assumes "min_gallery (C#Cs@[D])"
shows   "set (wall_crossings (C#Cs@[D])) ⊆ walls_betw C D"
proof
fix H assume "H ∈ set (wall_crossings (C#Cs@[D]))"
from this obtain As A B Bs
where H: "C#Cs@[D] = As@[A,B]@Bs" "H=the_wall_betw A B"
using in_set_wall_crossings_decomp
by    blast
from assms have pgal: "pgallery (C#Cs@[D])"
using min_gallery_pgallery by fast
with H(1) obtain f g
where fg: "OpposedThinChamberComplexFoldings X f g A" "B=g`A"
pgalleryD_distinct[of "As@[A,B]@Bs"] ex_walls[of A B]
by    auto
from H(2) fg have H': "A∈f⊢𝒞" "B∈g⊢𝒞" "H = {f⊢𝒞,g⊢𝒞}" "H∈walls"
using OpposedThinChamberComplexFoldings.basech_halfchsys[
OF fg(1)
]
OpposedThinChamberComplexFoldings.chambers(2)[OF fg(1)]
OpposedThinChamberComplexFoldings.this_wall_betwI[OF fg(1)]
foldpairs_def
by    auto
have CD: "C ∈ f⊢𝒞 ∪ g⊢𝒞" "D ∈ f⊢𝒞 ∪ g⊢𝒞"
using pgal pgalleryD_chamber chamber_system_def
OpposedThinChamberComplexFoldings.halfchsys_decomp(1)[
OF fg(1)
]
by    auto
show "H ∈ walls_betw C D"
proof (cases Bs As rule: two_lists_cases_snoc_Cons')
case both_Nil with H show ?thesis
using H'(3) the_wall_betw_nempty[of A B] unfolding walls_betw_def by force
next
case (Nil1 E Es)
show ?thesis
proof (cases "C∈f⊢𝒞")
case True
with Nil1 H(1) have "separated_by H C D"
using H'(2,3) by (auto intro: separated_byI)
thus ?thesis using H'(4) unfolding walls_betw_def by simp
next
case False with assms Nil1 H(1) show ?thesis
using OpposedThinChamberComplexFoldings.foldg[
OF fg(1)
]
CD(1) H'(1,2) pgal pgallery
OpposedThinChamberComplexFoldings.flopped_half_chamber_systems_gf[
OF fg(1)
]
ThinChamberComplexFolding.gallery_double_cross_not_minimal1[
of X g E A B Es "[]"
]
by    force
qed
next
case (Nil2 Fs F)
show ?thesis
proof (cases "D∈f⊢𝒞")
case True
with assms Nil2 H(1) show ?thesis
using OpposedThinChamberComplexFoldings.foldf[
OF fg(1)
]
H'(1,2) pgal pgallery
OpposedThinChamberComplexFoldings.flopped_half_chamber_systems_fg[
OF fg(1)
]
ThinChamberComplexFolding.gallery_double_cross_not_minimal_Cons1[
of X f
]
by    force
next
case False with Nil2 H(1) have "separated_by H C D"
using CD(2) H'(1,3) by (auto intro: separated_byI)
thus ?thesis using H'(4) unfolding walls_betw_def by simp
qed
next
case (snoc_Cons Fs F E Es) show ?thesis
proof (cases "C∈f⊢𝒞" "D∈g⊢𝒞" rule: two_cases)
case both thus ?thesis
using H'(3,4) walls_betw_def unfolding separated_by_def by auto
next
case one
with snoc_Cons assms H(1) show ?thesis
using OpposedThinChamberComplexFoldings.foldf[
OF fg(1)
]
CD(2) H'(2) pgal pgallery
OpposedThinChamberComplexFoldings.flopped_half_chamber_systems_fg[
OF fg(1)
]
ThinChamberComplexFolding.gallery_double_cross_not_minimal1[
of X f C B D "Es@[A]"
]
by    fastforce
next
case other
with snoc_Cons assms H(1) show ?thesis
using OpposedThinChamberComplexFoldings.ThinChamberComplexFolding_g[
OF fg(1)
]
CD(1) H'(1) pgal pgallery
OpposedThinChamberComplexFoldings.flopped_half_chamber_systems_gf[
OF fg(1)
]
ThinChamberComplexFolding.gallery_double_cross_not_minimal1[
of X g E A F Es "B#Fs"
]
by    force
next
case neither
hence "separated_by {g⊢𝒞,f⊢𝒞} C D" using CD by (auto intro: separated_byI)
thus ?thesis
using H'(3,4) walls_betw_def by (auto simp add: insert_commute)
qed
qed
qed

subsubsection ‹The group of automorphisms›

text ‹
Recall that a pair of opposed foldings of a thin chamber complex can be stitched together to form
an automorphism of the complex. Choosing an arbitrary chamber in the complex to act as a sort of
centre of the complex (referred to as the fundamental chamber), we consider the group (under
composition) generated by the automorphisms afforded by the chambers adjacent to the fundamental
chamber via the pairs of opposed foldings that we have assumed to exist.
›

context ThinChamberComplexManyFoldings
begin

definition fundfoldpairs :: "(('a⇒'a)×('a⇒'a)) set"
where "fundfoldpairs ≡ {(f,g). OpposedThinChamberComplexFoldings X f g C0}"

abbreviation induced_automorph :: "('a⇒'a) ⇒ ('a⇒'a) ⇒ ('a⇒'a)"
where "induced_automorph f g ≡
OpposedThinChamberComplexFoldings.induced_automorphism X f g"

abbreviation Abs_induced_automorph :: "('a⇒'a) ⇒ ('a⇒'a) ⇒ 'a permutation"
where "Abs_induced_automorph f g ≡ Abs_permutation (induced_automorph f g)"

abbreviation "S ≡ ⋃(f,g)∈fundfoldpairs. {Abs_induced_automorph f g}"
abbreviation "W ≡ ⟨S⟩"

lemma fundfoldpairs_induced_autormorph_bij:
"(f,g) ∈ fundfoldpairs ⟹ bij (induced_automorph f g)"
using     OpposedThinChamberComplexFoldings.induced_automorphism_bij
unfolding fundfoldpairs_def
by        fast

lemmas permutation_conv_induced_automorph =
Abs_permutation_inverse[OF CollectI, OF fundfoldpairs_induced_autormorph_bij]

lemma fundfoldpairs_induced_autormorph_order2:
"(f,g) ∈ fundfoldpairs ⟹ induced_automorph f g ∘ induced_automorph f g = id"
using     OpposedThinChamberComplexFoldings.indaut_order2
unfolding fundfoldpairs_def
by        fast

lemma fundfoldpairs_induced_autormorph_ntrivial:
"(f,g) ∈ fundfoldpairs ⟹ induced_automorph f g ≠ id"
using     OpposedThinChamberComplexFoldings.induced_automorphism_ntrivial
unfolding fundfoldpairs_def
by        fast

lemma fundfoldpairs_fundchamber_image:
"(f,g)∈fundfoldpairs ⟹ Abs_induced_automorph f g `→ C0 = g`C0"
using fundfoldpairs_def
permutation_conv_induced_automorph
OpposedThinChamberComplexFoldings.induced_automorphism_C0
)

lemma fundfoldpair_fundchamber_in_half_chamber_system_f:
"(f,g)∈fundfoldpairs ⟹ C0∈f⊢𝒞"
using fundfoldpairs_def
OpposedThinChamberComplexFoldings.basech_halfchsys(1)
by    fast

lemma fundfoldpair_unique_half_chamber_system_f:
assumes "(f,g)∈fundfoldpairs" "(f',g')∈fundfoldpairs"
"Abs_induced_automorph f' g' = Abs_induced_automorph f g"
shows   "f'⊢𝒞 = f⊢𝒞"
proof-
from assms have "g'`C0 = g`C0"
using fundfoldpairs_fundchamber_image[OF assms(1)]
fundfoldpairs_fundchamber_image[OF assms(2)]
by    simp
with assms show "f'⊢𝒞 = f⊢𝒞"
using fundfoldpairs_def
OpposedThinChamberComplexFoldings.unique_half_chamber_system_f[
of X f g C0 f' g'
]
by    auto
qed

lemma fundfoldpair_unique_half_chamber_systems_chamber_ng_f:
assumes "(f,g)∈fundfoldpairs" "(f',g')∈fundfoldpairs"
"Abs_induced_automorph f' g' = Abs_induced_automorph f g"
"chamber C" "C∉g⊢𝒞"
shows   "C∈f'⊢𝒞"
using assms(1,3-5) fundfoldpairs_def chamber_system_def
OpposedThinChamberComplexFoldings.flopped_half_chamber_systems_gf[
THEN sym
]
fundfoldpair_unique_half_chamber_system_f[OF assms(1,2)]
by    fastforce

"(f,g)∈fundfoldpairs ⟹
the_wall_betw C0 (Abs_induced_automorph f g `→ C0) = {f⊢𝒞,g⊢𝒞}"
using fundfoldpairs_def
OpposedThinChamberComplexFoldings.this_wall_betw_basechambers
OpposedThinChamberComplexFoldings.induced_automorphism_C0

lemma zero_notin_S: "0∉S"
proof
assume "0∈S"
from this obtain f g
where "(f,g)∈fundfoldpairs" "0 = Abs_induced_automorph f g"
by    fast
thus False
using Abs_permutation_inject[of id "induced_automorph f g"]
bij_id fundfoldpairs_induced_autormorph_bij
fundfoldpairs_induced_autormorph_ntrivial
qed

lemma S_order2_add: "s∈S ⟹ s + s = 0"
using fundfoldpairs_induced_autormorph_bij zero_permutation.abs_eq
plus_permutation_abs_eq fundfoldpairs_induced_autormorph_order2
)

assumes "s∈S"
from assms show "s+^2 = 0" using S_order2_add by (simp add: nataction_2)
next
fix m assume "0 < m" "s+^m = 0"
with assms show "2 ≤ m" using zero_notin_S by (cases "m=1") auto
qed simp

lemma S_sym: "uminus ` S ⊆ S"
using S_uminus by auto

lemmas sum_list_S_in_W  = sum_list_lists_in_genby_sym[OF S_sym]
lemmas W_conv_sum_lists = genby_sym_eq_sum_lists[OF S_sym]

lemma S_endomorphism:
"s∈S ⟹ ChamberComplexEndomorphism X (permutation s)"
using fundfoldpairs_def
OpposedThinChamberComplexFoldings.induced_automorphism_morphism

lemma S_list_endomorphism:
"ss∈lists S ⟹ ChamberComplexEndomorphism X (permutation (sum_list ss))"
by  (induct ss)
zero_permutation.rep_eq trivial_endomorphism plus_permutation.rep_eq
S_endomorphism ChamberComplexEndomorphism.endo_comp
)

lemma W_endomorphism:
"w∈W ⟹ ChamberComplexEndomorphism X (permutation w)"
using W_conv_sum_lists S_list_endomorphism by auto

lemma S_automorphism:
"s∈S ⟹ ChamberComplexAutomorphism X (permutation s)"
using fundfoldpairs_def
OpposedThinChamberComplexFoldings.induced_automorphism_automorphism

lemma S_list_automorphism:
"ss∈lists S ⟹ ChamberComplexAutomorphism X (permutation (sum_list ss))"
by  (induct ss)
zero_permutation.rep_eq trivial_automorphism plus_permutation.rep_eq
S_automorphism ChamberComplexAutomorphism.comp
)

lemma W_automorphism:
"w∈W ⟹ ChamberComplexAutomorphism X (permutation w)"
using W_conv_sum_lists S_list_automorphism by auto

lemma S_respects_labels: "⟦ label_wrt B φ; s∈S; v∈(⋃X) ⟧ ⟹ φ (s → v) = φ v"
using fundfoldpairs_def
OpposedThinChamberComplexFoldings.indaut_resplabels[
of X _ _ C0 B φ v
]

lemma S_list_respects_labels:
"⟦ label_wrt B φ; ss∈lists S; v∈(⋃X) ⟧ ⟹ φ (sum_list ss → v) = φ v"
using S_endomorphism ChamberComplexEndomorphism.vertex_map[of X]
by    (induct ss arbitrary: v rule: rev_induct)
plus_permutation.rep_eq S_respects_labels zero_permutation.rep_eq
)

lemma W_respects_labels:
"⟦ label_wrt B φ; w∈W; v∈(⋃X) ⟧ ⟹ φ (w→v) = φ v"
using W_conv_sum_lists S_list_respects_labels[of B φ _ v] by auto

end (* context ThinChamberComplexManyFoldings *)

subsubsection ‹Action of the group of automorphisms on the chamber system›

text ‹
Now we examine the action of the group @{term W} on the chamber system. In particular, we show
that the action is transitive.
›

context ThinChamberComplexManyFoldings
begin

lemma fundchamber_S_chamber: "s∈S ⟹ chamber (s`→C0)"
using fundfoldpairs_def
fundfoldpairs_fundchamber_image
OpposedThinChamberComplexFoldings.chamber_D0
)

lemma fundchamber_W_image_chamber:
"w∈W ⟹ chamber (w`→C0)"
using fundchamber W_endomorphism
ChamberComplexEndomorphism.chamber_map
by    auto

lemma fundchamber_S_adjacent: "s∈S ⟹ C0 ∼ (s`→C0)"
using fundfoldpairs_def
fundfoldpairs_fundchamber_image
OpposedThinChamberComplexFoldings.chambers(2)
)

"w∈W ⟹ s∈S ⟹ (w`→C0) ∼ ((w+s)`→C0)"
W_endomorphism
ChamberComplexEndomorphism.adj_map[of X "permutation w" C0 "s`→C0"]
by    (auto simp add: image_comp plus_permutation.rep_eq)

lemma fundchamber_S_image_neq_fundchamber: "s∈S ⟹ s`→C0 ≠ C0"
using fundfoldpairs_def OpposedThinChamberComplexFoldings.chambers(3)

lemma fundchamber_next_WS_image_neq:
assumes "s∈S"
shows   "(w+s) `→ C0 ≠ w `→ C0"
proof
assume "(w+s) `→ C0 = w `→ C0"
with assms show False
using fundchamber_S_image_neq_fundchamber[of s]
by    (auto simp add: plus_permutation.rep_eq image_comp permutation_eq_image)
qed

by    simp

fundfoldpairs_def fundfoldpairs_fundchamber_image
by    blast

lemma S_fixespointwise_fundchamber_image_int:
assumes "s∈S"
shows   "fixespointwise ((→) s) (C0∩s`→C0)"
proof-
from assms(1) obtain f g
where fg: "(f,g)∈fundfoldpairs" "s = Abs_induced_automorph f g"
by    fast
show ?thesis
proof (rule fixespointwise_cong)
from fg show "fun_eq_on ((→) s) (induced_automorph f g) (C0∩s`→C0)"
using permutation_conv_induced_automorph fun_eq_onI by fastforce
from fg show "fixespointwise (induced_automorph f g) (C0∩s`→C0)"
using fundfoldpairs_fundchamber_image fundfoldpairs_def
OpposedThinChamberComplexFoldings.indaut_fixes_fundfacet
by    auto
qed
qed

lemma S_fixes_fundchamber_image_int:
"s∈S ⟹ s`→(C0∩s`→C0) = C0∩s`→C0"
using fixespointwise_im[OF S_fixespointwise_fundchamber_image_int] by simp

lemma fundfacets:
assumes "s∈S"
shows   "C0∩s`→C0 ⊲ C0" "C0∩s`→C0 ⊲ s`→C0"
fundchamber_S_image_neq_fundchamber[of s]
by      auto

shows   "∃!s∈S. D = s`→C0"
proof (rule ex_ex1I)
from assms show "∃s. s∈S ∧ D = s `→ C0"
next
fix s t assume "s∈S ∧ D = s`→C0" "t∈S ∧ D = t`→C0"
hence s: "s∈S" "D = s`→C0"
and t: "t∈S" "D = t`→C0"
by  auto
from s(1) t(1) obtain f g f' g'
where "(f,g)∈fundfoldpairs" "s = Abs_induced_automorph f  g"
and   "(f',g')∈fundfoldpairs" "t = Abs_induced_automorph f' g'"
by    auto
with s(2) t(2) show "s=t"
using fundfoldpairs_def fundfoldpairs_fundchamber_image
OpposedThinChamberComplexFoldings.induced_automorphism_unique[
of X f' g' C0 f g
]
by    auto
qed

lemma fundchamber_S_image_inj_on: "inj_on (λs. s`→C0) S"
proof (rule inj_onI)
fix s t assume "s∈S" "t∈S" "s`→C0 = t`→C0" thus "s=t"
bex1_equality[OF fundadjset_ex1_eq_S_image, of "s`→C0" s t]
by    simp
qed

lemma S_list_image_gallery:
"ss∈lists S ⟹ gallery (map (λw. w`→C0) (sums ss))"
proof (induct ss rule: list_induct_ssnoc)
case (Single s) thus ?case
gallery_def
next
case (ssnoc ss s t)
define Cs D E where "Cs = map (λw. w `→ C0) (sums ss)"
and "D = sum_list (ss@[s]) `→ C0"
and "E = sum_list (ss@[s,t]) `→ C0"
with ssnoc have "gallery (Cs@[D,E])"
using sum_list_S_in_W[of "ss@[s,t]"] sum_list_S_in_W[of "ss@[s]"]
fundchamber_W_image_chamber
sum_list_append[of "ss@[s]" "[t]"]
by    (auto intro: gallery_snocI simp add: sums_snoc)
with Cs_def D_def E_def show ?case using sums_snoc[of "ss@[s]" t] by (simp add: sums_snoc)
qed (auto simp add: gallery_def fundchamber zero_permutation.rep_eq)

lemma pgallery_last_eq_W_image:
"pgallery (C0#Cs@[C]) ⟹ ∃w∈W. C = w`→C0"
proof (induct Cs arbitrary: C rule: rev_induct)
case Nil
using pgallery_def chamberD_simplex adjacentset_def by fastforce
from this obtain s where "s∈S" "C = s`→C0"
thus ?case using genby_genset_closed[of s S] by fast
next
case (snoc D Ds)
have DC: "chamber D" "chamber C" "D∼C" "D≠C"
using pgallery_def snoc(2)
by    auto
from snoc obtain w where w: "w∈W" "D = w`→C0"
using pgallery_append_reduce1[of "C0#Ds@[D]" "[C]"] by force
from w(2) have "(-w)`→D = C0"
image_comp plus_permutation.rep_eq[THEN sym]
zero_permutation.rep_eq
)
with DC w(1) have "C0 ∼ (-w)`→C" "C0 ≠ (-w)`→C" "(-w)`→C ∈ X"
using genby_uminus_closed W_endomorphism[of "-w"]
permutation_eq_image[of "-w" D] chamberD_simplex[of C]
ChamberComplexEndomorphism.simplex_map[of X "permutation (-w)" C]
by    auto
from this obtain s where s: "s∈S" "(-w)`→C = s`→C0"
from s(2) have
"(permutation w ∘ permutation (-w))`C = (permutation w ∘ permutation s)`C0"
hence "C = (w+s)`→C0"
by (simp add: plus_permutation.rep_eq[THEN sym] zero_permutation.rep_eq)
with w(1) s(1) show ?case
using genby_genset_closed[of s S] genby_add_closed by blast
qed

lemma chamber_eq_W_image:
assumes "chamber C"
shows   "∃w∈W. C = w`→C0"
proof (cases "C=C0")
case True
hence "0∈W" "C = 0`→C0"
using genby_0_closed by (auto simp add: zero_permutation.rep_eq)
thus ?thesis by fast
next
case False with assms show ?thesis
using fundchamber chamber_pconnect pgallery_last_eq_W_image by blast
qed

lemma S_list_image_crosses_walls:
"ss ∈ lists S ⟹ {} ∉ set (wall_crossings (map (λw. w`→C0) (sums ss)))"
proof (induct ss rule: list_induct_ssnoc)
case (Single s) thus ?case
fundchamber_S_image_neq_fundchamber[of s] ex_walls[of C0 "s`→C0"]
OpposedThinChamberComplexFoldings.this_wall_betw_basechambers
next
case (ssnoc ss s t)
moreover
define A B where "A = sum_list (ss@[s]) `→ C0" and "B = sum_list (ss@[s,t]) `→ C0"
moreover from ssnoc(2) A_def B_def obtain f g
where "OpposedThinChamberComplexFoldings X f g A" "B=g`A"
using sum_list_S_in_W[of "ss@[s]"] sum_list_S_in_W[of "ss@[s,t]"]
fundchamber_W_image_chamber sum_list_append[of "ss@[s]" "[t]"]
fundchamber_next_WS_image_neq[of t "sum_list (ss@[s])"]
ex_walls[of A B]
by    auto
ultimately show ?case
using OpposedThinChamberComplexFoldings.this_wall_betw_basechambers
sums_snoc[of "ss@[s]" t]
by    (force simp add: sums_snoc wall_crossings_snoc)

end (* context ThinChamberComplexManyFoldings *)

subsubsection ‹A labelling by the vertices of the fundamental chamber›

text ‹
Here we show that by repeatedly applying the composition of all the elements in the collection
@{term S} of fundamental automorphisms, we can retract the entire chamber complex onto the
fundamental chamber. This retraction provides a means of labelling the chamber complex, using the
vertices of the fundamental chamber as labels.
›

context ThinChamberComplexManyFoldings
begin

definition Spair :: "'a permutation ⇒ ('a⇒'a)×('a⇒'a)"
where "Spair s ≡
SOME fg. fg ∈ fundfoldpairs ∧ s = case_prod Abs_induced_automorph fg"

lemma Spair_fundfoldpair: "s∈S ⟹ Spair s ∈ fundfoldpairs"
using Spair_def
someI_ex[of
"λfg. fg ∈ fundfoldpairs ∧
s = case_prod Abs_induced_automorph fg"
]
by    auto

lemma Spair_induced_automorph:
"s∈S ⟹ s = case_prod Abs_induced_automorph (Spair s)"
using Spair_def
someI_ex[of
"λfg. fg ∈ fundfoldpairs ∧
s = case_prod Abs_induced_automorph fg"
]
by    auto

lemma S_list_pgallery_decomp1:
assumes ss: "set ss = S" and gal: "Cs≠[]" "pgallery (C0#Cs)"
shows   "∃s∈set ss. ∃C∈set Cs. ∀(f,g)∈fundfoldpairs.
s = Abs_induced_automorph f g ⟶ C ∈ g⊢𝒞"
proof (cases Cs)
case (Cons D Ds)
using pgallery_def chamberD_simplex adjacentset_def by fastforce
from this obtain s where s: "s∈S" "D = s`→C0"
from s(2) have
"∀(f,g)∈fundfoldpairs. s = Abs_induced_automorph f g ⟶ D∈g⊢𝒞"
using fundfoldpairs_def fundfoldpairs_fundchamber_image
OpposedThinChamberComplexFoldings.basechambers_half_chamber_systems(2)
by    auto
with s(1) ss Cons show ?thesis by auto

lemma S_list_pgallery_decomp2:
assumes "set ss = S" "Cs≠[]" "pgallery (C0#Cs)"
shows
"∃rs s ts. ss = rs@s#ts ∧
(∃C∈set Cs. ∀(f,g)∈fundfoldpairs.
s = Abs_induced_automorph f g ⟶ C ∈ g⊢𝒞) ∧
(∀r∈set rs. ∀C∈set Cs. ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ C∈f⊢𝒞)"
proof-
from assms obtain rs s ts  where rs_s_ts:
"ss = rs@s#ts"
"∃C∈set Cs. ∀(f,g)∈fundfoldpairs.
s = Abs_induced_automorph f g ⟶ C ∈ g⊢𝒞"
"∀r∈set rs. ∀C∈set Cs.
¬ (∀(f,g)∈fundfoldpairs. r = Abs_induced_automorph f g ⟶ C ∈ g⊢𝒞)"
using split_list_first_prop[OF S_list_pgallery_decomp1, of ss Cs]
by    auto
have "∀r∈set rs. ∀C∈set Cs. ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ C∈f⊢𝒞"
proof (rule ballI, rule ballI, rule prod_ballI, rule impI)
fix r C f g
assume  "r ∈ set rs" "C ∈ set Cs" "(f,g)∈fundfoldpairs"
"r = Abs_induced_automorph f g"
with rs_s_ts(3) assms(3) show "C∈f⊢𝒞"
using pgalleryD_chamber
fundfoldpair_unique_half_chamber_systems_chamber_ng_f[
of _ _ f g C
]
by    fastforce
qed
with rs_s_ts(1,2) show ?thesis by auto
qed

lemma S_list_pgallery_decomp3:
assumes "set ss = S" "Cs≠[]" "pgallery (C0#Cs)"
shows
"∃rs s ts As B Bs. ss = rs@s#ts ∧ Cs = As@B#Bs ∧
(∀(f,g)∈fundfoldpairs. s = Abs_induced_automorph f g ⟶ B∈g⊢𝒞) ∧
(∀A∈set As. ∀(f,g)∈fundfoldpairs.
s = Abs_induced_automorph f g ⟶ A∈f⊢𝒞) ∧
(∀r∈set rs. ∀C∈set Cs. ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ C∈f⊢𝒞)"
proof-
from assms obtain rs s ts where rs_s_ts:
"ss = rs@s#ts"
"∃B∈set Cs. ∀(f,g)∈fundfoldpairs. s = Abs_induced_automorph f g ⟶ B ∈ g⊢𝒞"
"∀r∈set rs. ∀B∈set Cs. ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ B∈f⊢𝒞"
using S_list_pgallery_decomp2[of ss Cs]
by    auto
obtain As B Bs where As_B_Bs:
"Cs = As@B#Bs"
"∀(f,g)∈fundfoldpairs. s = Abs_induced_automorph f g ⟶ B ∈ g⊢𝒞"
"∀A∈set As. ∃(f,g)∈fundfoldpairs. s = Abs_induced_automorph f g ∧ A∉g⊢𝒞"
using split_list_first_prop[OF rs_s_ts(2)]
by    fastforce
from As_B_Bs(1,3) assms(3)
have "∀A∈set As. ∀(f,g)∈fundfoldpairs.
s = Abs_induced_automorph f g ⟶ A∈f⊢𝒞"
using pgalleryD_chamber
fundfoldpair_unique_half_chamber_systems_chamber_ng_f
by    auto
with rs_s_ts(1,3) As_B_Bs(1,2) show ?thesis by fast
qed

lemma fundfold_trivial_f𝒞:
"r∈S ⟹ ∀(f,g)∈fundfoldpairs. r = Abs_induced_automorph f g ⟶ C∈f⊢𝒞 ⟹
fst (Spair r) ` C = C"
using Spair_fundfoldpair[of r] Spair_induced_automorph[of r] fundfoldpairs_def
OpposedThinChamberComplexFoldings.axioms(2)[
of X "fst (Spair r)" "snd (Spair r)" C0
]
ChamberComplexFolding.chamber_retraction2[of X "fst (Spair r)" C]
by    fastforce

lemma fundfold_comp_trivial_f𝒞:
"set rs ⊆ S ⟹
∀r∈set rs. ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ C∈f⊢𝒞 ⟹
fold fst (map Spair rs) ` C = C"
proof (induct rs)
case (Cons r rs)
have "fold fst (map Spair (r#rs)) ` C =
fold fst (map Spair rs) ` fst (Spair r) ` C"
also from Cons have "… = C" by (simp add: fundfold_trivial_f𝒞)
finally show ?case by fast
qed simp

lemma fundfold_trivial_f𝒞_list:
"r∈S ⟹
∀C∈set Cs. ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ C∈f⊢𝒞 ⟹
fst (Spair r) ⊨ Cs = Cs"
using fundfold_trivial_f𝒞 by (induct Cs) auto

lemma fundfold_comp_trivial_f𝒞_list:
"set rs ⊆ S ⟹
∀r∈set rs. ∀C∈set Cs. ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ C∈f⊢𝒞 ⟹
fold fst (map Spair rs) ⊨ Cs = Cs"
proof (induct rs Cs rule: list_induct2')
case (4 r rs C Cs)
from 4(3)
have  r: "∀D∈set (C#Cs). ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ D∈f⊢𝒞"
by    simp
from 4(2)
have  "fold fst (map Spair (r#rs)) ⊨ (C#Cs) =
map ((`) (fold fst (map Spair rs))) (fst (Spair r) ⊨ (C#Cs))"
also from 4 have "… = C#Cs"
using fundfold_trivial_f𝒞_list[of r "C#Cs"]
finally show ?case by fast
qed auto

lemma fundfold_gallery_map:
"s∈S ⟹ gallery Cs ⟹ gallery (fst (Spair s) ⊨ Cs)"
using Spair_fundfoldpair fundfoldpairs_def
OpposedThinChamberComplexFoldings.axioms(2)
ChamberComplexFolding.gallery_map[of X "fst (Spair s)"]
by    fastforce

lemma fundfold_comp_gallery_map:
assumes pregal: "gallery Cs"
shows   "set ss ⊆ S ⟹ gallery (fold fst (map Spair ss) ⊨ Cs)"
proof (induct ss rule: rev_induct)
case (snoc s ss)
hence 1: "gallery (fst (Spair s) ⊨ (fold fst (map Spair ss) ⊨ Cs))"
using fundfold_gallery_map by fastforce
have 2: "fst (Spair s) ⊨ (fold fst (map Spair ss) ⊨ Cs) =
fold fst (map Spair (ss@[s])) ⊨ Cs"
show ?case using 1 subst[OF 2, of gallery, OF 1] by fast

lemma fundfold_comp_pgallery_ex_funpow:
assumes ss: "set ss = S"
shows   "pgallery (C0#Cs@[C]) ⟹
∃n. (fold fst (map Spair ss) ^^ n) ` C = C0"
proof (induct Cs arbitrary: C rule: length_induct)
fix Cs C
assume step  :  "∀ys. length ys < length Cs ⟶
(∀x. pgallery (C0 # ys @ [x]) ⟶
(∃n. (fold fst (map Spair ss) ^^ n) ` x = C0))"
and  set_up:  "pgallery (C0#Cs@[C])"
from ss set_up obtain rs s ts As B Bs where decomps:
"ss = rs@s#ts" "Cs@[C] = As@B#Bs"
"∀(f,g)∈fundfoldpairs. s = Abs_induced_automorph f g ⟶ B∈g⊢𝒞"
"∀A∈set As. ∀(f,g)∈fundfoldpairs. s = Abs_induced_automorph f g ⟶ A∈f⊢𝒞"
"∀r∈set rs. ∀D∈set (Cs@[C]). ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ D∈f⊢𝒞"
using S_list_pgallery_decomp3[of ss "Cs@[C]"]
by    fastforce
obtain Es E where EsE: "C0#As = Es@[E]" using cons_conv_snoc by fast

have EsE_s_f𝒞:
"∀A∈set (Es@[E]). ∀(f,g)∈fundfoldpairs.
s = Abs_induced_automorph f g ⟶ A∈f⊢𝒞"
proof (rule ballI)
fix A assume "A∈set (Es@[E])"
with EsE decomps(4)
show  "∀(f, g)∈fundfoldpairs. s = Abs_induced_automorph f g ⟶ A ∈ f ⊢ 𝒞"
using fundfoldpair_fundchamber_in_half_chamber_system_f
set_ConsD[of A C0 As]
by    auto
qed
moreover from decomps(2) EsE
have  decomp2: "C0#Cs@[C] = Es@E#B#Bs"
by    simp
moreover from ss decomps(1) have "s∈S" by auto
ultimately have sB: "fst (Spair s) ` B = E"
using set_up decomps(3) Spair_fundfoldpair[of s]
Spair_induced_automorph[of s] fundfoldpairs_def
of X "fst (Spair s)" "snd (Spair s)" C0 E B
]
by    auto

show "∃n. (fold fst (map Spair ss) ^^ n) ` C = C0"
proof (cases "Es=[] ∧ Bs = []")
case True
from decomps(5) have
"∀r∈set rs. ∀(f,g)∈fundfoldpairs. r = Abs_induced_automorph f g ⟶ C∈f⊢𝒞"
by auto
with decomps(1) ss
have  "fold fst (map Spair ss) ` C = fold fst (map Spair ts) ` fst (Spair s) ` C"
using fundfold_comp_trivial_f𝒞[of rs C]
by    (fastforce simp add: image_comp[THEN sym])
moreover
have  "∀r∈set ts. ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ C0∈f⊢𝒞"
using fundfoldpair_fundchamber_in_half_chamber_system_f
by    fast
ultimately have "(fold fst (map Spair ss) ^^ 1) ` C = C0"
using True decomps(1,2) ss EsE sB fundfold_comp_trivial_f𝒞[of ts C0]
fundfold_comp_trivial_f𝒞[of ts C0]
by    fastforce
thus ?thesis by fast
next
case False have EsBs: "¬ (Es = [] ∧ Bs = [])" by fact
show ?thesis
proof (cases "fold fst (map Spair ss) ` C = C0")
case True
hence "(fold fst (map Spair ss) ^^ 1) ` C = C0" by simp
thus ?thesis by fast
next
case False
from decomps(5) have C0CsC_rs_f𝒞:
"∀r∈set rs. ∀D∈set (C0#Cs@[C]). ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ D∈f⊢𝒞"
using fundfoldpair_fundchamber_in_half_chamber_system_f
by    auto
from decomps(1)
have  "fold fst (map Spair (rs@[s])) ⊨ (C0#Cs@[C]) =
fst (Spair s) ⊨ (fold fst (map Spair rs) ⊨ (C0#Cs@[C]))"
also from ss decomps(1)
have  "… =  fst (Spair s) ⊨ (C0#Cs@[C])"
using C0CsC_rs_f𝒞 fundfold_comp_trivial_f𝒞_list[of rs "C0#Cs@[C]"]
by    fastforce
also from decomp2 have "… =  fst (Spair s) ⊨ (Es@E#B#Bs)"
finally
have  "fold fst (map Spair (rs@[s])) ⊨ (C0#Cs@[C]) =
Es @ E # E # fst (Spair s) ⊨ Bs"
using decomps(1) ss sB EsE_s_f𝒞 fundfold_trivial_f𝒞_list[of s "Es@[E]"]
by    fastforce
with set_up ss decomps(1)
have  gal: "gallery (Es @ E # fst (Spair s) ⊨ Bs)"
using pgallery fundfold_comp_gallery_map[of _ "rs@[s]"]
gallery_remdup_adj[of Es E "fst (Spair s) ⊨ Bs"]
by    fastforce

from EsBs decomp2 EsE
have  "∃Zs. length Zs < length Cs ∧
Es @ E # fst (Spair s) ⊨ Bs = C0 # Zs @ [fst (Spair s) ` C]"
using sB
by    (cases Bs Es rule: two_lists_cases_snoc_Cons') auto
from this obtain Zs where Zs:
"length Zs < length Cs"
"Es @ E # fst (Spair s) ⊨ Bs = C0 # Zs @ [fst (Spair s) ` C]"
by fast
define Ys where "Ys = fold fst (map Spair ts) ⊨ Zs"
with Zs(2) have
"fold fst (map Spair ts) ⊨ (Es @ E # fst (Spair s) ⊨ Bs) =
fold fst (map Spair ts) ` C0 # Ys @ [fold fst (map Spair (s#ts)) ` C]"
moreover
have  "∀r∈set ts. ∀(f,g)∈fundfoldpairs.
r = Abs_induced_automorph f g ⟶ C0∈f⊢𝒞"
using fundfoldpair_fundchamber_in_half_chamber_system_f
by    fast
ultimately have
"fold fst (map Spair ts) ⊨ (Es @ E # fst (Spair s) ⊨ Bs) =
C0 # Ys @ [fold fst (map Spair (s#ts)) ` fold fst (map Spair rs) ` C]"
using decomps(1) ss C0CsC_rs_f𝒞 fundfold_comp_trivial_f𝒞[of ts C0]
fundfold_comp_trivial_f𝒞[of rs C]
by    fastforce
with decomps(1) ss obtain Xs where Xs:
"length Xs ≤ length Ys"
"pgallery (C0 # Xs @ [fold fst (map Spair ss) ` C])"
using gal fundfold_comp_gallery_map[of "Es @ E # fst (Spair s) ⊨ Bs" ts]
gallery_obtain_pgallery[OF False[THEN not_sym]]
from Ys_def Xs(1) Zs(1) have "length Xs < length Cs" by simp
with Xs(2) obtain n where "(fold fst (map Spair ss) ^^ (Suc n)) ` C = C0"
using step by (force simp add: image_comp funpow_Suc_right[THEN sym])
thus ?thesis by fast
qed
qed

qed

lemma fundfold_comp_chamber_ex_funpow:
assumes ss: "set ss = S" and C: "chamber C"
shows   "∃n. (fold fst (map Spair ss) ^^ n) ` C = C0"
proof (cases "C=C0")
case True
hence "(fold fst (map Spair ss) ^^ 0) ` C = C0" by simp
thus ?thesis by fast
next
case False with fundchamber assms show ?thesis
using chamber_pconnect[of C0 C] fundfold_comp_pgallery_ex_funpow
by    fastforce
qed

lemma fundfold_comp_fixespointwise_C0:
assumes "set ss ⊆ S"
shows   "fixespointwise (fold fst (map Spair ss)) C0"
proof (rule fold_fixespointwise, rule ballI)
fix fg assume "fg ∈ set (map Spair ss)"
from this obtain s where "s∈set ss" "fg = Spair s" by auto
with assms
have  fg': "OpposedThinChamberComplexFoldings X (fst fg) (snd fg) C0"
using Spair_fundfoldpair fundfoldpairs_def
by    fastforce
show "fixespointwise (fst fg) C0"
using OpposedThinChamberComplexFoldings.axioms(2)[OF fg']
OpposedThinChamberComplexFoldings.chamber_D0[OF fg']
OpposedThinChamberComplexFoldings.chambers(4)[OF fg']
chamber_system_def
ChamberComplexFolding.chamber_retraction1[of X "fst fg" C0]
by    auto
qed

lemma fundfold_comp_endomorphism:
assumes "set ss ⊆ S"
shows   "ChamberComplexEndomorphism X (fold fst (map Spair ss))"
proof (rule fold_chamber_complex_endomorph_list, rule ballI)
fix fg assume fg: "fg ∈set (map Spair ss)"
from this obtain s where "s∈set ss" "fg = Spair s" by auto
with assms show "ChamberComplexEndomorphism X (fst fg)"
using     Spair_fundfoldpair
OpposedThinChamberComplexFoldings.axioms(2)[of X]
ChamberComplexFolding.axioms(1)[of X]
ChamberComplexRetraction.axioms(1)[of X]
unfolding fundfoldpairs_def
by        fastforce
qed

lemma finite_S: "finite S"
by    (blast intro: inj_on_finite fundchamber_S_image_inj_on)

lemma ex_label_retraction: "∃φ. label_wrt C0 φ ∧ fixespointwise φ C0"
proof-
obtain ss where ss: "set ss = S" using finite_S finite_list by fastforce

define fgs where "fgs = map Spair ss"
― ‹for @{term "fg ∈ set fgs"}, have @{term "(fst fg) ` D = C0"} for some @{term "D ∈ fundajdset"}›

define ψ where "ψ = fold fst fgs" (* ψ = fn ∘ … ∘ f1 *)
define vdist where "vdist v = (LEAST n. (ψ^^n) v ∈ C0)" for v
define φ where "φ v = (ψ^^(vdist v)) v" for v

have "label_wrt C0 φ"
unfolding label_wrt_def
proof
fix C assume C: "C∈𝒞"
show "bij_betw φ C C0"
proof-
from ψ_def fgs_def ss C obtain m where m: "(ψ^^m)`C = C0"
using chamber_system_def fundfold_comp_chamber_ex_funpow by fastforce
have "⋀v. v∈C ⟹ (ψ^^m) v = φ v"
proof-
fix v assume v: "v∈C"
define n where "n = (LEAST n. (ψ^^n) v ∈ C0)"
from v m φ_def vdist_def n_def have "m ≥ n" "φ v ∈ C0"
using Least_le[of "λn. (ψ^^n) v ∈ C0" m]
LeastI_ex[of "λn. (ψ^^n) v ∈ C0"]
by    auto
then show "(ψ^^m) v = φ v"
using ss ψ_def fgs_def φ_def vdist_def n_def funpow_add[of "m-n" n ψ]
fundfold_comp_fixespointwise_C0
funpower_fixespointwise fixespointwiseD
by    fastforce
qed
with C m ss ψ_def fgs_def show ?thesis
using chamber_system_def fundchamber fundfold_comp_endomorphism
ChamberComplexEndomorphism.funpower_endomorphism[of X]
ChamberComplexEndomorphism.bij_betw_chambers[of X]
bij_betw_cong[of C "ψ^^m" φ C0]
by    fastforce
qed
qed
moreover from vdist_def φ_def have "fixespointwise φ C0"
using Least_eq_0 by (fastforce intro: fixespointwiseI)
ultimately show ?thesis by fast
qed

lemma ex_label_map: "∃φ. label_wrt C0 φ"
using ex_label_retraction by fast

end (* context ThinChamberComplexManyFoldings *)

subsubsection ‹More on the action of the group of automorphisms on chambers›

text ‹
Recall that we have already verified that @{term W} acts transitively on the chamber system. We
now use the labelling of the chamber complex examined in the previous section to show that this
action is simply transitive.
›

context ThinChamberComplexManyFoldings
begin

lemma fundchamber_W_image_ker:
assumes "w∈W" "w`→C0 = C0"
shows   "w = 0"
proof-
obtain φ where φ: "label_wrt C0 φ" using ex_label_map by fast
have "fixespointwise (permutation w) C0"
using W_respects_labels[OF φ assms(1)] chamberD_simplex[OF fundchamber]
ChamberComplexEndomorphism.respects_label_fixes_chamber_imp_fixespointwise[
OF W_endomorphism, OF assms(1) φ fundchamber assms(2)
]
by    fast
with assms(1) show ?thesis
using fundchamber W_automorphism trivial_automorphism
standard_uniqueness_automorphs
permutation_inject[of w 0]
qed

lemma fundchamber_W_image_inj_on:
"inj_on (λw. w`→C0) W"
proof (rule inj_onI)
fix w w' assume ww': "w∈W" "w'∈W" "w`→C0 = w'`→C0"
from ww'(3) have "(-w')`→w`→C0 = (-w')`→w'`→C0" by simp
with ww'(1,2) show "w = w'"
using fundchamber_W_image_ker[of "-w'+w"] add.assoc[of w' "-w'" w]
image_comp plus_permutation.rep_eq[THEN sym]
)
qed

end (* context ThinChamberComplexManyFoldings *)

subsubsection ‹A bijection between the fundamental chamber and the set of generating automorphisms›

text ‹
Removing a single vertex from the fundamental chamber determines a facet, a facet in the
fundamental chamber determines an adjacent chamber (since our complex is thin), and a chamber
adjacent to the fundamental chamber determines an automorphism (via some pair of opposed foldings)
in our generating set @{term S}. Here we show that this correspondence is bijective.
›

context ThinChamberComplexManyFoldings
begin

definition fundantivertex :: "'a permutation ⇒ 'a"
where "fundantivertex s ≡ (THE v. v ∈ C0-s`→C0)"

abbreviation "fundantipermutation ≡ the_inv_into S fundantivertex"

lemma fundantivertex: "s∈S ⟹ fundantivertex s ∈ C0-s`→C0"
fundchamber_S_image_neq_fundchamber[of s]
by    auto

lemma fundantivertex_fundchamber_decomp:
"s∈S ⟹ C0 = insert (fundantivertex s) (C0∩s`→C0)"
fundchamber_S_image_neq_fundchamber[of s]
by    auto

lemma fundantivertex_unstable:
"s∈S ⟹ s → fundantivertex s ≠ fundantivertex s"
using fundantivertex_fundchamber_decomp[of s]
image_insert[of "(→) s" "fundantivertex s" "C0∩s`→C0"]
S_fixes_fundchamber_image_int fundchamber_S_image_neq_fundchamber
by    fastforce

lemma fundantivertex_inj_on: "inj_on fundantivertex S"
proof (rule inj_onI)
fix s t assume st: "s∈S" "t∈S" "fundantivertex s = fundantivertex t"
hence "insert (fundantivertex s) (C0∩s`→C0) =
insert (fundantivertex s) (C0∩t`→C0)"
using fundantivertex_fundchamber_decomp[of s]
fundantivertex_fundchamber_decomp[of t]
by    auto
moreover from st
have  "fundantivertex s ∉ C0∩s`→C0" "fundantivertex s ∉ C0∩t`→C0"
using fundantivertex[of s] fundantivertex[of t]
by    auto
ultimately have "C0∩s`→C0 = C0∩t`→C0"
using insert_subset_equality[of "fundantivertex s"] by simp
with st(1,2) show "s=t"
using fundchamber fundchamber_S_chamber[of s] fundchamber_S_chamber[of t]
fundfacets[of s] fundfacets(2)[of t]
fundchamber_S_image_neq_fundchamber[of s]
fundchamber_S_image_neq_fundchamber[of t]
facet_unique_other_chamber[of C0 "C0∩s`→C0" "s`→C0" "t`→C0"]
genby_genset_closed[of _ S]
inj_onD[OF fundchamber_W_image_inj_on, of s t]
by    auto
qed

lemma fundantivertex_surj_on: "fundantivertex ` S = C0"
proof (rule seteqI)
show "⋀v. v ∈ fundantivertex ` S ⟹ v∈C0" using fundantivertex by fast
next
fix v assume v: "v∈C0"
define D where "D = the_adj_chamber C0 (C0-{v})"
by    fastforce
from this obtain s where s: "s∈S" "D = s`→C0"
with v D_def [abs_def] have "fundantivertex s = v"
fundchamber_S_image_neq_fundchamber[of s]
facetrel_diff_vertex[of v C0]
unfolding fundantivertex_def
with s(1) show "v ∈ fundantivertex ` S" by fast
qed

lemma fundantivertex_bij_betw: "bij_betw fundantivertex S C0"
unfolding bij_betw_def
using     fundantivertex_inj_on fundantivertex_surj_on
by        fast

lemma card_S_fundchamber: "card S = card C0"
using bij_betw_same_card[OF fundantivertex_bij_betw] by fast

lemma card_S_chamber:
"chamber C ⟹ card C = card S"
using fundchamber chamber_card[of C0 C] card_S_fundchamber by auto

lemma fundantipermutation1:
"v∈C0 ⟹ fundantipermutation v ∈ S"
using fundantivertex_surj_on the_inv_into_into[OF fundantivertex_inj_on] by blast

end (* context ThinChamberComplexManyFoldings *)

subsection ‹Thick chamber complexes›

text ‹
A thick chamber complex is one in which every facet is a facet of at least three chambers.
›

locale ThickChamberComplex = ChamberComplex X
for X :: "'a set set"
+ assumes thick:
"chamber C ⟹ z⊲C ⟹
∃D E. D∈X-{C} ∧ z⊲D ∧ E∈X-{C,D} ∧ z⊲E"
begin

definition some_third_chamber :: "'a set ⇒ 'a set ⇒ 'a set ⇒ 'a set"
where "some_third_chamber C D z ≡ SOME E. E∈X-{C,D} ∧ z⊲E"

lemma facet_ex_third_chamber: "chamber C ⟹ z⊲C ⟹ ∃E∈X-{C,D}. z⊲E"
using thick[of C z] by auto

lemma some_third_chamberD_facet:
"chamber C ⟹ z⊲C ⟹ z ⊲ some_third_chamber C D z"
using facet_ex_third_chamber[of C z D] someI_ex[of "λE. E∈X-{C,D} ∧ z⊲E"]
some_third_chamber_def
by    auto

lemma some_third_chamberD_simplex:
"chamber C ⟹ z⊲C ⟹ some_third_chamber C D z ∈ X"
using facet_ex_third_chamber[of C z D] someI_ex[of "λE. E∈X-{C,D} ∧ z⊲E"]
some_third_chamber_def
by    auto

"chamber C ⟹ z⊲C ⟹ C ∼ some_third_chamber C D z"
using some_third_chamberD_facet by (fast intro: adjacentI)

lemma chamber_some_third_chamber:
"chamber C ⟹ z⊲C ⟹ chamber (some_third_chamber C D z)"