Link components of a grid diagram

The O- and X-markings of a grid diagram determine an oriented link combinatorially. Starting at the O-marking in column c, follow its horizontal segment to the X-marking in the same row, then follow the vertical segment to the O-marking in that column. On column labels this is the permutation

c ↦ X⁻¹(O(c)).

Its cycles are exactly the link components. This file packages that permutation, its cycle decomposition and component count, and the predicate that the represented link is a knot. The grid-diagram disjointness condition makes the component permutation fixed-point-free, so Mathlib's cycle decomposition accounts for every marking, and the component count is also the number of orbits TauCeti.orbitCount of the component permutation.

On a knot grid the component permutation is a single cycle through all columns, so it leads from any base column to any other column; the least number of steps is the traversal index TauCeti.GridDiagram.IsKnot.traversalIndex, which is less than the grid number and injective in the target column.

Row relabeling leaves the component permutation unchanged, while column relabeling conjugates it. Consequently the cycle type, component count, and knot predicate are preserved by both relabelings, as well as by diagonal reflection, half-turn rotation, and exchanging O with X.

Main definitions

• TauCeti.GridDiagram.componentPerm: the permutation obtained by following one horizontal and one vertical grid segment.
• TauCeti.GridDiagram.componentCycles: the cycle factors representing the link components.
• TauCeti.GridDiagram.componentCycleType: the multiset of component sizes.
• TauCeti.GridDiagram.componentCount: the number of represented link components.
• TauCeti.GridDiagram.IsKnot: the represented link has exactly one component.
• TauCeti.GridDiagram.IsKnot.traversalIndex: on a knot grid, the number of steps of the component permutation from a base column to a column.

References

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.1, "Grid diagrams and grid states", and supplies the knot-versus-link distinction needed by the later knot invariant τ in Lane G.6 and the links stage in Lane G.9. The component traversal follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

def TauCeti.GridDiagram.componentPerm {n : ℕ} (G : GridDiagram n) : Equiv.Perm (Fin n)

The permutation of O-marking columns obtained by traversing one horizontal segment from O to X, then the vertical segment back to O.

Thus componentPerm G c = G.X.transpose (G.O c). Its permutation cycles are the components of the oriented link represented by G.

theorem TauCeti.GridDiagram.componentPerm_def {n : ℕ} (G : GridDiagram n) : G.componentPerm = G.X.toPerm⁻¹ * G.O.toPerm

The component permutation is the O-marking permutation followed by the inverse of the X-marking permutation. Downstream modules use this defining formula to read off the component permutation of a diagram whose two marking permutations are known.

@[simp]

theorem TauCeti.GridDiagram.componentPerm_apply {n : ℕ} (G : GridDiagram n) (c : Fin n) : G.componentPerm c = G.X.transpose.toPerm (G.O.toPerm c)

Applying the component permutation follows the O-marking's row to its unique X-marking column.

theorem TauCeti.GridDiagram.componentPerm_apply_eq_iff {n : ℕ} (G : GridDiagram n) {c d : Fin n} : G.componentPerm c = d ↔ G.X.toPerm d = G.O.toPerm c

The component permutation sends c to d exactly when the X-marking of column d lies in the row of the O-marking of column c.

theorem TauCeti.GridDiagram.X_componentPerm_apply {n : ℕ} (G : GridDiagram n) (c : Fin n) : G.X.toPerm (G.componentPerm c) = G.O.toPerm c

The X-marking of column componentPerm c lies in the row of the O-marking of column c.

theorem TauCeti.GridDiagram.O_transpose_X_componentPerm {n : ℕ} (G : GridDiagram n) (c : Fin n) : G.O.transpose.toPerm (G.X.toPerm (G.componentPerm c)) = c

The O-marking in the row of the X-marking of column componentPerm c is the O-marking of column c: the component permutation walks from O_c along its row to that X-marking.

theorem TauCeti.GridDiagram.componentPerm_apply_ne_self {n : ℕ} (G : GridDiagram n) (c : Fin n) : G.componentPerm c ≠ c

The component permutation has no fixed columns, because an O and an X cannot occupy the same square.

@[simp]

theorem TauCeti.GridDiagram.support_componentPerm {n : ℕ} (G : GridDiagram n) : G.componentPerm.support = Finset.univ

Every column belongs to the support of the component permutation.

def TauCeti.GridDiagram.componentCycles {n : ℕ} (G : GridDiagram n) : Finset (Equiv.Perm (Fin n))

The cycle factors of the component permutation. Each factor is one component of the represented link, expressed as a cyclic permutation of its O-marking columns.

@[simp]

theorem TauCeti.GridDiagram.mem_componentCycles_iff {n : ℕ} (G : GridDiagram n) (c : Equiv.Perm (Fin n)) : c ∈ G.componentCycles ↔ c.IsCycle ∧ ∀ a ∈ c.support, c a = G.componentPerm a

A permutation is a component cycle exactly when it is a cycle agreeing with the component permutation throughout its support.

def TauCeti.GridDiagram.componentCycleType {n : ℕ} (G : GridDiagram n) : Multiset ℕ

The multiset of component sizes of the link represented by a grid diagram.

theorem TauCeti.GridDiagram.componentCycleType_def {n : ℕ} (G : GridDiagram n) : G.componentCycleType = G.componentPerm.cycleType

The component-size multiset is the cycle type of the component permutation.

def TauCeti.GridDiagram.componentCount {n : ℕ} (G : GridDiagram n) : ℕ

The number of components of the link represented by a grid diagram.

theorem TauCeti.GridDiagram.componentCount_def {n : ℕ} (G : GridDiagram n) : G.componentCount = G.componentCycleType.card

The component count is the cardinality of the component-size multiset.

@[simp]

theorem TauCeti.GridDiagram.card_componentCycles {n : ℕ} (G : GridDiagram n) : G.componentCycles.card = G.componentCount

The number of component cycles agrees with componentCount.

@[simp]

theorem TauCeti.GridDiagram.sum_componentCycleType {n : ℕ} (G : GridDiagram n) : G.componentCycleType.sum = n

The component sizes sum to the grid size: every marking belongs to exactly one component.

theorem TauCeti.GridDiagram.componentCount_eq_orbitCount {n : ℕ} (G : GridDiagram n) : G.componentCount = orbitCount G.componentPerm

The number of components is the number of orbits of the component permutation. Every orbit is a genuine cycle here, since the component permutation has no fixed column.

def TauCeti.GridDiagram.IsKnot {n : ℕ} (G : GridDiagram n) : Prop

A grid diagram represents a knot when its component permutation has exactly one cycle.

theorem TauCeti.GridDiagram.isKnot_def {n : ℕ} (G : GridDiagram n) : G.IsKnot ↔ G.componentCount = 1

A grid diagram is a knot diagram exactly when its component count is one.

theorem TauCeti.GridDiagram.isKnot_iff_componentPerm_isCycle {n : ℕ} (G : GridDiagram n) : G.IsKnot ↔ G.componentPerm.IsCycle

A grid diagram represents a knot exactly when its component permutation is a single nontrivial cycle.

theorem TauCeti.GridDiagram.IsKnot.componentCycleType_eq {n : ℕ} (G : GridDiagram n) (hG : G.IsKnot) : G.componentCycleType = {n}

The sole component of a knot grid contains all n markings.

@[simp]

theorem TauCeti.GridDiagram.componentCount_eq_zero_iff {n : ℕ} (G : GridDiagram n) : G.componentCount = 0 ↔ n = 0

A grid diagram has no link components exactly when its size is zero.

@[simp]

theorem TauCeti.GridDiagram.componentCount_eq_zero_of_zero (G : GridDiagram 0) : G.componentCount = 0

The empty grid has no link components.

@[simp]

theorem TauCeti.GridDiagram.not_isKnot_of_zero (G : GridDiagram 0) : ¬G.IsKnot

An empty grid does not represent a knot.

theorem TauCeti.GridDiagram.IsKnot.ne_zero {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) : n ≠ 0

A knot grid has at least one column.

theorem TauCeti.GridDiagram.IsKnot.exists_pow_componentPerm_apply_eq {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (c₀ c : Fin n) : ∃ (k : ℕ), (G.componentPerm ^ k) c₀ = c

On a knot grid the component permutation, a single cycle through all columns, leads from any column to any other.

def TauCeti.GridDiagram.IsKnot.traversalIndex {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (c₀ c : Fin n) : ℕ

The traversal index of a column c from a base column c₀ of a knot grid: the least number of steps of the component permutation leading from c₀ to c.

@[simp]

theorem TauCeti.GridDiagram.IsKnot.pow_traversalIndex_apply {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (c₀ c : Fin n) : (G.componentPerm ^ hG.traversalIndex c₀ c) c₀ = c

The component permutation leads from the base column to c in traversalIndex c₀ c steps.

theorem TauCeti.GridDiagram.IsKnot.traversalIndex_le {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (c₀ : Fin n) {c : Fin n} {k : ℕ} (hk : (G.componentPerm ^ k) c₀ = c) : hG.traversalIndex c₀ c ≤ k

The traversal index is at most any number of steps leading from the base column to c.

@[simp]

theorem TauCeti.GridDiagram.IsKnot.traversalIndex_self {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (c₀ : Fin n) : hG.traversalIndex c₀ c₀ = 0

The base column has traversal index 0.

theorem TauCeti.GridDiagram.IsKnot.traversalIndex_lt {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (c₀ c : Fin n) : hG.traversalIndex c₀ c < n

The traversal index is less than the grid number.

theorem TauCeti.GridDiagram.IsKnot.traversalIndex_injective {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (c₀ : Fin n) : Function.Injective (hG.traversalIndex c₀)

Distinct columns have distinct traversal indices.

@[simp]

theorem TauCeti.GridDiagram.isKnot_of_two (G : GridDiagram 2) : G.IsKnot

Every 2 × 2 grid diagram represents a knot. Its fixed-point-free component permutation is the transposition of the two columns.

Traversing a knot

theorem TauCeti.GridDiagram.IsKnot.isCycleOn_componentPerm {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) : G.componentPerm.IsCycleOn Set.univ

The component permutation of a knot grid is a single cycle through all columns.

noncomputable def TauCeti.GridDiagram.IsKnot.traversal {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (c₀ : Fin n) : Fin n ≃ Fin n

The traversal of a knot grid from the column c₀: step t reaches the column componentPerm ^ t c₀, after t horizontal and t vertical segments. The component permutation of a knot is a single cycle through all n columns, so the first n steps reach every column exactly once.

@[simp]

theorem TauCeti.GridDiagram.IsKnot.traversal_apply {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (c₀ t : Fin n) : (hG.traversal c₀) t = (G.componentPerm ^ ↑t) c₀

@[simp]

theorem TauCeti.GridDiagram.IsKnot.val_traversal_symm_self {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (c₀ : Fin n) : ↑((hG.traversal c₀).symm c₀) = 0

The traversal from c₀ starts at c₀.

theorem TauCeti.GridDiagram.IsKnot.val_traversal_symm_componentPerm {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) {c₀ c : Fin n} (hc : G.componentPerm c ≠ c₀) : ↑((hG.traversal c₀).symm (G.componentPerm c)) = ↑((hG.traversal c₀).symm c) + 1

Each step of the traversal follows the component permutation: the column after c is reached one step after c, unless it is the starting column c₀, which the traversal returns to after n steps.

Naturality under grid symmetries

@[simp]

theorem TauCeti.GridDiagram.componentPerm_relabelRows {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) : (relabelRows ρ G).componentPerm = G.componentPerm

Relabeling rows does not change the component permutation: the common row relabeling cancels between the O- and X-marking permutations.

theorem TauCeti.GridDiagram.componentPerm_relabelColumns {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) : (relabelColumns κ G).componentPerm = κ * G.componentPerm * κ⁻¹

Relabeling columns conjugates the component permutation by the column relabeling.

@[simp]

theorem TauCeti.GridDiagram.componentCycles_relabelRows {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) : (relabelRows ρ G).componentCycles = G.componentCycles

Row relabeling preserves the component cycles.

theorem TauCeti.GridDiagram.mem_componentCycles_relabelColumns {n : ℕ} (G : GridDiagram n) (κ c : Equiv.Perm (Fin n)) : κ * c * κ⁻¹ ∈ (relabelColumns κ G).componentCycles ↔ c ∈ G.componentCycles

Column relabeling transports component cycles by conjugation.

@[simp]

theorem TauCeti.GridDiagram.componentCycleType_relabelRows {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) : (relabelRows ρ G).componentCycleType = G.componentCycleType

Row relabeling preserves the component-size multiset.

@[simp]

theorem TauCeti.GridDiagram.componentCycleType_relabelColumns {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) : (relabelColumns κ G).componentCycleType = G.componentCycleType

Column relabeling preserves the component-size multiset.

@[simp]

theorem TauCeti.GridDiagram.componentPerm_swapMarkings {n : ℕ} (G : GridDiagram n) : G.swapMarkings.componentPerm = G.componentPerm⁻¹

Exchanging the O- and X-markings inverts the component permutation.

theorem TauCeti.GridDiagram.mem_componentCycles_swapMarkings {n : ℕ} (G : GridDiagram n) (c : Equiv.Perm (Fin n)) : c⁻¹ ∈ G.swapMarkings.componentCycles ↔ c ∈ G.componentCycles

Exchanging the marking types reverses every component cycle.

@[simp]

theorem TauCeti.GridDiagram.componentCycleType_swapMarkings {n : ℕ} (G : GridDiagram n) : G.swapMarkings.componentCycleType = G.componentCycleType

Exchanging the two marking types preserves the component-size multiset.

theorem TauCeti.GridDiagram.componentPerm_transpose {n : ℕ} (G : GridDiagram n) : G.transpose.componentPerm = G.X.toPerm * G.componentPerm⁻¹ * G.X.toPerm⁻¹

Diagonal reflection conjugates the inverse component permutation by the X-marking permutation.

theorem TauCeti.GridDiagram.mem_componentCycles_transpose {n : ℕ} (G : GridDiagram n) (c : Equiv.Perm (Fin n)) : G.X.toPerm * c⁻¹ * G.X.toPerm⁻¹ ∈ G.transpose.componentCycles ↔ c ∈ G.componentCycles

Diagonal reflection transports component cycles by inversion and conjugation.

@[simp]

theorem TauCeti.GridDiagram.componentCycleType_transpose {n : ℕ} (G : GridDiagram n) : G.transpose.componentCycleType = G.componentCycleType

Diagonal reflection preserves the component-size multiset.

theorem TauCeti.GridDiagram.mem_componentCycles_rotate {n : ℕ} (G : GridDiagram n) (c : Equiv.Perm (Fin n)) : Fin.revPerm * c * Fin.revPerm⁻¹ ∈ G.rotate.componentCycles ↔ c ∈ G.componentCycles

Half-turn rotation transports component cycles by coordinate-reversal conjugation.

@[simp]

theorem TauCeti.GridDiagram.componentCycleType_rotate {n : ℕ} (G : GridDiagram n) : G.rotate.componentCycleType = G.componentCycleType

Half-turn rotation preserves the component-size multiset.

@[simp]

theorem TauCeti.GridDiagram.componentCount_relabelRows {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) : (relabelRows ρ G).componentCount = G.componentCount

Row relabeling preserves the number of represented link components.

@[simp]

theorem TauCeti.GridDiagram.componentCount_relabelColumns {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) : (relabelColumns κ G).componentCount = G.componentCount

Column relabeling preserves the number of represented link components.

@[simp]

theorem TauCeti.GridDiagram.componentCount_transpose {n : ℕ} (G : GridDiagram n) : G.transpose.componentCount = G.componentCount

Diagonal reflection preserves the number of represented link components.

@[simp]

theorem TauCeti.GridDiagram.componentCount_rotate {n : ℕ} (G : GridDiagram n) : G.rotate.componentCount = G.componentCount

Half-turn rotation preserves the number of represented link components.

@[simp]

theorem TauCeti.GridDiagram.componentCount_swapMarkings {n : ℕ} (G : GridDiagram n) : G.swapMarkings.componentCount = G.componentCount

Exchanging the two marking types preserves the number of represented link components.

@[simp]

theorem TauCeti.GridDiagram.isKnot_relabelRows {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) : (relabelRows ρ G).IsKnot ↔ G.IsKnot

Row relabeling preserves whether a grid diagram represents a knot.

@[simp]

theorem TauCeti.GridDiagram.isKnot_relabelColumns {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) : (relabelColumns κ G).IsKnot ↔ G.IsKnot

Column relabeling preserves whether a grid diagram represents a knot.

@[simp]

theorem TauCeti.GridDiagram.isKnot_swapColumns {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapColumns a b G).IsKnot ↔ G.IsKnot

Exchanging two columns preserves whether a grid diagram represents a knot.

theorem TauCeti.GridDiagram.IsKnot.swapColumns {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (a b : Fin n) : (GridDiagram.swapColumns a b G).IsKnot

Exchanging two columns of a knot grid gives a knot grid.

@[simp]

theorem TauCeti.GridDiagram.isKnot_transpose {n : ℕ} (G : GridDiagram n) : G.transpose.IsKnot ↔ G.IsKnot

Diagonal reflection preserves whether a grid diagram represents a knot.

@[simp]

theorem TauCeti.GridDiagram.isKnot_rotate {n : ℕ} (G : GridDiagram n) : G.rotate.IsKnot ↔ G.IsKnot

Half-turn rotation preserves whether a grid diagram represents a knot.

@[simp]

theorem TauCeti.GridDiagram.isKnot_swapMarkings {n : ℕ} (G : GridDiagram n) : G.swapMarkings.IsKnot ↔ G.IsKnot

Exchanging the two marking types preserves whether a grid diagram represents a knot.