def
Gallery.CrossesWallAt
{V : Type u_1}
[DecidableEq V]
{K : ChamberComplex V}
(g : Gallery K.toSimplicialComplex)
(f : K.Folding)
(i : Fin (g.chambers.length - 1))
:
The gallery $g$ crosses the wall of $f$ at edge $i$ if $g_i$ and $g_{i+1}$ lie on opposite sides of the wall.
Instances For
def
Gallery.WallCrossings
{V : Type u_1}
[DecidableEq V]
{K : ChamberComplex V}
(g : Gallery K.toSimplicialComplex)
(f : K.Folding)
:
The set of edges along $g$ at which the gallery crosses the wall of $f$.
Instances For
structure
ChamberComplex.WallCrossingProperties
{V : Type u_1}
[DecidableEq V]
(K : ChamberComplex V)
:
Wall-crossing properties: in a minimal gallery, two same-side endpoints give no wall crossings, opposite-side endpoints give at least one wall crossing, and minimal galleries cross each wall at most once.
- both_fixed_no_crossing (f : K.Folding) (C D : Finset V) : K.IsMaximal C → K.IsMaximal D → Finset.image f.morph.toFun C = C → Finset.image f.morph.toFun D = D → ∀ (g : Gallery K.toSimplicialComplex), g.Connects C D → g.length = galleryDist K.toSimplicialComplex C D → g.WallCrossings f = ∅
- both_moved_no_crossing (f : K.Folding) (C D : Finset V) : K.IsMaximal C → K.IsMaximal D → Finset.image f.morph.toFun C ≠ C → Finset.image f.morph.toFun D ≠ D → ∀ (g : Gallery K.toSimplicialComplex), g.Connects C D → g.length = galleryDist K.toSimplicialComplex C D → g.WallCrossings f = ∅
- opposite_at_least_one (f : K.Folding) (C D : Finset V) : K.IsMaximal C → K.IsMaximal D → OppositeSides f C D → ∀ (g : Gallery K.toSimplicialComplex), g.Connects C D → ∃ (i : Fin (g.chambers.length - 1)), i ∈ g.WallCrossings f
- at_most_one_crossing (f : K.Folding) (C D : Finset V) : K.IsMaximal C → K.IsMaximal D → ∀ (g : Gallery K.toSimplicialComplex), g.Connects C D → g.length = galleryDist K.toSimplicialComplex C D → ∀ (i j : Fin (g.chambers.length - 1)), i ∈ g.WallCrossings f → j ∈ g.WallCrossings f → i = j