Documentation

TauCeti.KnotTheory.Grid.Commutation.Relabeling

Relabeling and grid commutation arcs #

This file records the relabeling bookkeeping for the row and column arcs used in grid commutation hypotheses. A column relabeling only renames the columns, so it transports column arcs and column non-interleaving by applying the inverse column permutation to the labels. Dually, a row relabeling only renames the rows, so it transports row arcs and row non-interleaving by the inverse row permutation.

The deliberately absent mixed statements are the point: an arbitrary row permutation need not preserve the cyclic order in the row coordinate, so it does not transport column arcs to column arcs; likewise for arbitrary column permutations and row arcs. The swap corollaries specialize the permutation formulas to the elementary grid commutations used later.

Main results #

References #

This supplies a prerequisite for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.5, "Invariance over 𝔽₂. Grid moves = commutation + (de)stabilization", where commutation maps are attached to elementary row and column commutations. The conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

source
@[simp]
theorem TauCeti.GridDiagram.columnArc_relabelColumns {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) (c : Fin n) :
(relabelColumns κ G).columnArc c = G.columnArc ((Equiv.symm κ) c)

Column relabeling only renames the column whose vertical arc is being read.

source
theorem TauCeti.GridDiagram.mem_columnArc_relabelColumns {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) (c r : Fin n) :
r ∈ (relabelColumns κ G).columnArc c ↔ r ∈ G.columnArc ((Equiv.symm κ) c)

Membership in a column arc after column relabeling is membership in the old arc with the inverse column label.

source
@[simp]
theorem TauCeti.GridDiagram.columnArc_swapColumns {n : ℕ} (G : GridDiagram n) (a b c : Fin n) :
(swapColumns a b G).columnArc c = G.columnArc ((Equiv.swap a b) c)

A column swap renames the column whose vertical arc is being read.

source
theorem TauCeti.GridDiagram.mem_columnArc_swapColumns {n : ℕ} (G : GridDiagram n) (a b c r : Fin n) :
r ∈ (swapColumns a b G).columnArc c ↔ r ∈ G.columnArc ((Equiv.swap a b) c)

Membership in a column arc after a column swap is membership in the old arc with the swapped column label.

source
@[simp]
theorem TauCeti.GridDiagram.columnsNoninterleaving_relabelColumns {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) (a b : Fin n) :
(relabelColumns κ G).ColumnsNoninterleaving a b ↔ G.ColumnsNoninterleaving ((Equiv.symm κ) a) ((Equiv.symm κ) b)

Column non-interleaving is transported by column relabeling through the inverse labels.

source
@[simp]
theorem TauCeti.GridDiagram.columnsNoninterleaving_swapColumns {n : ℕ} (G : GridDiagram n) (a b c d : Fin n) :
(swapColumns a b G).ColumnsNoninterleaving c d ↔ G.ColumnsNoninterleaving ((Equiv.swap a b) c) ((Equiv.swap a b) d)

Column non-interleaving is transported by a column swap through the swapped labels.

source
@[simp]
theorem TauCeti.GridDiagram.rowArc_relabelRows {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) (r : Fin n) :
(relabelRows ρ G).rowArc r = G.rowArc ((Equiv.symm ρ) r)

Row relabeling only renames the row whose horizontal arc is being read.

source
theorem TauCeti.GridDiagram.mem_rowArc_relabelRows {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) (r c : Fin n) :
c ∈ (relabelRows ρ G).rowArc r ↔ c ∈ G.rowArc ((Equiv.symm ρ) r)

Membership in a row arc after row relabeling is membership in the old arc with the inverse row label.

source
@[simp]
theorem TauCeti.GridDiagram.rowArc_swapRows {n : ℕ} (G : GridDiagram n) (a b r : Fin n) :
(swapRows a b G).rowArc r = G.rowArc ((Equiv.swap a b) r)

A row swap renames the row whose horizontal arc is being read.

source
theorem TauCeti.GridDiagram.mem_rowArc_swapRows {n : ℕ} (G : GridDiagram n) (a b r c : Fin n) :
c ∈ (swapRows a b G).rowArc r ↔ c ∈ G.rowArc ((Equiv.swap a b) r)

Membership in a row arc after a row swap is membership in the old arc with the swapped row label.

source
@[simp]
theorem TauCeti.GridDiagram.rowsNoninterleaving_relabelRows {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) (a b : Fin n) :
(relabelRows ρ G).RowsNoninterleaving a b ↔ G.RowsNoninterleaving ((Equiv.symm ρ) a) ((Equiv.symm ρ) b)

Row non-interleaving is transported by row relabeling through the inverse labels.

source
@[simp]
theorem TauCeti.GridDiagram.rowsNoninterleaving_swapRows {n : ℕ} (G : GridDiagram n) (a b c d : Fin n) :
(swapRows a b G).RowsNoninterleaving c d ↔ G.RowsNoninterleaving ((Equiv.swap a b) c) ((Equiv.swap a b) d)

Row non-interleaving is transported by a row swap through the swapped labels.