A grid rectangle move is a column transposition

An oriented rectangle R : GridRectangleBetween x y records the two side columns at which the target state y differs from the source state x: at the initial side column y reads the row x uses at the terminal side, and vice versa, while the two states agree away from the two side columns. That is exactly the effect of swapping the two side columns of x, so the target state is the column transposition x.swapColumns R.left R.right.

This file makes that identification precise and draws the point-set consequences: the two states share all but two of their occupied grid points, and each occupied grid point they do not share is one of the four corners of the rectangle. The shared grid points are exactly the intersection of the two point sets, which has n - 2 elements. These are the bookkeeping facts a Maslov or Alexander grading-change computation across a rectangle rests on, and they let later ∂² = 0-style arguments reason about x and y through a single transposition.

Main results

• TauCeti.GridRectangleBetween.target_eq_swapColumns: the target state of a rectangle is the source state with the two side columns swapped.
• TauCeti.GridRectangleBetween.target_eq_swapRows: equivalently, the source state with the two rows those columns occupy swapped.
• TauCeti.GridRectangleBetween.nonempty_iff: oriented rectangles between x and y exist exactly when y is a column transposition of x.
• TauCeti.GridRectangleBetween.source_eq_swapColumns: the symmetric statement recovering the source from the target.
• TauCeti.GridRectangleBetween.mem_pointSet_inter_iff: a grid point is shared by the two states exactly when it belongs to the source and avoids the two side columns -- the rectangle specialization of GridState.mem_pointSet_inter_swapColumns_iff from Diagram.lean.
• TauCeti.GridRectangleBetween.source_pointSet_eq, TauCeti.GridRectangleBetween.target_pointSet_eq: each state's point set is the shared part together with its own two corners.
• TauCeti.GridRectangleBetween.card_pointSet_inter: the two states share exactly n - 2 grid points.
• TauCeti.GridState.rectangle_induction_on: any two grid states are joined by a sequence of rectangle moves.

References

The column-transposition picture of a rectangle move follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.

theorem TauCeti.GridRectangleBetween.target_apply {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (c : Fin n) : y.toPerm c = x.toPerm ((Equiv.swap R.left R.right) c)

Pointwise form of the column-transposition identity: at each column the target state reads the row the source state reads at the swapped column.

theorem TauCeti.GridRectangleBetween.target_eq_swapColumns {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : y = GridState.swapColumns R.left R.right x

The target state of an oriented rectangle is the source state with its two side columns swapped. The rectangle's defining equations -- the two side columns exchange their rows and the other columns are unchanged -- are precisely the action of the column transposition.

theorem TauCeti.GridRectangleBetween.target_eq_swapRows {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : y = GridState.swapRows (x.toPerm R.left) (x.toPerm R.right) x

The target state of an oriented rectangle is also the source state with the two rows occupied by its side columns swapped: a grid state is a bijection from columns to rows, so exchanging the two side columns exchanges exactly the two rows they occupy.

def TauCeti.GridRectangleBetween.ofSwapColumns {n : ℕ} (x y : GridState n) (a b : Fin n) (hab : a ≠ b) (h : y = GridState.swapColumns a b x) : GridRectangleBetween x y

The oriented rectangle associated to an equality expressing the target as a nontrivial column swap of the source.

@[simp]

theorem TauCeti.GridRectangleBetween.ofSwapColumns_left {n : ℕ} (x y : GridState n) (a b : Fin n) (hab : a ≠ b) (h : y = GridState.swapColumns a b x) : (ofSwapColumns x y a b hab h).left = a

The initial side of the rectangle constructed from a column-swap equality.

@[simp]

theorem TauCeti.GridRectangleBetween.ofSwapColumns_right {n : ℕ} (x y : GridState n) (a b : Fin n) (hab : a ≠ b) (h : y = GridState.swapColumns a b x) : (ofSwapColumns x y a b hab h).right = b

The terminal side of the rectangle constructed from a column-swap equality.

@[simp]

theorem TauCeti.GridRectangleBetween.ofSwapColumns_bottom {n : ℕ} (x y : GridState n) (a b : Fin n) (hab : a ≠ b) (h : y = GridState.swapColumns a b x) : (ofSwapColumns x y a b hab h).bottom = x.toPerm a

The lower side of the rectangle constructed from a column-swap equality.

@[simp]

theorem TauCeti.GridRectangleBetween.ofSwapColumns_top {n : ℕ} (x y : GridState n) (a b : Fin n) (hab : a ≠ b) (h : y = GridState.swapColumns a b x) : (ofSwapColumns x y a b hab h).top = x.toPerm b

The upper side of the rectangle constructed from a column-swap equality.

@[simp]

theorem TauCeti.GridRectangleBetween.ofSwapColumns_toGridRectangle {n : ℕ} (x y : GridState n) (a b : Fin n) (hab : a ≠ b) (h : y = GridState.swapColumns a b x) : (ofSwapColumns x y a b hab h).toGridRectangle = { left := a, right := b, bottom := x.toPerm a, top := x.toPerm b }

The toroidal rectangle underlying the rectangle constructed from a column-swap equality.

theorem TauCeti.GridRectangleBetween.nonempty_iff {n : ℕ} {x y : GridState n} : Nonempty (GridRectangleBetween x y) ↔ ∃ (a : Fin n) (b : Fin n), a ≠ b ∧ y = GridState.swapColumns a b x

Oriented rectangles between x and y exist exactly when y is a column transposition of x. A rectangle realizes its side columns as a transposition taking x to y, and conversely a column transposition exhibits an oriented rectangle on those two columns.

theorem TauCeti.GridRectangleBetween.source_eq_swapColumns {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : x = GridState.swapColumns R.left R.right y

The source state of an oriented rectangle is the target state with its two side columns swapped: swapping the same pair of columns twice is the identity.

theorem TauCeti.GridRectangleBetween.target_toPerm_eq {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : y.toPerm = Equiv.trans (Equiv.swap R.left R.right) x.toPerm

The underlying permutation of the target state is the source permutation precomposed with the transposition of the two side columns.

theorem TauCeti.GridRectangleBetween.mem_target_pointSet_iff {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p : Fin n × Fin n) : p ∈ y.pointSet ↔ ((Equiv.swap R.left R.right) p.1, p.2) ∈ x.pointSet

A grid point lies in the target state exactly when its column-transposed grid point lies in the source state.

theorem TauCeti.GridRectangleBetween.mem_pointSet_inter_iff {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p : Fin n × Fin n) : p ∈ x.pointSet ∩ y.pointSet ↔ p ∈ x.pointSet ∧ p.1 ≠ R.left ∧ p.1 ≠ R.right

The two side columns carry the four corners of a rectangle, so a grid point that the two states share must avoid both side columns. Conversely, away from the side columns the two states agree, so every source grid point off the side columns is shared.

theorem TauCeti.GridRectangleBetween.left_bottom_notMem_inter {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : (R.left, R.bottom) ∉ x.pointSet ∩ y.pointSet

The lower-left corner is not shared with the target state: it sits on a side column.

theorem TauCeti.GridRectangleBetween.right_top_notMem_inter {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : (R.right, R.top) ∉ x.pointSet ∩ y.pointSet

The upper-right corner is not shared with the target state: it sits on a side column.

theorem TauCeti.GridRectangleBetween.left_top_notMem_inter {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : (R.left, R.top) ∉ x.pointSet ∩ y.pointSet

The upper-left target corner is not shared with the source state: it sits on a side column.

theorem TauCeti.GridRectangleBetween.right_bottom_notMem_inter {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : (R.right, R.bottom) ∉ x.pointSet ∩ y.pointSet

The lower-right target corner is not shared with the source state: it sits on a side column.

theorem TauCeti.GridRectangleBetween.source_pointSet_eq {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : x.pointSet = insert (R.left, R.bottom) (insert (R.right, R.top) (x.pointSet ∩ y.pointSet))

The source state's point set is its shared intersection with the target point set together with the two source corners (R.left, R.bottom) and (R.right, R.top).

theorem TauCeti.GridRectangleBetween.target_pointSet_eq {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : y.pointSet = insert (R.left, R.top) (insert (R.right, R.bottom) (x.pointSet ∩ y.pointSet))

The target state's point set is the shared part together with its own two corners.

theorem TauCeti.GridRectangleBetween.card_pointSet_inter {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : (x.pointSet ∩ y.pointSet).card = n - 2

The source and target states share exactly n - 2 grid points: all of the source's n grid points except its two corners.

theorem TauCeti.GridState.rectangle_induction_on {n : ℕ} {P : GridState n → Prop} (x₀ : GridState n) (h₀ : P x₀) (h : ∀ (x y : GridState n) (a : GridRectangleBetween x y), P x → P y) (x : GridState n) : P x

Any two grid states are joined by rectangle moves. A property of grid states that holds at one state x₀ and passes from the source to the target of every oriented rectangle holds at every state: every grid state is reached from x₀ by a sequence of column transpositions, and each column transposition is a rectangle move.