structure SimplicialComplex.Morphism {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] (K : SimplicialComplex V) (L : SimplicialComplex W) : Type (max u_1 u_2)

A simplicial morphism $K \to L$: a vertex map sending each face of $K$ to a face of $L$.

• toFun : V → W
• map_face (s : Finset V) : s ∈ K.faces → Finset.image self.toFun s ∈ L.faces

def SimplicialComplex.Morphism.IsChamberMap {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {K : SimplicialComplex V} {L : SimplicialComplex W} (f : K.Morphism L) : Prop

A morphism is a chamber map if it sends maximal faces to maximal faces.

def SimplicialComplex.Morphism.PreservesFacets {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {K : SimplicialComplex V} {L : SimplicialComplex W} (f : K.Morphism L) : Prop

A morphism preserves facets if codim-$1$ inclusions in $K$ go to codim-$1$ inclusions in $L$.

def SimplicialComplex.AgreeOn {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {K : SimplicialComplex V} {L : SimplicialComplex W} (f g : K.Morphism L) (C : Finset V) : Prop

Two morphisms f, g agree on $C$ if they coincide on every vertex of $C$.

def SimplicialComplex.AgreeOnImage {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {K : SimplicialComplex V} {L : SimplicialComplex W} (f g : K.Morphism L) (C : Finset V) : Prop

Two morphisms have equal image on $C$: $f(C) = g(C)$ as sets.

def SimplicialComplex.AtMostTwoChambers {W : Type u_2} [DecidableEq W] (L : SimplicialComplex W) : Prop

The "at most two chambers per facet" property: a facet $F$ lies in at most two chambers.

def SimplicialComplex.Morphism.NonStutteringAdj {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {K : SimplicialComplex V} {L : SimplicialComplex W} (f : K.Morphism L) : Prop

A morphism is non-stuttering on adjacent pairs: it never collapses adjacent chambers.

def SimplicialComplex.SubFaceCompatible {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {K : SimplicialComplex V} {L : SimplicialComplex W} (f g : K.Morphism L) : Prop

Sub-face compatibility: if $f, g$ agree on the image of a chamber $C$, then they agree on the image of any face of $C$.

theorem SimplicialComplex.agreeOn_imp_agreeOnImage {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {K : SimplicialComplex V} {L : SimplicialComplex W} {f g : K.Morphism L} {C : Finset V} (h : AgreeOn f g C) : AgreeOnImage f g C

Pointwise agreement on $C$ implies image agreement on $C$.

theorem SimplicialComplex.agree_image_next_chamber {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {K : SimplicialComplex V} {L : SimplicialComplex W} (hL : L.AtMostTwoChambers) (f g : K.Morphism L) (hf : f.IsChamberMap) (hg : g.IsChamberMap) (hfF : f.PreservesFacets) (hgF : g.PreservesFacets) (hf_ns : f.NonStutteringAdj) (hg_ns : g.NonStutteringAdj) (hcompat : SubFaceCompatible f g) {C₁ C₂ : Finset V} (hadj : K.Adjacent C₁ C₂) (hC₁_max : K.IsMaximal C₁) (hagree : AgreeOnImage f g C₁) : AgreeOnImage f g C₂

Inductive step: if $f, g$ agree on the image of $C_1$ and $C_1, C_2$ are adjacent, then under the hypotheses (at-most-two, chamber maps, facet preservation, non-stutter, sub-face compatible) they also agree on the image of $C_2$.

theorem SimplicialComplex.mem_of_getLast?_eq_some {α : Type u_3} {l : List α} {a : α} (h : l.getLast? = some a) : a ∈ l

If l.getLast? = some a then a ∈ l.

theorem SimplicialComplex.agree_image_along_chain {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {K : SimplicialComplex V} {L : SimplicialComplex W} (hL : L.AtMostTwoChambers) (f g : K.Morphism L) (hf : f.IsChamberMap) (hg : g.IsChamberMap) (hfF : f.PreservesFacets) (hgF : g.PreservesFacets) (hf_ns : f.NonStutteringAdj) (hg_ns : g.NonStutteringAdj) (hcompat : SubFaceCompatible f g) (cs : List (Finset V)) (hne : cs ≠ []) (hchain : List.IsChain K.Adjacent cs) (hall : ∀ C ∈ cs, K.IsMaximal C) (hagree : AgreeOnImage f g (cs.head hne)) (D : Finset V) : D ∈ cs → AgreeOnImage f g D

Propagate image-agreement of $f, g$ along an entire chain of chambers via successive applications of agree_image_next_chamber.

theorem SimplicialComplex.uniqueness_lemma_32 {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {K : ChamberComplex V} {L : SimplicialComplex W} (hL : L.AtMostTwoChambers) (f g : K.Morphism L) (hf : f.IsChamberMap) (hg : g.IsChamberMap) (hfF : f.PreservesFacets) (hgF : g.PreservesFacets) (hf_ns : f.NonStutteringAdj) (hg_ns : g.NonStutteringAdj) (hcompat : SubFaceCompatible f g) (C : Finset V) (hC : K.IsMaximal C) (hagree : AgreeOnImage f g C) (D : Finset V) : K.IsMaximal D → AgreeOnImage f g D

Uniqueness Lemma 3.2: in a chamber complex $K$ with $L$ satisfying the at-most-two property, two chamber maps with matching image on some chamber $C$ have matching image on every chamber of $K$ — i.e. they are determined by their action on a single chamber.

theorem SimplicialComplex.image_eq_of_fixes_pointwise {V : Type u_1} [DecidableEq V] {f : V → V} {C : Finset V} (h : ∀ v ∈ C, f v = v) : Finset.image f C = C

If $f$ fixes $C$ pointwise then $f(C) = C$ as a set.

theorem SimplicialComplex.fixes_pointwise_of_facet_and_image {V : Type u_1} [DecidableEq V] {f : V → V} {C F : Finset V} (hFC : F ⊆ C) (hcard : (C \ F).card = 1) (hfixF : ∀ v ∈ F, f v = v) (himg : Finset.image f C = C) (v : V) : v ∈ C → f v = v

If $F \subseteq C$ with $|C \setminus F| = 1$, $f$ fixes $F$ pointwise, and $f(C) = C$ then $f$ fixes the whole $C$ pointwise.

theorem SimplicialComplex.thin_fixes_next_chamber {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (hthin : X.IsThin) (f : X.Morphism X.toSimplicialComplex) (hf : f.IsChamberMap) (hfF : f.PreservesFacets) {C₁ C₂ : Finset V} (hadj : X.Adjacent C₁ C₂) (hfix₁ : ∀ v ∈ C₁, f.toFun v = v) (hne : Finset.image f.toFun C₂ ≠ C₁) (v : V) : v ∈ C₂ → f.toFun v = v

In a thin complex: if $f$ fixes $C_1$ pointwise and $f(C_2) \neq C_1$ (no "fold back"), then $f$ fixes the adjacent chamber $C_2$ pointwise too.

def SimplicialComplex.GalleryStuttersUnder {V : Type u_1} [DecidableEq V] (cs : List (Finset V)) (f : V → V) : Prop

The image gallery $(C \mapsto f(C))$ stutters: some adjacent images are equal.

def SimplicialComplex.FixesAllPointwise {V : Type u_1} (cs : List (Finset V)) (f : V → V) : Prop

$f$ fixes every chamber of $cs$ pointwise.

theorem SimplicialComplex.fixes_along_chain_of_nonstuttering {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (hthin : X.IsThin) (f : X.Morphism X.toSimplicialComplex) (hf : f.IsChamberMap) (hfF : f.PreservesFacets) (cs : List (Finset V)) (hne : cs ≠ []) (hchain : List.IsChain X.Adjacent cs) (hall : ∀ C ∈ cs, X.IsMaximal C) (hfix_head : ∀ v ∈ cs.head hne, f.toFun v = v) (hns : List.IsChain (fun (x1 x2 : Finset V) => x1 ≠ x2) (List.map (fun (C : Finset V) => Finset.image f.toFun C) cs)) (C : Finset V) : C ∈ cs → ∀ v ∈ C, f.toFun v = v

Variant of thin_fixes_next_chamber extended along an entire non-stuttering chain.

theorem SimplicialComplex.uniqueness_lemma_book {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (hthin : X.IsThin) (f : X.Morphism X.toSimplicialComplex) (hf : f.IsChamberMap) (hfF : f.PreservesFacets) (C₀ : Finset V) (_hC₀ : X.IsMaximal C₀) (hfix : ∀ v ∈ C₀, f.toFun v = v) (γ : Gallery X.toSimplicialComplex) (hstart : γ.chambers.head? = some C₀) : GalleryStuttersUnder γ.chambers f.toFun ∨ FixesAllPointwise γ.chambers f.toFun

Book uniqueness lemma (3.3/3.5), internal form: in a thin chamber complex, if $f$ is a facet-preserving chamber map fixing $C_0$ pointwise, then along any gallery starting at $C_0$, either the $f$-image stutters or $f$ fixes every chamber pointwise.

theorem SimplicialComplex.thin_fixes_next_chamber_no_pfacets {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (hthin : X.IsThin) (f : X.Morphism X.toSimplicialComplex) (hf : f.IsChamberMap) {C₁ C₂ : Finset V} (hadj : X.Adjacent C₁ C₂) (hfix₁ : ∀ v ∈ C₁, f.toFun v = v) (hne : Finset.image f.toFun C₂ ≠ C₁) (v : V) : v ∈ C₂ → f.toFun v = v

Variant of thin_fixes_next_chamber not requiring PreservesFacets — the facet property of $f(C_2)$ is derived from cardinalities.

theorem SimplicialComplex.fixes_along_chain_no_pfacets {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (hthin : X.IsThin) (f : X.Morphism X.toSimplicialComplex) (hf : f.IsChamberMap) (cs : List (Finset V)) (hne : cs ≠ []) (hchain : List.IsChain X.Adjacent cs) (hall : ∀ C ∈ cs, X.IsMaximal C) (hfix_head : ∀ v ∈ cs.head hne, f.toFun v = v) (hns : List.IsChain (fun (x1 x2 : Finset V) => x1 ≠ x2) (List.map (fun (C : Finset V) => Finset.image f.toFun C) cs)) (C : Finset V) : C ∈ cs → ∀ v ∈ C, f.toFun v = v

Chain variant of thin_fixes_next_chamber_no_pfacets — propagates pointwise fixing along a non-stuttering chain without assuming PreservesFacets.

theorem SimplicialComplex.uniqueness_lemma {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (hthin : X.IsThin) (f : X.Morphism X.toSimplicialComplex) (hf : f.IsChamberMap) (C₀ : Finset V) (_hC₀ : X.IsMaximal C₀) (hfix : ∀ v ∈ C₀, f.toFun v = v) (γ : Gallery X.toSimplicialComplex) (hstart : γ.chambers.head? = some C₀) : GalleryStuttersUnder γ.chambers f.toFun ∨ FixesAllPointwise γ.chambers f.toFun

Uniqueness lemma (no facet-preservation hypothesis): in a thin chamber complex, if $f$ is a chamber map fixing $C_0$ pointwise, then along any gallery starting at $C_0$, either $f$'s image stutters or $f$ fixes every chamber of the gallery pointwise.