Theory Chamber

section ‹Chamber complexes›

text ‹
  Now we develop the basic theory of chamber complexes, including both thin and thick complexes.
  Some terminology: a maximal simplex is now called a chamber, and a chain (with respect to
  adjacency) of chambers is now called a gallery. A gallery in which no chamber appears more than
  once is called proper, and we use the prefix p as a naming convention to denote proper.
  Again, we remind the reader that some sources reserve the name gallery for (a slightly weaker
  notion of) what we are calling a proper gallery, using pregallery to denote an improper gallery.

theory Chamber
imports Algebra Simplicial


subsection ‹Locale definition and basic facts›

locale ChamberComplex = SimplicialComplex X
  for X :: "'a set set"
+ assumes simplex_in_max : "yX  x. maxsimp x  yx"
  and     maxsimp_connect: " x  y; maxsimp x; maxsimp y   
                            xs. maxsimpchain (x#xs@[y])"

context ChamberComplex

abbreviation "chamber       maxsimp"
abbreviation "gallery       maxsimpchain"
abbreviation "pgallery      pmaxsimpchain"
abbreviation "min_gallery   min_maxsimpchain"
abbreviation "supchamber v  (SOME C. chamber C  vC)"

lemmas faces                     = faces
lemmas singleton_simplex         = singleton_simplex
lemmas chamberI                  = maxsimpI
lemmas chamberD_simplex          = maxsimpD_simplex
lemmas chamberD_maximal          = maxsimpD_maximal
lemmas finite_chamber            = finite_maxsimp
lemmas chamber_nempty            = maxsimp_nempty
lemmas chamber_vertices          = maxsimp_vertices
lemmas gallery_def               = maxsimpchain_def
lemmas gallery_snocI             = maxsimpchain_snocI
lemmas galleryD_chamber          = maxsimpchainD_maxsimp
lemmas galleryD_adj              = maxsimpchainD_adj
lemmas gallery_CConsI            = maxsimpchain_CConsI
lemmas gallery_Cons_reduce       = maxsimpchain_Cons_reduce
lemmas gallery_append_reduce1    = maxsimpchain_append_reduce1
lemmas gallery_append_reduce2    = maxsimpchain_append_reduce2
lemmas gallery_remdup_adj        = maxsimpchain_remdup_adj
lemmas gallery_obtain_pgallery   = maxsimpchain_obtain_pmaxsimpchain
lemmas pgallery_def              = pmaxsimpchain_def
lemmas pgalleryI_gallery         = pmaxsimpchainI_maxsimpchain
lemmas pgalleryD_chamber         = pmaxsimpchainD_maxsimp
lemmas pgalleryD_adj             = pmaxsimpchainD_adj
lemmas pgalleryD_distinct        = pmaxsimpchainD_distinct
lemmas pgallery_Cons_reduce      = pmaxsimpchain_Cons_reduce
lemmas pgallery_append_reduce1   = pmaxsimpchain_append_reduce1
lemmas pgallery                  = pmaxsimpchain
lemmas min_gallery_simps         = min_maxsimpchain.simps
lemmas min_galleryI_betw         = min_maxsimpchainI_betw
lemmas min_galleryI_betw_compare = min_maxsimpchainI_betw_compare
lemmas min_galleryD_min_betw     = min_maxsimpchainD_min_betw
lemmas min_galleryD_gallery      = min_maxsimpchainD_maxsimpchain
lemmas min_gallery_pgallery      = min_maxsimpchain_pmaxsimpchain
lemmas min_gallery_rev           = min_maxsimpchain_rev
lemmas min_gallery_adj           = min_maxsimpchain_adj
lemmas not_min_galleryI_betw     = not_min_maxsimpchainI_betw

lemmas min_gallery_betw_CCons_reduce =
lemmas min_gallery_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 "vX"
  defines "C  supchamber v"
  shows   "chamber C" "vC"
  using   assms simplex_in_max someI[of "λC. chamber C  vC"]
  by      auto

  "ChamberSubcomplex Y  Y  X  ChamberComplex Y 
    (C. ChamberComplex.chamber Y C  chamber C)"

lemma ChamberSubcomplexI:
  assumes "YX" "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 Y ys"
  using chambersub_imp_sub maxsimpchain_in_subcomplex by simp

lemma subcomplex_gallery:
  "ChamberSubcomplex Y 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
  case Single with assms show ?thesis
    using min_galleryD_gallery galleryD_chamber chamber_in_subcomplex
          ChamberComplex.min_gallery_simps(2) ChamberSubcomplexD_complex
    by    force
  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
          ChamberComplex.min_galleryI_betw[of Y]
    by    force

lemma chamber_card: "chamber C  chamber D  card C = card D"
  using maxsimp_connect[of C D] galleryD_adj adjacentchain_card
  by    (cases "C=D") auto

lemma chamber_facet_is_chamber_facet:
  " chamber C; chamber D; zC; zD   zD"
  using finite_chamber finite_facetrel_card chamber_card[of C]
  by    (fastforce intro: facetrelI_cardSuc)

lemma chamber_adj:
  assumes "chamber C" "DX" "C  D"
  shows   "chamber D"
  from assms(2) obtain B where B: "chamber B" "DB"
    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

lemma chambers_share_facet:
  assumes "chamber C" "chamber (insert v z)" "zC"
  shows   "zinsert v z"
proof (rule facetrelI)
  from assms show "vz"
    using finite_chamber[of C] finite_chamber[of "insert v z"] card_insert_if[of z v]
    by    (auto simp add: finite_facetrel_card chamber_card)
qed simp

lemma adjacentset_chamber: "chamber C  Dadjacentset C  chamber D"
  using adjacentset_def chamber_adj by fast

lemma chamber_shared_facet: " chamber C; zC; DX; zD   chamber D"
  by (fast intro: chamber_adj adjacentI)

lemma adjacentset_conv_facetchambersets:
  assumes "X  {{}}" "chamber C"
  shows   "adjacentset C = (vC. {DX. C-{v}D})"
proof (rule seteqI)
  fix D assume D: "D  adjacentset C"
  show "D  (vC. {DX. 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
    case False
    from D have D': "CD" using adjacentsetD_adj by fast
    with False obtain v where v: "vD" "C = insert v (CD)"
      using adjacent_int_decomp by fast
    hence "C-{v} = CD" 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
  from assms(2)
    show  "D. D  (vC. {EX. C-{v}E}) 
            D  adjacentset C"
    using     facetrel_diff_vertex adjacentI
    unfolding adjacentset_def
    by        fastforce

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

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

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" "CD"
  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" "CD"
  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" "CD"
  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   "FX" "chamber D"
  shows     "chamber (closest_supchamber F D)" "F  closest_supchamber F D"
  using     assms arg_min_natI[of "λC. chamber C  FC" ] simplex_in_max[of F]
  unfolding closest_supchamber_def
  by        auto

lemma closest_supchamber_closest:
  "chamber C  FC 
    chamber_distance (closest_supchamber F D) D  chamber_distance C D"
  using arg_min_nat_le[of "λC. chamber C  FC" C] closest_supchamber_def
  by simp

lemma face_distance_le:
  "chamber C  FC  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  FC  face_distance F C = 0"
  using chamber_distance_def closest_supchamber_def face_distance_def
          of "λC. chamber C  FC" 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

definition label_wrt :: "'b set  ('a'b)  bool"
  where "label_wrt B f  (C𝒞. bij_betw f C B)"

lemma label_wrtD: "label_wrt B f  C𝒞  bij_betw f C B"
  using label_wrt_def by fast

lemma label_wrtD': "label_wrt B f  chamber C  bij_betw f C B"
  using label_wrt_def chamber_system_def by fast

lemma label_wrt_adjacent:
  assumes "label_wrt B f" "chamber C" "chamber D" "CD" "vC-D" "wD-C"
  shows   "f v = f w"
  from assms(5) have "f`D = insert (f v) (f`(CD))"
    using adjacent_conv_insert[OF assms(4), of v] label_wrtD'[OF assms(1,2)]
          label_wrtD'[OF assms(1,3)]
          bij_betw_imp_surj_on[of f]
    by    force
  with assms(6) show ?thesis
    using adjacent_sym[OF assms(4)] adjacent_conv_insert[of D C]
          inj_on_insert[of f w "CD"]
          bij_betw_imp_inj_on[OF label_wrtD', OF assms(1,3)]
    by    (force simp add: Int_commute)

lemma label_wrt_adjacent_shared_facet:
  " label_wrt B f; chamber (insert v z); chamber (insert w z); vz; wz  
    f v = f w"
  by (auto intro: label_wrt_adjacent adjacentI facetrelI)

lemma label_wrt_elt_image: "label_wrt B f  vX  f v  B"
  using simplex_in_max label_wrtD' bij_betw_imp_surj_on by fast

end (* context ChamberComplex *)

subsection ‹Morphisms of chamber complexes›

text ‹
  While any function on the vertex set of a simplicial complex can be considered a morphism of
  simplicial complexes onto its image, for chamber complexes we require the function send chambers
  onto chambers of the same cardinality in some chamber complex of the codomain.

subsubsection ‹Morphism locale and basic facts›

locale ChamberComplexMorphism = domain: ChamberComplex X + codomain: ChamberComplex Y
  for     X :: "'a set set"
  and     Y :: "'b set set"
+ fixes   f :: "'a'b"
  assumes chamber_map:  "domain.chamber C  codomain.chamber (f`C)"
  and     dim_map    :  "domain.chamber C  card (f`C) = card C"

lemma (in ChamberComplex) trivial_morphism:
  "ChamberComplexMorphism X X id"
  by unfold_locales auto

lemma (in ChamberComplex) inclusion_morphism:
  assumes "ChamberSubcomplex Y"
  shows   "ChamberComplexMorphism Y X id"
  by      (
            rule ChamberComplexMorphism.intro,
            rule ChamberSubcomplexD_complex,
            rule assms, unfold_locales
          (auto simp add: subcomplex_chamber[OF assms])

context ChamberComplexMorphism

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
  by    unfold_locales auto

lemma comp:
  assumes "ChamberComplexMorphism Y Z g"
  shows   "ChamberComplexMorphism X Z (gf)"
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 ((gf)`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])

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

lemma restrict_codomain:
  assumes "codomain.ChamberSubcomplex Z" "fX  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

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: "xX  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: "xX  f`xY"
  using chamber_map domain.simplex_in_max codomain.chamberD_simplex
        codomain.faces[of _ "f`x"]
  by    force

lemma simplices_map: "fX  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  zC  f`z  f`C"
  using facetrel_subset facetrel_card codim_map[of C z]
  by    (fastforce intro: facetrelI_card)

lemma adj_int_im:
  assumes "domain.chamber C" "domain.chamber D" "C  D" "f`C  f`D"
  shows   "(f`C  f`D)  f`C"
proof (rule facetrelI_card)
  from assms(1,2) chamber_map have 1: "f`C  f`D  f`C = f`D"
    using codomain.chamberD_simplex codomain.chamberD_maximal[of "f`C" "f`D"]
    by    simp
  thus "f ` C  f ` D  f ` C" by fast

  from assms(1) have "card (f`C - f`C  f`D)  card (f`C - f`(CD))"
    using domain.finite_chamber
          card_mono[of "f`C - f`(CD)" "f`C - f`C  f`D"]
    by    fast
  moreover from assms(1,3,4) have "card (f`C - f`(CD)) = 1"
    using codim_map[of C "CD"] 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

lemma adj_map':
  assumes "domain.chamber C" "domain.chamber D" "C  D" "f`C  f`D"
  shows   "f`C  f`D"
  using   assms(3,4) adj_int_im[OF assms] adjacent_sym
          adj_int_im[OF assms(2) assms(1)]
  by      (auto simp add: Int_commute intro: adjacentI)

lemma adj_map:
  " domain.chamber C; domain.chamber D; C  D   f`C  f`D"
  using adjacent_refl[of "f`C"] adj_map' empty_not_adjacent[of D] by fastforce

lemma chamber_vertex_outside_facet_image:
  assumes "vz" "domain.chamber (insert v z)"
  shows   "f v  f`z"
  from assms(1) have "insert v z - z = {v}" by force
  with assms(2) show ?thesis using codim_map by fastforce

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),
  from assms show
    "x. domain.chamber x  SimplicialComplex.maxsimp Z (f ` x)"
    using chamber_map ChamberComplex.subcomplex_chamber by fast
qed (auto simp add: dim_map)

end (* context ChamberComplexMorphism *)

subsubsection ‹Action on pregalleries and galleries›

context ChamberComplexMorphism

lemma gallery_map: " Cs (fCs)"
proof (induct Cs rule: list_induct_CCons)
  case (Single C) thus ?case
    using domain.galleryD_chamber chamber_map codomain.gallery_def by auto
  case (CCons B C Cs)
  have " (f`B # f`C # fCs)"
  proof (rule codomain.gallery_CConsI)
    from CCons(2) show "codomain.chamber (f ` B)"
      using domain.galleryD_chamber chamber_map by simp
    from CCons show " (f`C # fCs)"
      using domain.gallery_Cons_reduce by auto
    from CCons(2) show "f`B   f`C"
      using domain.gallery_Cons_reduce[of B "C#Cs"] domain.galleryD_adj
            domain.galleryD_chamber adj_map
      by    fastforce
  thus ?case by simp
qed (simp add: codomain.maxsimpchain_def)

lemma gallery_betw_map:
  " (C#Cs@[D]) (f`C # fCs @ [f`D])"
  using gallery_map by fastforce

end (* context ChamberComplexMorphism *)

subsubsection ‹Properties of the image›

context ChamberComplexMorphism

lemma subcomplex_image: "codomain.Subcomplex (fX)"
  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 (fX) (f`x)"
proof (
  rule SimplicialComplex.maxsimpI, rule simplicialcomplex_image, rule imageI,
  rule domain.chamberD_simplex, rule assms
  from assms show "z. zfX  f`x  z  z = f`x"
    using chamber_map[of x] simplex_map codomain.chamberD_maximal[of "f`x"]
    by    blast

lemma maxsimp_preimage:
  assumes "CX" "SimplicialComplex.maxsimp (fX) (f`C)"
  shows "domain.chamber C"
  from assms(1) obtain D where D: "domain.chamber D" "CD"
    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 "fX" "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

lemma chamber_preimage:
  "CX  codomain.chamber (f`C)  domain.chamber C"
  using chamber_in_image maxsimp_preimage by simp

lemma chambercomplex_image: "ChamberComplex (fX)"
proof (intro_locales, rule simplicialcomplex_image, unfold_locales)
  show "y. yfX  x. SimplicialComplex.maxsimp (fX) x  y  x"
    using domain.simplex_in_max maxsimp_map_into_image by fast
  fix x y
  assume xy:  "xy" "SimplicialComplex.maxsimp (fX) x"
              "SimplicialComplex.maxsimp (fX) y"
  from xy(2,3) obtain zx zy where zxy: "zxX" "x = f`zx" "zyX" "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: " (zx#ws@[zy])"
    using maxsimp_preimage domain.maxsimp_connect[of zx zy] by auto
  with ws zxy(2,4) have "SimplicialComplex.maxsimpchain (fX) (x#(fws)@[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 (fX) (x#xs@[y])" by fast

lemma chambersubcomplex_image: "codomain.ChamberSubcomplex (fX)"
  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 (fX) f"
  using restrict_codomain chambersubcomplex_image by fast

end (* context ChamberComplexMorphism *)

subsubsection ‹Action on the chamber system›

context ChamberComplexMorphism

lemma chamber_system_into: "fdomain.𝒞  codomain.𝒞"
  using chamber_map domain.chamber_system_def codomain.chamber_system_def
  by    auto

lemma chamber_system_image: "fdomain.𝒞 = codomain.𝒞  (fX)"
  show "fdomain.𝒞  codomain.𝒞  (fX)"
    using chamber_system_into domain.chamber_system_simplices by fast
  show "fdomain.𝒞  codomain.𝒞  (fX)"
    fix D assume "D  codomain.𝒞  (fX)"
    hence "C. domain.chamber C  f`C = D"
      using codomain.chamber_system_def chamber_preimage by fast
    thus "D  fdomain.𝒞" using domain.chamber_system_def by auto

lemma image_chamber_system: "ChamberComplex.𝒞 (fX) = 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.𝒞 (fX) = codomain.𝒞  (fX)"
  using image_chamber_system chamber_system_image by simp

lemma face_distance_eq_chamber_distance_map:
  assumes "domain.chamber C" "domain.chamber D" "CD" "zC"
          "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
          gallery_betw_map[OF domain.gallery_least_length, of C D]
  by      force

lemma face_distance_eq_chamber_distance_min_gallery_betw_map:
  assumes "domain.chamber C" "domain.chamber D" "CD" "zC"
          "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" "fCs" "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 : "fX = 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 (gf) (X)" "fixespointwise (fg) (Y)"
  shows   "ChamberComplexIsomorphism X Y f"
proof (rule ChamberComplexIsomorphism.intro)
  show "ChamberComplexMorphism X Y f" ..
  show "ChamberComplexIsomorphism_axioms X Y f"
    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 "fX = Y"
    proof (rule order.antisym, rule simplices_map, rule subsetI)
      fix y assume "yY"
      moreover hence "(fg) ` y  fX"
        using ChamberComplexMorphism.simplex_map[OF assms(1)]
        by    (simp add: image_comp[THEN sym])
      ultimately show "y  fX" 
        using fixespointwise_subset[OF assms(3), of y] fixespointwise_im by fastforce

context ChamberComplexIsomorphism

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 (fCs)"
  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,
  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

lemma iso_comp:
  assumes "ChamberComplexIsomorphism Y Z g"
  shows   "ChamberComplexIsomorphism X Z (gf)"
  by      (
            rule ChamberComplexIsomorphism.intro, rule comp,
            rule ChamberComplexIsomorphism.axioms(1),
            rule assms, unfold_locales, rule bij_betw_trans,
            rule bij_betw_vertices,
            rule ChamberComplexIsomorphism.bij_betw_vertices,
            rule assms
          (simp add:
            setsetmapim_comp surj_simplex_map assms

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

lemma inv: "ChamberComplexIsomorphism Y X (the_inv_into (X) f)"
  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
    by    force
  fix C assume C: "codomain.chamber C"
  hence C': "CfX" 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 "DX" "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: "zX" "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
  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])

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
  case False
  define Cs Ds where "Cs = (ARG_MIN length Cs. (C#Cs@[D]))"
    and "Ds = (ARG_MIN length Ds. (f`C # Ds @ [f`D]))"
  from assms False Cs_def have " (f`C # fCs @ [f`D])"
    using gallery_map domain.maxsimp_connect[of C D]
          arg_min_natI[of "λCs. (C#Cs@[D])"]
    by    fastforce
  moreover from assms Cs_def
    have  "Es. (f`C # Es @ [f`D]) 
            length (fCs)  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. (C#Cs@[D])" _ length]
    by    force
  ultimately have "length Ds = length (fCs)"
    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

lemma face_distance_map:
  assumes "domain.chamber C" "FX"
  shows   "codomain.face_distance (f`F) (f`C) = domain.face_distance F C"
  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"
    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)
      by    (fastforce intro: arg_min_nat_le)
    with assms D_def D'_def show ?thesis
      using chambers(2) chamber_distance_map by simp
    have "domain.chamber_distance D C  codomain.chamber_distance D' (f`C)"
    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
  ultimately show ?thesis
    using D_def D'_def domain.face_distance_def codomain.face_distance_def
    by    simp

end (* context ChamberComplexIsomorphism *)

subsubsection ‹Endomorphisms›

locale ChamberComplexEndomorphism = ChamberComplexMorphism X X f
  for X :: "'a set set"
  and f :: "'a'a"
+ assumes trivial_outside : "vX  f v = v"
  ― ‹to facilitate uniqueness arguments›

lemma (in ChamberComplex) trivial_endomorphism:
  "ChamberComplexEndomorphism X id"
  by  (
        rule ChamberComplexEndomorphism.intro, rule trivial_morphism,

context ChamberComplexEndomorphism

abbreviation "ChamberSubcomplex  domain.ChamberSubcomplex"
abbreviation "Subcomplex  domain.Subcomplex"
abbreviation "chamber  domain.chamber"
abbreviation "gallery"
abbreviation "𝒞  domain.chamber_system"
abbreviation "label_wrt  domain.label_wrt"

lemmas dim_map                 = dim_map
lemmas simplex_map             = simplex_map
lemmas vertex_map              = vertex_map
lemmas chamber_map             = chamber_map
lemmas adj_map                 = adj_map
lemmas facet_map               = facet_map
lemmas bij_betw_chambers       = bij_betw_chambers
lemmas chamber_system_into     = chamber_system_into
lemmas chamber_system_image    = chamber_system_image
lemmas image_chamber_system    = image_chamber_system
lemmas chambercomplex_image    = chambercomplex_image
lemmas chambersubcomplex_image = chambersubcomplex_image

lemmas face_distance_eq_chamber_distance_map =
lemmas face_distance_eq_chamber_distance_min_gallery_betw_map =
lemmas facedist_chdist_mingal_btwmap =

lemmas trivial_endomorphism     = domain.trivial_endomorphism
lemmas finite_simplices         = domain.finite_simplices
lemmas faces                    = domain.faces
lemmas maxsimp_connect          = domain.maxsimp_connect
lemmas simplex_in_max           = domain.simplex_in_max
lemmas chamberD_simplex         = domain.chamberD_simplex
lemmas chamber_system_def       = domain.chamber_system_def
lemmas chamber_system_simplices = domain.chamber_system_simplices
lemmas galleryD_chamber         = domain.galleryD_chamber
lemmas galleryD_adj             = domain.galleryD_adj
lemmas gallery_append_reduce1   = domain.gallery_append_reduce1
lemmas gallery_Cons_reduce      = domain.gallery_Cons_reduce
lemmas gallery_chamber_system   = domain.gallery_chamber_system
lemmas label_wrtD               = domain.label_wrtD
lemmas label_wrt_adjacent       = domain.label_wrt_adjacent

lemma endo_comp:
  assumes "ChamberComplexEndomorphism X g"
  shows   "ChamberComplexEndomorphism X (gf)"
proof (rule ChamberComplexEndomorphism.intro)
  from assms show "ChamberComplexMorphism X X (gf)"
    using comp ChamberComplexEndomorphism.axioms by fast
  from assms show "ChamberComplexEndomorphism_axioms X (gf)"
    using trivial_outside ChamberComplexEndomorphism.trivial_outside
    by    unfold_locales auto

lemma restrict_endo:
  assumes "ChamberSubcomplex Y" "fY  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]
          restrict_domain fun_eq_on_restrict1
    by    fast
  show "ChamberComplexEndomorphism_axioms Y (restrict1 f (Y))"
    by unfold_locales simp

lemma funpower_endomorphism:
  "ChamberComplexEndomorphism X (f^^n)"
proof (induct n)
  case 0 show ?case using trivial_endomorphism subst[of id] by fastforce
  case (Suc m)
  hence "ChamberComplexEndomorphism X (f^^m  f)"
    using endo_comp by auto
  moreover have "f^^m  f = f^^(Suc m)"
    by (simp add: funpow_Suc_right[THEN sym])
  ultimately show ?case
    using subst[of _ _ "λf. ChamberComplexEndomorphism X f"] by fast

end (* context ChamberComplexEndomorphism *)

lemma (in ChamberComplex) fold_chamber_complex_endomorph_list:
  "xset 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
  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

context ChamberComplexEndomorphism

lemma split_gallery:
  " Cf𝒞; D𝒞-f𝒞; gallery (C#Cs@[D])  
    As A B Bs. Af𝒞  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
  case (Cons E Es)
  show ?case
  proof (cases "Ef𝒞")
    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: "Af𝒞" "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
    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

lemma respects_labels_adjacent:
  assumes "label_wrt B φ" "chamber C" "chamber D" "CD" "vC. φ (f v) = φ v"
  shows   "vD. φ (f v) = φ v"
proof (cases "C=D")
  case False have CD: "CD" by fact
  with assms(4) obtain w where w: "wD" "C = insert w (CD)"
    using adjacent_int_decomp by fast
  with assms(2) have fC: "f w  f`(CD)" "f`C = insert (f w) (f`(CD))"
    using chamber_vertex_outside_facet_image[of w "CD"] by auto
  show ?thesis
    fix v assume v: "vD"
    show "φ (f v) = φ v"
    proof (cases "vC")
      case False
      with assms(3,4) v have fD: "f v  f`(DC)" "f`D = insert (f v) (f`(DC))"
        using adjacent_sym[of C D] adjacent_conv_insert[of D C v]
              chamber_vertex_outside_facet_image[of v "DC"]
        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
        case False
        from assms(2-4) have "chamber (f`C)" "chamber (f`D)" and fCfD: "f`Cf`D"
          using chamber_map adj_map by auto
        moreover from assms(4) fC fCfD False have "f w  f`C - f`D"
          using adjacent_to_adjacent_int[of C D f] by auto
        ultimately show ?thesis
          using assms(4) fD fCfD False adjacent_sym
                adjacent_to_adjacent_int[of D C f]
                label_wrt_adjacent[OF assms(1), of "f`C" "f`D" "f w" "f v", THEN sym]
          by    auto
      with False v w assms(5) show ?thesis
        using label_wrt_adjacent[OF assms(1-4), of w v, THEN sym] by fastforce
    qed (simp add: assms(5))
qed (simp add: assms(5))

lemma respects_labels_gallery:
  assumes "label_wrt B φ" "vC. φ (f v) = φ v"
  shows   "gallery (C#Cs@[D])  vD. φ (f v) = φ v"
proof (induct Cs arbitrary: D rule: rev_induct)
  case Nil with assms(2) show ?case
    using galleryD_chamber galleryD_adj
          respects_labels_adjacent[OF assms(1), of C D]
    by    force
  case (snoc E Es)
  with assms(2) show ?case
    using gallery_append_reduce1[of "C#Es@[E]"] galleryD_chamber galleryD_adj
          binrelchain_append_reduce2[of adjacent "C#Es" "[E,D]"]
          respects_labels_adjacent[OF assms(1), of E D]
    by    force

lemma respect_label_fix_chamber_imp_fun_eq_on:
  assumes label  :  "label_wrt B φ"
  and     chamber:  "chamber C" "f`C = g`C"
  and     respect:  "vC. φ (f v) = φ v" "vC. φ (g v) = φ v"
  shows   "fun_eq_on f g C"
proof (rule fun_eq_onI)
  fix v assume "vC"
  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

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 : "vX  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

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 "xX" "yX" rule: two_cases) auto
  show "surj f" unfolding surj_def
    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 "yX") auto

lemma comp:
  assumes "ChamberComplexAutomorphism X g"
  shows   "ChamberComplexAutomorphism X (gf)"
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)"
    from assms show "bij_betw (gf) (X) (X)"
      using bij_betw_vertices ChamberComplexAutomorphism.bij_betw_vertices
      by    fast
    from assms show "(gf)  X = X"
      using surj_simplex_map ChamberComplexAutomorphism.surj_simplex_map 
      by    (force simp add: setsetmapim_comp)
  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"
  fix x show "f x = g x"
    using trivial_outside fun_eq_onD[OF assms(2)] 
          ChamberComplexAutomorphism.trivial_outside[OF assms(1)]
    by    force

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: "vX  f (f v) = f v"

lemmas simplex_map = simplex_map
lemmas chamber_map = chamber_map
lemmas gallery_map = gallery_map

lemma vertex_retraction: "vf`(X)  f v = v"
  using retraction by fast

lemma simplex_retraction1: "xfX  fixespointwise f x"
  using retraction fixespointwiseI[of x f] by auto

lemma simplex_retraction2: "xfX  f`x = x"
  using retraction retraction[THEN sym] by blast

lemma chamber_retraction1: "Cf𝒞  fixespointwise f C"
  using chamber_system_simplices simplex_retraction1 by auto

lemma chamber_retraction2: "Cf𝒞  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"
  from assms(2) obtain C where "chamber C" "vC" using simplex_in_max by fast
  thus ?thesis
    using chamber_retraction1[of C] chamber_system_def chamber_map
          maxsimp_connect[of "f`C" C] chamber_retraction1[of "f`C"]
          respects_labels_gallery[OF assms(1), THEN bspec, of "f`C" _ C v]
    by    (force simp add: fixespointwiseD)

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  CfX 
      ∃!D. chamber D  DfX  f`D = C"

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

definition opp_half_apartment :: "'a set set"
  where "opp_half_apartment  {xX. C𝒞-f𝒞. xC}"
abbreviation "Y  opp_half_apartment"

lemma opp_half_apartment_subset_complex: "YX"
  using opp_half_apartment_def by fast

lemma simplicialcomplex_opp_half_apartment: "SimplicialComplex Y"
  show "xY. finite x"
    using opp_half_apartment_subset_complex finite_simplices by fast
  fix x y assume "xY" "yx" thus "yY"
    using     opp_half_apartment_subset_complex faces[of x y]
    unfolding opp_half_apartment_def
    by        auto

lemma subcomplex_opp_half_apartment: "Subcomplex Y"
  using opp_half_apartment_subset_complex simplicialcomplex_opp_half_apartment
  by    fast

lemma opp_half_apartmentI: " xX; C𝒞-f𝒞; xC   xY"
  using opp_half_apartment_def by auto

lemma opp_chambers_subset_opp_half_apartment: "𝒞-f𝒞  Y"
  fix C assume "C  𝒞-f𝒞"
  thus "C  Y" using chamber_system_simplices opp_half_apartmentI by auto

lemma maxsimp_in_opp_half_apartment:
  assumes "SimplicialComplex.maxsimp Y C"
  shows   "C  𝒞-f𝒞"
  from assms obtain D where D: "D𝒞-f𝒞" "CD"
    using SimplicialComplex.maxsimpD_simplex[
            OF simplicialcomplex_opp_half_apartment, of C
    by    auto
  with assms show ?thesis
    using opp_chambers_subset_opp_half_apartment 
            OF simplicialcomplex_opp_half_apartment
    by    force

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

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" "CfX" "chamber D" "DfX" "f`C = f`D"
  shows   "C=D"
  from assms(1) folding have ex1: "∃!B. chamber B  BfX  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

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" "BfX" "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 "Cf𝒞"
  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
  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

lemma opp_chambers_distinct_map:
  "set Cs  𝒞-f𝒞  distinct Cs  distinct (fCs)"
  using distinct_map subset_inj_on[OF inj_on_opp_chambers] by auto

lemma opp_chamberD1: "Cf𝒞  opp_chamber C  𝒞-f𝒞"
    using theI'[OF folding'] by simp

lemma opp_chamberD2: "Cf𝒞  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

subsubsection ‹Locales and basic facts›

locale ThinishChamberComplex = ChamberComplex X
  for X :: "'a set set"
+ assumes thinish:
  " chamber C; zC; DX-{C}. zD   ∃!DX-{C}. zD"
  ― ‹being adjacent to a chamber, such a @{term D} would also be a chamber (see lemma
@{text "chamber_adj"})›

lemma facet_unique_other_chamber:
  " chamber B; zB; chamber C; zC; chamber D; zD; CB; DB 
  using chamberD_simplex bex1_equality[OF thinish, OF _ _ bexI, of B z C C D]
  by    auto

lemma finite_adjacentset:
  assumes "chamber C"
  shows   "finite (adjacentset C)"
proof (cases "X = {{}}")
  case True thus ?thesis using adjacentset_def by simp
  case False
  moreover have "finite (vC. {DX. C-{v}D})"
    from assms show "finite C" using finite_chamber by simp
    fix v assume "vC"
    with assms have Cv: "C-{v}C"
      using chamberD_simplex facetrel_diff_vertex by fast
    with assms have C: "C{DX. C-{v}D}"
      using chamberD_simplex by fast
    show "finite {DX. C-{v}D}"
    proof (cases "{DX. C-{v}D} - {C} = {}")
      case True
      hence 1: "{DX. C-{v}D} = {C}" using C by auto
      show ?thesis using ssubst[OF 1, of finite] by simp
      case False
      from this obtain D where D: "DX-{C}" "C-{v}D" by fast
      with assms have 2: "{DX. 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
  ultimately show ?thesis
    using assms adjacentset_conv_facetchambersets by simp

lemma label_wrt_eq_on_adjacent_vertex:
  fixes   v v' :: 'a
  and     z z' :: "'a set"
  defines D : "D  insert v z"
  and     D': "D'  insert v' z'"
  assumes label   : "label_wrt B f" "f v = f v'"
  and     chambers: "chamber C" "chamber D" "chamber D'" "zC" "z'C" "DC" "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: "zD" and z': "z'D'"
    using chambers_share_facet by auto
  show "zD" by fact

  from chambers(4,5) obtain w w'
    where w : "w  z " "C = insert w  z"
    and   w': "w' z'" "C = insert w' z'"
    unfolding facetrel_def
    by        fastforce
  from w' D' chambers(1,3) have "f`z' = f`C - {f v'}"
    using z' label_wrtD'[OF label(1), of C] bij_betw_imp_inj_on[of f C]
          facetrel_complement_vertex[of z']
          label_wrt_adjacent_shared_facet[OF label(1), of v']
    by    simp
  moreover from w D chambers(1,2) have "f`z = f`C - {f v}"
    using z label_wrtD'[OF label(1), of C] bij_betw_imp_inj_on[of f C]
          facetrel_complement_vertex[of z]
          label_wrt_adjacent_shared_facet[OF label(1), of v]
    by    simp
  ultimately show "zD'"
    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" "zC" "zD" "CD"
            "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

end (* context ThinishChamberComplex *)

lemma (in ChamberComplexIsomorphism) thinish_image_shared_facet:
  assumes dom:  "domain.chamber C" "domain.chamber D" "zC" "zD" "CD"
  and     cod:  "ThinishChamberComplex Y" "codomain.chamber D'" "f`z  D'"
                "D'  f`C"
  shows   "f`D = D'"
proof (rule ThinishChamberComplex.facet_unique_other_chamber, rule cod(1))
  from dom(1,2) show "codomain.chamber (f`C)" "codomain.chamber (f`D)"
    using chamber_map by auto
  from dom show "f`z  f`C" "f`z  f`D" using facet_map by auto
  from dom have "domain.pgallery [C,D]"
    using domain.pgallery_def adjacentI by fastforce
  hence "codomain.pgallery [f`C,f`D]" using pgallery_map[of "[C,D]"] by simp
  thus "f`D  f`C" using codomain.pgalleryD_distinct by fastforce
qed (rule cod(2), rule cod(3), rule cod(4))

locale ThinChamberComplex = ChamberComplex X
  for X :: "'a set set"
+ assumes thin:  "chamber C  zC  ∃!DX-{C}. zD"

sublocale ThinChamberComplex < ThinishChamberComplex
  using thin by unfold_locales simp

context ThinChamberComplex

lemma thinish: "ThinishChamberComplex X" ..

lemmas face_distance_eq_chamber_distance_compare_other_chamber =

abbreviation "the_adj_chamber C z  THE D. DX-{C}  z  D"

lemma the_adj_chamber_simplex:
  "chamber C  z  C  the_adj_chamber C z  X"
  using theI'[OF thin] by fast

lemma the_adj_chamber_facet: "chamber C  zC  z  the_adj_chamber C z"
  using theI'[OF thin] by fast

lemma the_adj_chamber_is_adjacent:
  "chamber C  zC  C  the_adj_chamber C z"
  using the_adj_chamber_facet by (auto intro: adjacentI)
lemma the_adj_chamber:
  "chamber C  z  C  chamber (the_adj_chamber C z)"
  using the_adj_chamber_simplex the_adj_chamber_is_adjacent
  by    (fast intro: chamber_adj)

lemma the_adj_chamber_neq:
  "chamber C  z  C  the_adj_chamber C z  C"
  using theI'[OF thin] by fast

lemma the_adj_chamber_adjacentset:
  "chamber C  zC  the_adj_chamber C z  adjacentset C"
  using adjacentset_def the_adj_chamber_simplex the_adj_chamber_is_adjacent
  by    fast

end (* context ThinChamberComplex *)

lemmas (in ChamberComplexIsomorphism) thin_image_shared_facet =
  thinish_image_shared_facet[OF _ _ _ _ _ ThinChamberComplex.thinish]

subsubsection ‹The standard uniqueness argument for chamber morphisms of thin chamber complexes›

context ThinishChamberComplex

lemma standard_uniqueness_dbl:
  assumes morph   : "ChamberComplexMorphism W X f"
                    "ChamberComplexMorphism W X g"
  and     chambers: "ChamberComplex.chamber W C"
                    "ChamberComplex.chamber W D"
                    "CD" "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: "vD"
  show "f v = g v"
  proof (cases "vC")
    case True with funeq show ?thesis using fun_eq_onD by fast
    case False
    define F G where "F = f`C  f`D" and "G = g`C  g`D"

    from morph(1) chambers(1-4) have 1: "f`C  f`D"
      using ChamberComplexMorphism.adj_map' by fast
    with F_def chambers(4) have F_facet: "Ff`C" "Ff`D"
      using adjacent_int_facet1[of "f`C"] adjacent_int_facet2[of "f`C"] by auto

    from F_def G_def chambers have "G = F"
      using ChamberComplexMorphism.adj_map'[OF morph(2)]
            adjacent_to_adjacent_int[of C D g] 1
            adjacent_to_adjacent_int[of C D f] funeq fun_eq_on_im[of f g]
      by    force
    with G_def morph(2) chambers have F_facet': "Fg`D"
      using ChamberComplexMorphism.adj_map' adjacent_int_facet2 by blast
    with chambers(1,2,4,5) have 2: "g`D = f`D"
      using ChamberComplexMorphism.chamber_map[OF morph(1)] F_facet
            ChamberComplexMorphism.chamber_map[OF morph(2)]
            fun_eq_on_im[OF funeq]
            facet_unique_other_chamber[of "f`C" F "g`D" "f`D"]
      by    auto
    from chambers(3) v False have 3: "D = insert v (DC)"
      using adjacent_sym adjacent_conv_insert by fast
    from chambers(4) obtain w where w: "w  f`C" "w  f`D"
      using adjacent_int_decomp[OF adjacent_sym, OF 1] by blast
    with 3 have "w = f v" by fast
    moreover from 2 w(2) obtain v' where "v'D" "w = g v'" by auto
    ultimately show ?thesis
      using w(1) 3 funeq by (fastforce simp add: fun_eq_on_im)

lemma standard_uniqueness_pgallery_betw:
  assumes morph   : "ChamberComplexMorphism W X f"
                    "ChamberComplexMorphism W X g"
  and     chambers: "fun_eq_on f g C" " W (C#Cs@[D])"
                    "pgallery (f(C#Cs@[D]))" "pgallery (g(C#Cs@[D]))"
  shows   "fun_eq_on f g D"
  from morph(1) have W: "ChamberComplex W"
    using ChamberComplexMorphism.domain_complex by fast
  have " fun_eq_on f g C; W (C#Cs@[D]);
          pgallery (f(C#Cs@[D])); pgallery (g(C#Cs@[D]))  
          fun_eq_on f g D"
  proof (induct Cs arbitrary: C)
    case Nil from assms Nil(1) show ?case
      using ChamberComplex.galleryD_chamber[OF W Nil(2)]
            ChamberComplex.galleryD_adj[OF W Nil(2)]
            pgalleryD_distinct[OF Nil(3)] pgalleryD_distinct[OF Nil(4)]
            pgalleryD_chamber[OF Nil(4)] standard_uniqueness_dbl[of W f g C D]
      by    auto
    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" "CB"
        using ChamberComplex.galleryD_chamber[OF W Cons(3)]
              ChamberComplex.galleryD_adj[OF W Cons(3)]
        by    auto
      show "f`B  f`C" using pgalleryD_distinct[OF Cons(4)] by fastforce
      show "g`B  g`C" using pgalleryD_distinct[OF Cons(5)] by fastforce
      show "chamber (g`B)" using pgalleryD_chamber[OF Cons(5)] by fastforce
    qed (rule Cons(2))
    with Cons(1,3-5) show ?case
      using ChamberComplex.gallery_Cons_reduce[OF W, of C "B#Bs@[D]"]
            pgallery_Cons_reduce[of "f`C" "f(B#Bs@[D])"]
            pgallery_Cons_reduce[of "g`C" "g(B#Bs@[D])"]
      by    force
  with chambers show ?thesis by simp

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" "vD"
    using ChamberComplex.simplex_in_max[OF W] by auto
  moreover define Cs where "Cs = (ARG_MIN length Cs. 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

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

end (* context ThinishChamberComplex *)

context ThinChamberComplex

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"

abbreviation "opp_chamber  folding.opp_chamber"

lemma adjacent_half_chamber_system_image:
  assumes chambers: "C  f𝒞" "D  𝒞-f𝒞"
  and     adjacent: "CD"
  shows   "f`D = C"
  from adjacent obtain z where z: "zC" "zD" 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
          SimplicialComplex.faces[of "fX" C z]
          folding.simplex_retraction2[of z]
    by    auto
  moreover from chambers have "f`D  D" "CD" 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

lemma adjacent_half_chamber_system_image_reverse:
  " C  f𝒞; D  𝒞-f𝒞; CD   opp_chamber C = D"
  using adjacent_half_chamber_system_image[of C D]
        the1_equality[OF folding.folding']
  by    fastforce

lemma chamber_image_closer:
  assumes "D𝒞-f𝒞" "Bf𝒞" "Bf`D" "gallery (B#Ds@[D])"
  shows   "Cs. gallery (B#Cs@[f`D])  length Cs < length Ds"
  from assms(1,2,4) obtain As A E Es
    where split: "Af𝒞" "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 "AE"
    using gallery_append_reduce2[of As "A#E#Es"] galleryD_adj[of "A#E#Es"]
    by    simp
  with assms(2) split(1,2)
    have  fB: "f`B = B" and fA: "f`A = A" and fE: "f`E = A"
    using folding.chamber_retraction2 adjacent_half_chamber_system_image[of A E]
    by    auto
  show "Cs. gallery (B#Cs@[f`D])  length Cs < length Ds"
  proof (cases As)
    case Nil have As: "As = []" by fact
    show ?thesis
    proof (cases Es rule: rev_cases)
      case Nil with split(3) As assms(3) fE show ?thesis by simp
      case (snoc Fs F)
      with assms(4) split(3) As fE
        have  "Ds = E#Fs" "gallery (B # fFs @ [f`D])"
        using fB folding.gallery_map[of "B#E#Fs@[D]"] gallery_Cons_reduce
        by    auto
      thus ?thesis by auto
    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 # fHs @ [f`D])"
        using folding.gallery_map gallery_append_reduce1[of "B # fHs @ [f`D]"]
        by    force
      with decomp(1) show ?thesis by auto
      case (snoc Fs F)
      with split(3) Cons assms(4) fB fA fE
        have  decomp: "Ds = Hs@A#E#Fs" "gallery (B # f(Hs@A#Fs) @ [f`D])"
        using folding.gallery_map[of "B#Hs@A#E#Fs@[D]"]
              gallery_remdup_adj[of "B#fHs" A "fFs@[f`D]"]
        by    auto
      from decomp(1) have "length (f(Hs@A#Fs)) < length Ds" by simp
      with decomp(2) show ?thesis by blast

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"
  fix B assume B: "Bf𝒞"
  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
    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

lemma gallery_double_cross_not_minimal_Cons1:
  " Bf𝒞; C𝒞-f𝒞; Df𝒞; gallery (B#C#Cs@[D])  
    ¬ min_gallery (B#C#Cs@[D])"
  using galleryD_adj[of "B#C#Cs@[D]"]
        adjacent_half_chamber_system_image[of B C]
        folding.gallery_map[of "B#C#Cs@[D]"]
        gallery_Cons_reduce[of B "B # fCs @ [D]"]
        is_arg_minD2[of length "(λDs. maxsimpchain (B#Ds@[D]))" _ "fCs"]
        min_maxsimpchain.simps(3)[of B "C#Cs" D]
  by(simp add: folding.chamber_retraction2)(meson