Documentation

TauCeti.KnotTheory.Grid.Differential.Square.Support

Two-step support for the fully blocked grid differential #

This file records the finite support bookkeeping for applying the fully blocked grid differential twice. The one-step support theorem says that ∂ x is supported on the states obtained from x by one nontrivial column transposition. Applying that theorem again gives a small ambient set for ∂ (∂ x): the union of the column-swap neighbours of those neighbours.

The ∂² = 0 identity is not asserted here. These lemmas only isolate the finite target set on which the rectangle-pairing argument checks cancellation.

Main results #

References #

The one-step column-transposition support condition follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 3 and 4; this file packages its direct two-step consequence.

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

The grid states reachable from x by two nontrivial column transpositions.

This is the finite ambient set for the support of ∂ (∂ x) before the rectangle-pairing argument proves that all of its coefficients cancel.

Instances For
    source
    @[simp]
    theorem TauCeti.GridState.mem_twoStepColumnSwapNeighbors {n : ℕ} {x z : GridState n} :
    z ∈ x.twoStepColumnSwapNeighbors ↔ ∃ y ∈ x.columnSwapNeighbors, z ∈ y.columnSwapNeighbors

    Membership in the two-step column-swap neighbour set.

    source
    theorem TauCeti.GridState.mem_twoStepColumnSwapNeighbors_iff_exists_swaps {n : ℕ} {x z : GridState n} :
    z ∈ x.twoStepColumnSwapNeighbors ↔ ∃ (y : GridState n) (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 two-step column-swap neighbour set.

    source
    theorem TauCeti.GridState.card_twoStepColumnSwapNeighbors_le {n : ℕ} (x : GridState n) :
    x.twoStepColumnSwapNeighbors.card ≤ n.choose 2 ^ 2

    The two-step neighbour set has at most (n.choose 2) ^ 2 states.

    source
    theorem TauCeti.GridState.twoStepColumnSwapNeighbors_eq_empty_of_le_one {n : ℕ} (x : GridState n) (hn : n ≤ 1) :
    x.twoStepColumnSwapNeighbors = ∅

    In grid size at most 1, no state is reachable by two nontrivial column swaps.

    source
    @[simp]
    theorem TauCeti.GridState.twoStepColumnSwapNeighbors_eq_empty_of_zero (x : GridState 0) :
    x.twoStepColumnSwapNeighbors = ∅

    In grid size 0, no state is reachable by two nontrivial column swaps.

    source
    @[simp]
    theorem TauCeti.GridState.twoStepColumnSwapNeighbors_eq_empty_of_one (x : GridState 1) :
    x.twoStepColumnSwapNeighbors = ∅

    In grid size 1, no state is reachable by two nontrivial column swaps.

    source
    theorem TauCeti.GridDiagram.fullyBlockedDifferential_sq_support_subset_biUnion {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) :
    (G.fullyBlockedDifferential (G.fullyBlockedDifferential c)).support ⊆ c.support.biUnion fun (x : GridState n) => x.twoStepColumnSwapNeighbors

    The support of ∂ (∂ c) is contained in the union of the two-step neighbour sets attached to the states appearing in the input chain.

    source
    theorem TauCeti.GridDiagram.fullyBlockedDifferential_sq_apply_eq_zero_of_notMem_support_biUnion {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) {z : GridState n} (hz : z ∉ c.support.biUnion fun (x : GridState n) => x.twoStepColumnSwapNeighbors) :
    (G.fullyBlockedDifferential (G.fullyBlockedDifferential c)) z = 0

    If a state is not in any two-step neighbour set attached to the input support, its coefficient in ∂ (∂ c) is zero.

    source
    theorem TauCeti.GridDiagram.fullyBlockedDifferential_sq_support_card_le {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) :
    (G.fullyBlockedDifferential (G.fullyBlockedDifferential c)).support.card ≤ c.support.card * n.choose 2 ^ 2

    The support of ∂ (∂ c) has cardinality at most c.support.card * (n.choose 2) ^ 2.

    source
    theorem TauCeti.GridDiagram.fullyBlockedDifferential_sq_single_support_subset {n : ℕ} (G : GridDiagram n) (x : GridState n) :
    (G.fullyBlockedDifferential (G.fullyBlockedDifferential (Finsupp.single x 1))).support ⊆ x.twoStepColumnSwapNeighbors

    The support of ∂ (∂ x) is contained in the states reachable from x by two column transpositions. This is the finite search space for the rectangle-pairing proof of ∂² = 0 on generators.

    source
    theorem TauCeti.GridDiagram.fullyBlockedDifferential_sq_single_apply_eq_zero_of_notMem_twoStep {n : ℕ} (G : GridDiagram n) (x : GridState n) {z : GridState n} (hz : z ∉ x.twoStepColumnSwapNeighbors) :
    (G.fullyBlockedDifferential (G.fullyBlockedDifferential (Finsupp.single x 1))) z = 0

    If a state is not reachable by two column swaps from x, its coefficient in ∂ (∂ x) is zero.

    source
    theorem TauCeti.GridDiagram.fullyBlockedDifferential_sq_single_support_card_le {n : ℕ} (G : GridDiagram n) (x : GridState n) :
    (G.fullyBlockedDifferential (G.fullyBlockedDifferential (Finsupp.single x 1))).support.card ≤ n.choose 2 ^ 2

    The support of ∂ (∂ x) has at most (n.choose 2) ^ 2 states.