Documentation

TauCeti.KnotTheory.Grid.Differential.Square.Intermediates

Intermediate states in two column swaps #

The support of the square of the fully blocked grid differential is contained in the states reached from x by two nontrivial column swaps. This file records the exact finite set of possible intermediate states between a source x and a target z: the intersection of their one-swap neighbour sets.

For a diagonal path x → y → x, this set is exactly the full one-swap neighbour set of x. For a nondiagonal path, conjugating the first transposition by the second gives another factorization through a distinct intermediate state. Consequently every nonempty nondiagonal intermediate set has at least two elements.

These state-level factorizations do not pair rectangles: the juxtaposition argument must also track which of the two rectangles with given corners is used and whether its domain avoids the markings. They provide the finite diagonal/nondiagonal case split on which that argument is built.

Main definitions #

Main results #

References #

The square-zero proof (TauCeti.KnotTheory.Grid.Differential.Square.Zero) pairs juxtaposed rectangle decompositions as in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

source
def TauCeti.GridState.twoStepColumnSwapIntermediates {n : ℕ} (x z : GridState n) :
Finset (GridState n)

The grid states that can occur between x and z in a path of two nontrivial column swaps.

The definition is symmetric in the endpoints: an intermediate state is a one-swap neighbour of both.

Instances For
    source
    @[simp]
    theorem TauCeti.GridState.mem_twoStepColumnSwapIntermediates {n : ℕ} {x y z : GridState n} :
    y ∈ x.twoStepColumnSwapIntermediates z ↔ y ∈ x.columnSwapNeighbors ∧ y ∈ z.columnSwapNeighbors

    A state is an intermediate between x and z exactly when it is a one-swap neighbour of both endpoints.

    source
    theorem TauCeti.GridState.mem_twoStepColumnSwapIntermediates_iff_mem_columnSwapNeighbors {n : ℕ} {x y z : GridState n} :
    y ∈ x.twoStepColumnSwapIntermediates z ↔ y ∈ x.columnSwapNeighbors ∧ z ∈ y.columnSwapNeighbors

    A state is an intermediate between x and z exactly when it is reached from x by one nontrivial column swap and z is reached from it by another.

    source
    theorem TauCeti.GridState.mem_twoStepColumnSwapIntermediates_iff_exists_swaps {n : ℕ} {x y z : GridState n} :
    y ∈ x.twoStepColumnSwapIntermediates z ↔ ∃ (a : Fin n) (b : Fin n) (c : Fin n) (d : Fin n), a ≠ b ∧ c ≠ d ∧ y = swapColumns a b x ∧ z = swapColumns c d y

    An expanded membership form for the intermediate states in a two-swap path.

    source
    theorem TauCeti.GridState.twoStepColumnSwapIntermediates_comm {n : ℕ} (x z : GridState n) :
    x.twoStepColumnSwapIntermediates z = z.twoStepColumnSwapIntermediates x

    Swapping the two endpoints does not change their set of two-step intermediate states.

    source
    @[simp]
    theorem TauCeti.GridState.twoStepColumnSwapIntermediates_self {n : ℕ} (x : GridState n) :
    x.twoStepColumnSwapIntermediates x = x.columnSwapNeighbors

    The possible intermediate states between x and itself are exactly its one-swap neighbours.

    source
    theorem TauCeti.GridState.nonempty_twoStepColumnSwapIntermediates_iff {n : ℕ} {x z : GridState n} :
    (x.twoStepColumnSwapIntermediates z).Nonempty ↔ z ∈ x.twoStepColumnSwapNeighbors

    There is a two-step intermediate between x and z exactly when z is a two-step column-swap neighbour of x.

    source
    theorem TauCeti.GridState.swapColumns_mem_twoStepColumnSwapIntermediates_ne {n : ℕ} (x : GridState n) {a b c d : Fin n} (hab : a ≠ b) (hcd : c ≠ d) (hpairs : s(a, b) ≠ s(c, d)) :
    swapColumns c d x ∈ x.twoStepColumnSwapIntermediates (swapColumns c d (swapColumns a b x)) ∧ swapColumns c d x ≠ swapColumns a b x

    Applying the second of two distinct nontrivial column swaps first produces a distinct intermediate state.

    The remaining swap is the conjugate of the first one.

    source
    theorem TauCeti.GridState.exists_mem_twoStepColumnSwapIntermediates_ne_of_mem_of_ne {n : ℕ} {x y z : GridState n} (hy : y ∈ x.twoStepColumnSwapIntermediates z) (hzx : z ≠ x) :
    ∃ y' ∈ x.twoStepColumnSwapIntermediates z, y' ≠ y

    Every intermediate state on a nondiagonal two-step path has a distinct alternative intermediate state.

    source
    theorem TauCeti.GridState.one_lt_card_twoStepColumnSwapIntermediates {n : ℕ} {x z : GridState n} (hz : z ∈ x.twoStepColumnSwapNeighbors) (hzx : z ≠ x) :
    1 < (x.twoStepColumnSwapIntermediates z).card

    A nondiagonal two-step neighbour has at least two possible intermediate states.