Two-step rectangle decompositions

A two-step term in the square of the grid differential consists of a rectangle from x to an intermediate grid state and a second rectangle from that state to z. This file packages such a factorization as GridRectangleDecomposition, the shared object on which the disjoint, overlapping and annular cases of the square-zero argument all operate.

Such a factorization is determined by the ordered side columns of its two rectangles: the intermediate state is the source with the first pair of columns swapped, and an oriented rectangle between two given states is determined by its side columns.

Main definitions

• TauCeti.GridRectangleDecomposition: two composable oriented grid rectangles, the two-step decomposition TauCeti.GridTwoStepDecomposition with both steps rectangles.

Main results

• TauCeti.GridRectangleDecomposition.ext: a decomposition is determined by the ordered side columns of its two rectangles.
• TauCeti.GridRectangleDecomposition.sides_injective: the same statement as injectivity of the ordered quadruple of side columns.
• TauCeti.GridRectangleDecomposition.target_apply_of_notMem_sideColumns: away from the four side columns the target of a decomposition agrees with its source.
• TauCeti.GridRectangleDecomposition.transpose and transposeEquiv: diagonal reflection of both constituent rectangles gives an involutive equivalence between decompositions of the original and transposed endpoint states.
• TauCeti.GridRectangleDecomposition.target_mem_twoStepColumnSwapNeighbors: the target of a decomposition is reached from its source by two nontrivial column transpositions.
• TauCeti.GridRectangleDecomposition.sides_of_middle_eq_swapRows: when the intermediate state swaps two rows of the source, the side columns of both rectangles are read off from the rows of their corners.

References

The decomposition pairing follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

@[reducible, inline]

abbrev TauCeti.GridRectangleDecomposition {n : ℕ} (x z : GridState n) : Type

A decomposition of a two-step rectangle domain from x to z through an intermediate grid state.

theorem TauCeti.GridRectangleDecomposition.ext {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} (hfirstLeft : D.first.left = E.first.left) (hfirstRight : D.first.right = E.first.right) (hsecondLeft : D.second.left = E.second.left) (hsecondRight : D.second.right = E.second.right) : D = E

Two rectangle decompositions are equal when their ordered side columns agree: the first pair already determines the intermediate state.

theorem TauCeti.GridRectangleDecomposition.ext_iff {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} : D = E ↔ D.first.left = E.first.left ∧ D.first.right = E.first.right ∧ D.second.left = E.second.left ∧ D.second.right = E.second.right

theorem TauCeti.GridRectangleDecomposition.sides_injective {n : ℕ} (x z : GridState n) : Function.Injective fun (D : GridRectangleDecomposition x z) => (D.first.left, D.first.right, D.second.left, D.second.right)

A two-step rectangle decomposition is determined by the ordered quadruple of side columns of its two rectangles.

@[instance_reducible]

instance TauCeti.GridRectangleDecomposition.instDecidableEq {n : ℕ} {x z : GridState n} : DecidableEq (GridRectangleDecomposition x z)

Two-step rectangle decompositions between fixed states have decidable equality: such a decomposition is determined by its four side columns.

theorem TauCeti.GridRectangleDecomposition.target_apply_of_notMem_sideColumns {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) {c : Fin n} (h₁ : c ∉ D.first.sideColumns) (h₂ : c ∉ D.second.sideColumns) : z.toPerm c = x.toPerm c

Away from the four side columns of a two-step decomposition, its target state agrees with its source state: neither rectangle moves such a column.

def TauCeti.GridRectangleDecomposition.transpose {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : GridRectangleDecomposition x.transpose z.transpose

The diagonal reflection of a two-step rectangle decomposition. It reflects both constituent rectangles and the intermediate state, and hence gives a decomposition between the transposed endpoint states.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_middle {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.middle = D.middle.transpose

The intermediate state of a transposed decomposition is the transposed intermediate state.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_first {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : ⟨D.transpose.middle, D.transpose.first⟩ = ⟨D.middle.transpose, D.first.transpose⟩

The intermediate state and first rectangle of a transposed decomposition are the transposes of the original intermediate state and first rectangle. They are paired because the rectangle's target is indexed by the intermediate state.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_second {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : ⟨D.transpose.middle, D.transpose.second⟩ = ⟨D.middle.transpose, D.second.transpose⟩

The intermediate state and second rectangle of a transposed decomposition are the transposes of the original intermediate state and second rectangle. They are paired because the rectangle's source is indexed by the intermediate state.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_first_left {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.first.left = D.first.bottom

The first rectangle of a transposed decomposition has the original initial corner row as its initial side column.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_first_right {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.first.right = D.first.top

The first rectangle of a transposed decomposition has the original terminal corner row as its terminal side column.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_first_bottom {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.first.bottom = D.first.left

The first rectangle of a transposed decomposition has the original initial side column as its initial corner row.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_first_top {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.first.top = D.first.right

The first rectangle of a transposed decomposition has the original terminal side column as its terminal corner row.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_second_left {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.second.left = D.second.bottom

The second rectangle of a transposed decomposition has the original initial corner row as its initial side column.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_second_right {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.second.right = D.second.top

The second rectangle of a transposed decomposition has the original terminal corner row as its terminal side column.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_second_bottom {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.second.bottom = D.second.left

The second rectangle of a transposed decomposition has the original initial side column as its initial corner row.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_second_top {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.second.top = D.second.right

The second rectangle of a transposed decomposition has the original terminal side column as its terminal corner row.

@[simp]

theorem TauCeti.GridRectangleDecomposition.isEmpty_transpose_first {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.first.IsEmpty ↔ D.first.IsEmpty

The first rectangle of a transposed decomposition is empty exactly when the original first rectangle is.

@[simp]

theorem TauCeti.GridRectangleDecomposition.isEmpty_transpose_second {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.second.IsEmpty ↔ D.second.IsEmpty

The second rectangle of a transposed decomposition is empty exactly when the original second rectangle is.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transpose_transpose {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.transpose.transpose = D

Reflecting a two-step rectangle decomposition twice recovers the original decomposition.

def TauCeti.GridRectangleDecomposition.transposeEquiv {n : ℕ} (x z : GridState n) : GridRectangleDecomposition x z ≃ GridRectangleDecomposition x.transpose z.transpose

Diagonal reflection as an equivalence between decompositions of the original and reflected endpoint states. Its inverse is again diagonal reflection.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transposeEquiv_apply {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : (transposeEquiv x z) D = D.transpose

The decomposition reflection equivalence acts by diagonal reflection.

@[simp]

theorem TauCeti.GridRectangleDecomposition.transposeEquiv_symm_apply {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x.transpose z.transpose) : (transposeEquiv x z).symm D = D.transpose

The inverse of the decomposition reflection equivalence also acts by diagonal reflection.

theorem TauCeti.GridRectangleDecomposition.target_mem_twoStepColumnSwapNeighbors {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : z ∈ x.twoStepColumnSwapNeighbors

The target of a two-step rectangle decomposition is a two-step column-swap neighbour of its source: each of the two rectangles transposes its pair of distinct side columns.

theorem TauCeti.GridRectangleDecomposition.sides_of_middle_eq_swapRows {n : ℕ} {x z : GridState n} {E : GridRectangleDecomposition x z} {a b c d e f : Fin n} (hmiddle : E.middle = GridState.swapRows (x.toPerm a) (x.toPerm b) x) (hfirstBottom : E.first.bottom = x.toPerm c) (hfirstTop : E.first.top = x.toPerm d) (hsecondBottom : E.second.bottom = x.toPerm e) (hsecondTop : E.second.top = x.toPerm f) : E.first.left = c ∧ E.first.right = d ∧ E.second.left = (Equiv.swap a b) e ∧ E.second.right = (Equiv.swap a b) f

The side columns of a decomposition whose intermediate state swaps two rows of the source, read off from the rows of its corners.