Grid diagrams and grid states

A grid state of grid number n is a wrapper around a permutation of Fin n, sending each column to the unique row occupied by the state in that column. A grid diagram is encoded by two such permutation graphs, one for the O markings and one for the X markings, with the condition that no square contains both markings.

A state coordinate (c, r) is the grid point where column line c meets row line r. A marking coordinate (c, r) instead names the square whose lower-left corner is that grid point, bounded by column lines c, c + 1 and row lines r, r + 1, with indices read cyclically.

The point-set API records the basic row, column, cardinality, and disjointness facts about the occupied grid points of a grid state.

• TauCeti.GridState: a grid state with a permutation graph on Fin n.
• TauCeti.GridState.subdiagonal: the grid state whose occupied row is one below its column.
• TauCeti.GridState.pointSet: the finite set of occupied grid points of a grid state.
• TauCeti.GridDiagram: an n × n grid diagram with O and X markings.
• TauCeti.GridDiagram.OSet, TauCeti.GridDiagram.XSet: the marking-square sets.
• Relabeling, swapping, transposition, and marking-swap operations for grid states and diagrams.
• TauCeti.GridDiagram.cast: transport of a grid diagram along an equality of grid numbers.

References

• Ozsváth–Stipsicz–Szabó, Grid Homology for Knots and Links: grid diagrams (one O and one X marking in each row and column) in Chapter 3, and grid states (one point in each row and column) in Chapter 4.

structure TauCeti.GridState (n : ℕ) : Type

A grid state on an n × n toroidal grid.

The field toPerm sends each column to its occupied row. The named wrapper gives grid states their own preferred point-set API below, while still allowing direct access to the underlying permutation when needed.

• toPerm : Equiv.Perm (Fin n)

  The permutation sending each column to the occupied row in that column.

def TauCeti.GridState.equivPerm (n : ℕ) : GridState n ≃ Equiv.Perm (Fin n)

Grid states on an n × n grid are equivalent to permutations of Fin n, via the column-to-row permutation.

@[simp]

theorem TauCeti.GridState.equivPerm_symm_apply_toPerm (n : ℕ) (σ : Equiv.Perm (Fin n)) : ((equivPerm n).symm σ).toPerm = σ

@[simp]

theorem TauCeti.GridState.equivPerm_apply (n : ℕ) (x : GridState n) : (equivPerm n) x = x.toPerm

@[instance_reducible]

instance TauCeti.GridState.instFintype {n : ℕ} : Fintype (GridState n)

There are finitely many grid states of a fixed grid size.

@[instance_reducible]

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

Equality of grid states is decidable: a grid state is determined by its underlying permutation, whose equality is decidable. This makes finite sets of grid states computable.

@[instance_reducible]

instance TauCeti.GridState.instCoeFunForallFin {n : ℕ} : CoeFun (GridState n) fun (x : GridState n) => Fin n → Fin n

Apply a grid state to a column to get its occupied row.

theorem TauCeti.GridState.ext {n : ℕ} {x y : GridState n} (h : ∀ (c : Fin n), x.toPerm c = y.toPerm c) : x = y

Grid states are extensional in their column-to-row functions.

theorem TauCeti.GridState.ext_iff {n : ℕ} {x y : GridState n} : x = y ↔ ∀ (c : Fin n), x.toPerm c = y.toPerm c

def TauCeti.GridState.subdiagonal (n : ℕ) : GridState n

The subdiagonal grid state of an n-column grid: its point in column c lies one row below the diagonal point (c, c).

theorem TauCeti.GridState.subdiagonal_toPerm (n : ℕ) : (subdiagonal n).toPerm = (finRotate n)⁻¹

The permutation underlying the subdiagonal state is the inverse cyclic shift.

theorem TauCeti.GridState.subdiagonal_apply {n : ℕ} (c : Fin n) : (subdiagonal n).toPerm c = (finRotate n)⁻¹ c

The subdiagonal state reads off the inverse cyclic shift.

theorem TauCeti.GridState.subdiagonal_apply_add_one {n : ℕ} [NeZero n] (c : Fin n) : (subdiagonal n).toPerm c + 1 = c

Moving the subdiagonal point of a column up one row reaches the diagonal.

@[simp]

theorem TauCeti.GridState.subdiagonal_apply_eq_sub_one {n : ℕ} [NeZero n] (c : Fin n) : (subdiagonal n).toPerm c = c - 1

The subdiagonal state sends each column to the preceding row.

def TauCeti.GridState.pointSet {n : ℕ} (x : GridState n) : Finset (Fin n × Fin n)

The finite set of occupied grid points of a grid state. The first coordinate is the column and the second coordinate is the row.

theorem TauCeti.GridState.equivPerm_symm_pointSet {n : ℕ} (σ : Equiv.Perm (Fin n)) : ((equivPerm n).symm σ).pointSet = Finset.image (fun (c : Fin n) => (c, σ c)) Finset.univ

The point set of the grid state obtained from σ is the graph {(c, σ c)}.

@[simp]

theorem TauCeti.GridState.mem_pointSet {n : ℕ} (x : GridState n) (p : Fin n × Fin n) : p ∈ x.pointSet ↔ x.toPerm p.1 = p.2

Membership in the point set of a grid state is the graph condition for its permutation.

theorem TauCeti.GridState.mk_mem_pointSet {n : ℕ} (x : GridState n) (c r : Fin n) : (c, r) ∈ x.pointSet ↔ x.toPerm c = r

The grid point (c, r) lies in a grid state's point set exactly when x c = r.

@[simp]

theorem TauCeti.GridState.card_pointSet {n : ℕ} (x : GridState n) : x.pointSet.card = n

The point set of a grid state has exactly n occupied grid points.

theorem TauCeti.GridState.sum_pointSet {n : ℕ} {M : Type u_1} [AddCommMonoid M] (x : GridState n) (f : Fin n × Fin n → M) : ∑ p ∈ x.pointSet, f p = ∑ c : Fin n, f (c, x.toPerm c)

A sum over the occupied grid points of a grid state is a sum over the columns.

theorem TauCeti.GridState.sum_ite_mem_columns {n : ℕ} {R : Type u_1} [AddCommMonoidWithOne R] (x : GridState n) (C : Finset (Fin n)) : (∑ p ∈ x.pointSet, if p.1 ∈ C then 1 else 0) = ↑C.card

A grid state meets a set of columns in as many occupied grid points as there are columns.

theorem TauCeti.GridState.sum_ite_mem_rows {n : ℕ} {R : Type u_1} [AddCommMonoidWithOne R] (x : GridState n) (D : Finset (Fin n)) : (∑ p ∈ x.pointSet, if p.2 ∈ D then 1 else 0) = ↑D.card

A grid state meets a set of rows in as many occupied grid points as there are rows.

theorem TauCeti.GridState.disjoint_product_pointSet_iff {n : ℕ} (M : GridState n) (s t : Finset (Fin n)) : Disjoint (s ×ˢ t) M.pointSet ↔ ∀ c ∈ s, M.toPerm c ∉ t

A product of column and row sets avoids a grid state's points exactly when every column in the first set has its occupied row outside the second set.

theorem TauCeti.GridState.not_disjoint_product_univ_pointSet {n : ℕ} (M : GridState n) {s : Finset (Fin n)} (hs : s.Nonempty) : ¬Disjoint (s ×ˢ Finset.univ) M.pointSet

A grid state occupies a grid point in every column, so its point set meets s ×ˢ univ for every nonempty set s of columns.

theorem TauCeti.GridState.not_disjoint_univ_product_pointSet {n : ℕ} (M : GridState n) {t : Finset (Fin n)} (ht : t.Nonempty) : ¬Disjoint (Finset.univ ×ˢ t) M.pointSet

A grid state occupies a grid point in every row, so its point set meets univ ×ˢ t for every nonempty set t of rows.

theorem TauCeti.GridState.disjoint_univ_erase_product_singleton_pointSet_iff {n : ℕ} (M : GridState n) (c r : Fin n) : Disjoint (Finset.univ.erase c ×ˢ {r}) M.pointSet ↔ M.toPerm c = r

A row with one column removed avoids a grid state's points exactly when the point in that row lies in the removed column.

@[simp]

theorem TauCeti.GridState.pointSet_inj {n : ℕ} {x y : GridState n} : x.pointSet = y.pointSet ↔ x = y

Point sets of grid states are equal exactly when the underlying permutations are equal.

theorem TauCeti.GridState.disjoint_pointSet_iff {n : ℕ} (x y : GridState n) : Disjoint x.pointSet y.pointSet ↔ ∀ (c : Fin n), x.toPerm c ≠ y.toPerm c

Two grid states have disjoint point sets exactly when they disagree in every column.

def TauCeti.GridState.relabelRows {n : ℕ} (ρ : Equiv.Perm (Fin n)) (x : GridState n) : GridState n

Relabel the rows of a grid state by a permutation of Fin n.

If ρ is the row permutation, the point in column c moves from row x c to row ρ (x c).

def TauCeti.GridState.relabelColumns {n : ℕ} (κ : Equiv.Perm (Fin n)) (x : GridState n) : GridState n

Relabel the columns of a grid state by a permutation of Fin n.

The point in the old column c appears in the new column κ c, so the row in a new column c is read from the old column κ.symm c.

@[simp]

theorem TauCeti.GridState.relabelRows_apply {n : ℕ} (ρ : Equiv.Perm (Fin n)) (x : GridState n) (c : Fin n) : (relabelRows ρ x).toPerm c = ρ (x.toPerm c)

Row relabeling evaluates by applying the row permutation to the old row.

@[simp]

theorem TauCeti.GridState.relabelColumns_apply {n : ℕ} (κ : Equiv.Perm (Fin n)) (x : GridState n) (c : Fin n) : (relabelColumns κ x).toPerm c = x.toPerm ((Equiv.symm κ) c)

Column relabeling evaluates by reading the old state at the inverse column.

@[simp]

theorem TauCeti.GridState.relabelRows_refl {n : ℕ} (x : GridState n) : relabelRows (Equiv.refl (Fin n)) x = x

Relabeling rows by the identity permutation does not change a grid state.

@[simp]

theorem TauCeti.GridState.relabelColumns_refl {n : ℕ} (x : GridState n) : relabelColumns (Equiv.refl (Fin n)) x = x

Relabeling columns by the identity permutation does not change a grid state.

@[simp]

theorem TauCeti.GridState.relabelRows_relabelRows {n : ℕ} (ρ σ : Equiv.Perm (Fin n)) (x : GridState n) : relabelRows σ (relabelRows ρ x) = relabelRows (Equiv.trans ρ σ) x

Successive row relabelings compose.

@[simp]

theorem TauCeti.GridState.relabelColumns_relabelColumns {n : ℕ} (κ τ : Equiv.Perm (Fin n)) (x : GridState n) : relabelColumns τ (relabelColumns κ x) = relabelColumns (Equiv.trans κ τ) x

Successive column relabelings compose.

theorem TauCeti.GridState.relabelRows_relabelColumns {n : ℕ} (ρ κ : Equiv.Perm (Fin n)) (x : GridState n) : relabelColumns κ (relabelRows ρ x) = relabelRows ρ (relabelColumns κ x)

Row and column relabeling commute on grid states.

theorem TauCeti.GridState.mem_pointSet_relabelRows {n : ℕ} (ρ : Equiv.Perm (Fin n)) (x : GridState n) (p : Fin n × Fin n) : p ∈ (relabelRows ρ x).pointSet ↔ (p.1, (Equiv.symm ρ) p.2) ∈ x.pointSet

Membership in the point set after a row relabeling.

theorem TauCeti.GridState.mem_pointSet_relabelColumns {n : ℕ} (κ : Equiv.Perm (Fin n)) (x : GridState n) (p : Fin n × Fin n) : p ∈ (relabelColumns κ x).pointSet ↔ ((Equiv.symm κ) p.1, p.2) ∈ x.pointSet

Membership in the point set after a column relabeling.

theorem TauCeti.GridState.pointSet_eq_map_relabelRows {n : ℕ} (x : GridState n) (ρ : Equiv.Perm (Fin n)) : x.pointSet = Finset.map ((Equiv.refl (Fin n)).prodCongr (Equiv.symm ρ)).toEmbedding (relabelRows ρ x).pointSet

Undoing a row relabeling transports the relabeled state's points to the original point set.

theorem TauCeti.GridState.pointSet_eq_map_relabelColumns {n : ℕ} (x : GridState n) (κ : Equiv.Perm (Fin n)) : x.pointSet = Finset.map ((Equiv.symm κ).prodCongr (Equiv.refl (Fin n))).toEmbedding (relabelColumns κ x).pointSet

Undoing a column relabeling transports the relabeled state's points to the original point set.

theorem TauCeti.GridState.disjoint_map_relabelRows_pointSet_iff {n : ℕ} (x : GridState n) (ρ : Equiv.Perm (Fin n)) (S : Finset (Fin n × Fin n)) : Disjoint (Finset.map ((Equiv.refl (Fin n)).prodCongr (Equiv.symm ρ)).toEmbedding S) x.pointSet ↔ Disjoint S (relabelRows ρ x).pointSet

A set of squares relabeled back avoids a state's points exactly when the set avoids the row-relabeled state's points.

theorem TauCeti.GridState.disjoint_map_relabelColumns_pointSet_iff {n : ℕ} (x : GridState n) (κ : Equiv.Perm (Fin n)) (S : Finset (Fin n × Fin n)) : Disjoint (Finset.map ((Equiv.symm κ).prodCongr (Equiv.refl (Fin n))).toEmbedding S) x.pointSet ↔ Disjoint S (relabelColumns κ x).pointSet

A set of squares relabeled back avoids a state's points exactly when the set avoids the column-relabeled state's points.

def TauCeti.GridState.swapRows {n : ℕ} (a b : Fin n) (x : GridState n) : GridState n

Swapping two rows in a grid state.

def TauCeti.GridState.swapColumns {n : ℕ} (a b : Fin n) (x : GridState n) : GridState n

Swapping two columns in a grid state.

@[simp]

theorem TauCeti.GridState.swapRows_apply {n : ℕ} (a b : Fin n) (x : GridState n) (c : Fin n) : (swapRows a b x).toPerm c = (Equiv.swap a b) (x.toPerm c)

Row swaps evaluate by swapping the row selected by the old state.

@[simp]

theorem TauCeti.GridState.swapColumns_apply {n : ℕ} (a b : Fin n) (x : GridState n) (c : Fin n) : (swapColumns a b x).toPerm c = x.toPerm ((Equiv.swap a b) c)

Column swaps evaluate by reading the old state at the swapped column.

theorem TauCeti.GridState.eq_swap_of_swapColumns_apply_eq {n : ℕ} {x : GridState n} {a b c d : Fin n} (h : (swapColumns a b x).toPerm c = x.toPerm d) : c = (Equiv.swap a b) d

A column read off the row it occupies after a column swap.

theorem TauCeti.GridState.swapColumns_comm {n : ℕ} (a b : Fin n) (x : GridState n) : swapColumns a b x = swapColumns b a x

Swapping columns is symmetric in the two chosen columns.

theorem TauCeti.GridState.swapColumns_eq_swapRows {n : ℕ} (a b : Fin n) (x : GridState n) : swapColumns a b x = swapRows (x.toPerm a) (x.toPerm b) x

Swapping two columns of a grid state is the same as swapping the two rows they occupy: the state is a bijection between columns and rows, so either operation exchanges the rows of the points in columns a and b and leaves every other point in place.

@[simp]

theorem TauCeti.GridState.swapColumns_swapColumns {n : ℕ} (a b : Fin n) (x : GridState n) : swapColumns a b (swapColumns a b x) = x

Swapping the same pair of columns twice is the identity on grid states.

theorem TauCeti.GridState.swapColumns_swapColumns_conj {n : ℕ} (x : GridState n) (a b c d : Fin n) : swapColumns c d (swapColumns a b x) = swapColumns ((Equiv.swap c d) a) ((Equiv.swap c d) b) (swapColumns c d x)

Conjugating the first transposition by the second reorders two column swaps.

When the pairs are disjoint this is commutation. When a ≠ b, c ≠ d, and the pairs share exactly one column, the conjugated pair is the third pair among the three involved columns.

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

The grid states obtained from x by transposing a pair of distinct columns.

These are exactly the states a single grid rectangle can reach from x: the fully blocked differential of the generator x is supported here.

@[simp]

theorem TauCeti.GridState.mem_columnSwapNeighbors {n : ℕ} {x y : GridState n} : y ∈ x.columnSwapNeighbors ↔ ∃ (c : Fin n) (d : Fin n), c ≠ d ∧ y = swapColumns c d x

A state is a column-swap neighbour of x exactly when it is x with a pair of distinct columns transposed.

theorem TauCeti.GridState.mem_columnSwapNeighbors_comm {n : ℕ} {x y : GridState n} : y ∈ x.columnSwapNeighbors ↔ x ∈ y.columnSwapNeighbors

If y is a column-swap neighbour of x, then x is a column-swap neighbour of y.

This is the elementary reversibility of a rectangle target: the same pair of side columns swaps back to the source state.

theorem TauCeti.GridState.columnSwapNeighbors_eq_offDiag_image {n : ℕ} (x : GridState n) : x.columnSwapNeighbors = Finset.image (fun (p : Fin n × Fin n) => swapColumns p.1 p.2 x) Finset.univ.offDiag

The finite set of column-swap neighbours is the image of the off-diagonal of the column set: an ordered pair of distinct columns gives the state obtained by swapping those columns.

theorem TauCeti.GridState.sym2_mk_eq_of_swapColumns_eq {n : ℕ} {x : GridState n} {a b c d : Fin n} (hab : a ≠ b) (h : swapColumns a b x = swapColumns c d x) : s(a, b) = s(c, d)

If a nontrivial column swap of a grid state agrees with another column swap of it, then the two swap the same unordered pair of columns.

@[simp]

theorem TauCeti.GridState.card_columnSwapNeighbors {n : ℕ} (x : GridState n) : x.columnSwapNeighbors.card = n.choose 2

A grid state has exactly n.choose 2 column-swap neighbours.

theorem TauCeti.GridState.self_notMem_columnSwapNeighbors {n : ℕ} (x : GridState n) : x ∉ x.columnSwapNeighbors

A grid state is not a column-swap neighbour of itself: swapping two distinct columns moves the occupied row of either column, so the result differs from the original.

theorem TauCeti.GridState.mem_pointSet_swapRows {n : ℕ} (a b : Fin n) (x : GridState n) (p : Fin n × Fin n) : p ∈ (swapRows a b x).pointSet ↔ (p.1, (Equiv.swap a b) p.2) ∈ x.pointSet

Row swaps transport the point set by the row transposition.

theorem TauCeti.GridState.mem_pointSet_swapColumns {n : ℕ} (a b : Fin n) (x : GridState n) (p : Fin n × Fin n) : p ∈ (swapColumns a b x).pointSet ↔ ((Equiv.swap a b) p.1, p.2) ∈ x.pointSet

Column swaps transport the point set by the column transposition.

theorem TauCeti.GridState.mem_pointSet_inter_relabelColumns_iff {n : ℕ} (x : GridState n) (κ : Equiv.Perm (Fin n)) (p : Fin n × Fin n) : p ∈ x.pointSet ∩ (relabelColumns κ x).pointSet ↔ p ∈ x.pointSet ∧ κ p.1 = p.1

A grid point is shared by a grid state and a column relabeling exactly when it is a source-state grid point whose column is fixed by the relabeling permutation.

@[simp]

theorem TauCeti.GridState.swapRows_swapRows {n : ℕ} (a b : Fin n) (x : GridState n) : swapRows a b (swapRows a b x) = x

Swapping the same pair of rows twice is the identity on grid states.

theorem TauCeti.GridState.mem_pointSet_inter_swapColumns_iff {n : ℕ} (x : GridState n) {a b : Fin n} (h : a ≠ b) (p : Fin n × Fin n) : p ∈ x.pointSet ∩ (swapColumns a b x).pointSet ↔ p ∈ x.pointSet ∧ p.1 ≠ a ∧ p.1 ≠ b

A grid point is shared by a grid state and the state with columns a and b swapped exactly when it is a source-state grid point away from the two swapped columns.

theorem TauCeti.GridState.pointSet_eq_insert_insert_inter_swapColumns {n : ℕ} (x : GridState n) (a b : Fin n) : x.pointSet = insert (a, x.toPerm a) (insert (b, x.toPerm b) (x.pointSet ∩ (swapColumns a b x).pointSet))

The point set of a grid state is the shared part with a column swap, together with the two source-state grid points in the swapped columns.

theorem TauCeti.GridState.swapColumns_pointSet_eq_insert_insert_inter {n : ℕ} (x : GridState n) (a b : Fin n) : (swapColumns a b x).pointSet = insert (a, x.toPerm b) (insert (b, x.toPerm a) (x.pointSet ∩ (swapColumns a b x).pointSet))

The point set after swapping columns a and b is the shared part with the source state, together with the two target-state grid points in the swapped columns.

theorem TauCeti.GridState.card_pointSet_inter_swapColumns {n : ℕ} (x : GridState n) {a b : Fin n} (h : a ≠ b) : (x.pointSet ∩ (swapColumns a b x).pointSet).card = n - 2

A grid state and a swap of two distinct columns share exactly n - 2 grid points.

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

The diagonal reflection of a grid state.

Reflecting the occupied grid points across the main diagonal exchanges columns and rows, so the new permutation graph is the inverse of the old one.

@[simp]

theorem TauCeti.GridState.transpose_apply {n : ℕ} (x : GridState n) (c : Fin n) : x.transpose.toPerm c = (Equiv.symm x.toPerm) c

The diagonal reflection evaluates by the inverse permutation graph.

theorem TauCeti.GridState.apply_transpose_apply {n : ℕ} (x : GridState n) (r : Fin n) : x.toPerm (x.transpose.toPerm r) = r

The point of x in row r lies in column x.transpose r.

theorem TauCeti.GridState.transpose_apply_apply {n : ℕ} (x : GridState n) (c : Fin n) : x.transpose.toPerm (x.toPerm c) = c

The point of x in column c lies in row x c, so x.transpose sends that row back to c.

@[simp]

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

The diagonal reflection is an involution on grid states.

theorem TauCeti.GridState.transpose_injective {n : ℕ} : Function.Injective transpose

The diagonal reflection is injective on grid states.

@[simp]

theorem TauCeti.GridState.transpose_inj {n : ℕ} {x y : GridState n} : x.transpose = y.transpose ↔ x = y

Two grid states have equal diagonal reflections exactly when they are equal.

@[simp]

theorem TauCeti.GridState.relabelRows_transpose {n : ℕ} (ρ : Equiv.Perm (Fin n)) (x : GridState n) : (relabelRows ρ x).transpose = relabelColumns ρ x.transpose

Reflecting after a row relabeling is the same as column relabeling after reflecting.

@[simp]

theorem TauCeti.GridState.relabelColumns_transpose {n : ℕ} (κ : Equiv.Perm (Fin n)) (x : GridState n) : (relabelColumns κ x).transpose = relabelRows κ x.transpose

Reflecting after a column relabeling is the same as row relabeling after reflecting.

@[simp]

theorem TauCeti.GridState.swapRows_transpose {n : ℕ} (a b : Fin n) (x : GridState n) : (swapRows a b x).transpose = swapColumns a b x.transpose

Reflecting after a row swap is the same as the corresponding column swap after reflecting.

@[simp]

theorem TauCeti.GridState.swapColumns_transpose {n : ℕ} (a b : Fin n) (x : GridState n) : (swapColumns a b x).transpose = swapRows a b x.transpose

Reflecting after a column swap is the same as the corresponding row swap after reflecting.

theorem TauCeti.GridState.mem_pointSet_transpose {n : ℕ} (x : GridState n) (p : Fin n × Fin n) : p ∈ x.transpose.pointSet ↔ p.swap ∈ x.pointSet

A grid point lies in the reflected state exactly when its diagonal reflection lies in the original state.

theorem TauCeti.GridState.transpose_pointSet {n : ℕ} (x : GridState n) : x.transpose.pointSet = Finset.image Prod.swap x.pointSet

The point set of the reflected state is the diagonal reflection of the original point set.

structure TauCeti.GridDiagram (n : ℕ) : Type

An n × n grid diagram, encoded by the O-marking and X-marking permutation graphs.

The permutation fields enforce one O and one X in each row and column. The disjoint field says no square contains both markings. With this encoding GridDiagram 0, the empty diagram, is inhabited, while GridDiagram 1 is empty: its only O and X permutations put both markings in the single square.

• O : GridState n

  The O marking in each column, encoded by its row.

• X : GridState n

  The X marking in each column, encoded by its row.

• disjoint (c : Fin n) : self.O.toPerm c ≠ self.X.toPerm c

  No square contains both an O marking and an X marking.

theorem TauCeti.GridDiagram.ext_iff {n : ℕ} {x y : GridDiagram n} : x = y ↔ x.O = y.O ∧ x.X = y.X

theorem TauCeti.GridDiagram.ext {n : ℕ} {x y : GridDiagram n} (O : x.O = y.O) (X : x.X = y.X) : x = y

instance TauCeti.instIsEmptyGridDiagramOfNatNat : IsEmpty (GridDiagram 1)

There is no grid diagram of size 1: the unique O and X markings would have to occupy the same square.

def TauCeti.GridDiagram.OSet {n : ℕ} (G : GridDiagram n) : Finset (Fin n × Fin n)

The finite set of O-marked squares of a grid diagram. A pair (c, r) names the square whose lower-left grid point is (c, r).

def TauCeti.GridDiagram.XSet {n : ℕ} (G : GridDiagram n) : Finset (Fin n × Fin n)

The finite set of X-marked squares of a grid diagram. A pair (c, r) names the square whose lower-left grid point is (c, r).

theorem TauCeti.GridDiagram.OSet_def {n : ℕ} (G : GridDiagram n) : G.OSet = G.O.pointSet

The O-marking set is the grid-point set of the O permutation.

theorem TauCeti.GridDiagram.XSet_def {n : ℕ} (G : GridDiagram n) : G.XSet = G.X.pointSet

The X-marking set is the grid-point set of the X permutation.

@[simp]

theorem TauCeti.GridDiagram.mem_OSet {n : ℕ} (G : GridDiagram n) (p : Fin n × Fin n) : p ∈ G.OSet ↔ G.O.toPerm p.1 = p.2

Membership in the O-marking set is the graph condition for the O permutation.

@[simp]

theorem TauCeti.GridDiagram.mem_XSet {n : ℕ} (G : GridDiagram n) (p : Fin n × Fin n) : p ∈ G.XSet ↔ G.X.toPerm p.1 = p.2

Membership in the X-marking set is the graph condition for the X permutation.

theorem TauCeti.GridDiagram.mk_mem_OSet {n : ℕ} (G : GridDiagram n) (c r : Fin n) : (c, r) ∈ G.OSet ↔ G.O.toPerm c = r

The square (c, r) contains an O marking exactly when G.O c = r.

theorem TauCeti.GridDiagram.mk_mem_XSet {n : ℕ} (G : GridDiagram n) (c r : Fin n) : (c, r) ∈ G.XSet ↔ G.X.toPerm c = r

The square (c, r) contains an X marking exactly when G.X c = r.

@[simp]

theorem TauCeti.GridDiagram.card_OSet {n : ℕ} (G : GridDiagram n) : G.OSet.card = n

A grid diagram has exactly n O markings.

@[simp]

theorem TauCeti.GridDiagram.card_XSet {n : ℕ} (G : GridDiagram n) : G.XSet.card = n

A grid diagram has exactly n X markings.

theorem TauCeti.GridDiagram.disjoint_OSet_XSet {n : ℕ} (G : GridDiagram n) : Disjoint G.OSet G.XSet

The O and X marking sets of a grid diagram are disjoint.

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

Relabel the rows of a grid diagram by relabeling both marking states.

@[simp]

theorem TauCeti.GridDiagram.relabelRows_X {n : ℕ} (ρ : Equiv.Perm (Fin n)) (G : GridDiagram n) : (relabelRows ρ G).X = GridState.relabelRows ρ G.X

@[simp]

theorem TauCeti.GridDiagram.relabelRows_O {n : ℕ} (ρ : Equiv.Perm (Fin n)) (G : GridDiagram n) : (relabelRows ρ G).O = GridState.relabelRows ρ G.O

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

Relabel the columns of a grid diagram by relabeling both marking states.

@[simp]

theorem TauCeti.GridDiagram.relabelColumns_X {n : ℕ} (κ : Equiv.Perm (Fin n)) (G : GridDiagram n) : (relabelColumns κ G).X = GridState.relabelColumns κ G.X

@[simp]

theorem TauCeti.GridDiagram.relabelColumns_O {n : ℕ} (κ : Equiv.Perm (Fin n)) (G : GridDiagram n) : (relabelColumns κ G).O = GridState.relabelColumns κ G.O

@[simp]

theorem TauCeti.GridDiagram.relabelRows_O_apply {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) (c : Fin n) : (relabelRows ρ G).O.toPerm c = ρ (G.O.toPerm c)

Row relabeling evaluates on the O marking by applying the row permutation.

@[simp]

theorem TauCeti.GridDiagram.relabelRows_X_apply {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) (c : Fin n) : (relabelRows ρ G).X.toPerm c = ρ (G.X.toPerm c)

Row relabeling evaluates on the X marking by applying the row permutation.

@[simp]

theorem TauCeti.GridDiagram.relabelColumns_O_apply {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) (c : Fin n) : (relabelColumns κ G).O.toPerm c = G.O.toPerm ((Equiv.symm κ) c)

Column relabeling evaluates on the O marking at the inverse old column.

@[simp]

theorem TauCeti.GridDiagram.relabelColumns_X_apply {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) (c : Fin n) : (relabelColumns κ G).X.toPerm c = G.X.toPerm ((Equiv.symm κ) c)

Column relabeling evaluates on the X marking at the inverse old column.

theorem TauCeti.GridDiagram.mem_OSet_relabelRows {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) (p : Fin n × Fin n) : p ∈ (relabelRows ρ G).OSet ↔ (p.1, (Equiv.symm ρ) p.2) ∈ G.OSet

Row relabeling transports the O marking set by the row permutation.

theorem TauCeti.GridDiagram.mem_XSet_relabelRows {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) (p : Fin n × Fin n) : p ∈ (relabelRows ρ G).XSet ↔ (p.1, (Equiv.symm ρ) p.2) ∈ G.XSet

Row relabeling transports the X marking set by the row permutation.

theorem TauCeti.GridDiagram.mem_OSet_relabelColumns {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) (p : Fin n × Fin n) : p ∈ (relabelColumns κ G).OSet ↔ ((Equiv.symm κ) p.1, p.2) ∈ G.OSet

Column relabeling transports the O marking set by the column permutation.

theorem TauCeti.GridDiagram.mem_XSet_relabelColumns {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) (p : Fin n × Fin n) : p ∈ (relabelColumns κ G).XSet ↔ ((Equiv.symm κ) p.1, p.2) ∈ G.XSet

Column relabeling transports the X marking set by the column permutation.

theorem TauCeti.GridDiagram.disjoint_map_relabelRows_XSet_iff {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) (S : Finset (Fin n × Fin n)) : Disjoint (Finset.map ((Equiv.refl (Fin n)).prodCongr (Equiv.symm ρ)).toEmbedding S) G.XSet ↔ Disjoint S (relabelRows ρ G).XSet

A set of squares with rows relabeled back avoids the original X-markings exactly when the set avoids the row-relabeled diagram's X-markings.

theorem TauCeti.GridDiagram.disjoint_map_relabelColumns_XSet_iff {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) (S : Finset (Fin n × Fin n)) : Disjoint (Finset.map ((Equiv.symm κ).prodCongr (Equiv.refl (Fin n))).toEmbedding S) G.XSet ↔ Disjoint S (relabelColumns κ G).XSet

A set of squares relabeled back avoids the original X-markings exactly when the set avoids the relabeled diagram's X-markings.

def TauCeti.GridDiagram.swapRows {n : ℕ} (a b : Fin n) (G : GridDiagram n) : GridDiagram n

Swapping two rows in a grid diagram.

def TauCeti.GridDiagram.swapColumns {n : ℕ} (a b : Fin n) (G : GridDiagram n) : GridDiagram n

Swapping two columns in a grid diagram.

@[simp]

theorem TauCeti.GridDiagram.swapRows_O {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapRows a b G).O = GridState.swapRows a b G.O

The O marking state of a row-swapped grid diagram.

@[simp]

theorem TauCeti.GridDiagram.swapRows_X {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapRows a b G).X = GridState.swapRows a b G.X

The X marking state of a row-swapped grid diagram.

@[simp]

theorem TauCeti.GridDiagram.swapColumns_O {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapColumns a b G).O = GridState.swapColumns a b G.O

The O marking state of a column-swapped grid diagram.

@[simp]

theorem TauCeti.GridDiagram.swapColumns_X {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapColumns a b G).X = GridState.swapColumns a b G.X

The X marking state of a column-swapped grid diagram.

theorem TauCeti.GridDiagram.swapRows_swapColumns_X_toPerm {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapColumns a b (swapRows a b G)).X.toPerm = Equiv.swap a b * G.X.toPerm * Equiv.swap a b

Exchanging two rows and the same two columns conjugates the X-permutation by the transposition.

theorem TauCeti.GridDiagram.swapRows_swapColumns_O_toPerm {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapColumns a b (swapRows a b G)).O.toPerm = Equiv.swap a b * G.O.toPerm * Equiv.swap a b

Exchanging two rows and the same two columns conjugates the O-permutation by the transposition.

theorem TauCeti.GridDiagram.mem_OSet_swapRows {n : ℕ} (G : GridDiagram n) (a b : Fin n) (p : Fin n × Fin n) : p ∈ (swapRows a b G).OSet ↔ (p.1, (Equiv.swap a b) p.2) ∈ G.OSet

Row swaps transport the O marking set by the row transposition.

theorem TauCeti.GridDiagram.mem_XSet_swapRows {n : ℕ} (G : GridDiagram n) (a b : Fin n) (p : Fin n × Fin n) : p ∈ (swapRows a b G).XSet ↔ (p.1, (Equiv.swap a b) p.2) ∈ G.XSet

Row swaps transport the X marking set by the row transposition.

theorem TauCeti.GridDiagram.mem_OSet_swapColumns {n : ℕ} (G : GridDiagram n) (a b : Fin n) (p : Fin n × Fin n) : p ∈ (swapColumns a b G).OSet ↔ ((Equiv.swap a b) p.1, p.2) ∈ G.OSet

Column swaps transport the O marking set by the column transposition.

theorem TauCeti.GridDiagram.mem_XSet_swapColumns {n : ℕ} (G : GridDiagram n) (a b : Fin n) (p : Fin n × Fin n) : p ∈ (swapColumns a b G).XSet ↔ ((Equiv.swap a b) p.1, p.2) ∈ G.XSet

Column swaps transport the X marking set by the column transposition.

theorem TauCeti.GridDiagram.disjoint_map_swapRows_XSet_iff {n : ℕ} (G : GridDiagram n) (a b : Fin n) (S : Finset (Fin n × Fin n)) : Disjoint (Finset.map ((Equiv.refl (Fin n)).prodCongr (Equiv.swap a b)).toEmbedding S) G.XSet ↔ Disjoint S (swapRows a b G).XSet

A set of squares with rows swapped back avoids the original X-markings exactly when the set avoids the row-swapped diagram's X-markings.

theorem TauCeti.GridDiagram.disjoint_map_swapColumns_XSet_iff {n : ℕ} (G : GridDiagram n) (a b : Fin n) (S : Finset (Fin n × Fin n)) : Disjoint (Finset.map (Equiv.prodCongr (Equiv.swap a b) (Equiv.refl (Fin n))).toEmbedding S) G.XSet ↔ Disjoint S (swapColumns a b G).XSet

A set of squares swapped back avoids the original X-markings exactly when the set avoids the swapped diagram's X-markings.

@[simp]

theorem TauCeti.GridDiagram.swapRows_swapRows {n : ℕ} (G : GridDiagram n) (a b : Fin n) : swapRows a b (swapRows a b G) = G

Swapping the same pair of rows twice is the identity on grid diagrams.

@[simp]

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

Swapping the same pair of columns twice is the identity on grid diagrams.

@[simp]

theorem TauCeti.GridDiagram.relabelRows_refl {n : ℕ} (G : GridDiagram n) : relabelRows (Equiv.refl (Fin n)) G = G

Relabeling rows by the identity permutation does not change a grid diagram.

@[simp]

theorem TauCeti.GridDiagram.relabelColumns_refl {n : ℕ} (G : GridDiagram n) : relabelColumns (Equiv.refl (Fin n)) G = G

Relabeling columns by the identity permutation does not change a grid diagram.

@[simp]

theorem TauCeti.GridDiagram.relabelRows_relabelRows {n : ℕ} (G : GridDiagram n) (ρ σ : Equiv.Perm (Fin n)) : relabelRows σ (relabelRows ρ G) = relabelRows (Equiv.trans ρ σ) G

Successive row relabelings compose on grid diagrams.

@[simp]

theorem TauCeti.GridDiagram.relabelColumns_relabelColumns {n : ℕ} (G : GridDiagram n) (κ τ : Equiv.Perm (Fin n)) : relabelColumns τ (relabelColumns κ G) = relabelColumns (Equiv.trans κ τ) G

Successive column relabelings compose on grid diagrams.

theorem TauCeti.GridDiagram.relabelRows_relabelColumns {n : ℕ} (G : GridDiagram n) (ρ κ : Equiv.Perm (Fin n)) : relabelColumns κ (relabelRows ρ G) = relabelRows ρ (relabelColumns κ G)

Row and column relabeling commute on grid diagrams.

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

The diagonal reflection of a grid diagram, reflecting both the O and X marking states.

Reflection across the main diagonal is a bijection of squares, so it preserves the condition that no square carries both markings.

@[simp]

theorem TauCeti.GridDiagram.transpose_X {n : ℕ} (G : GridDiagram n) : G.transpose.X = G.X.transpose

@[simp]

theorem TauCeti.GridDiagram.transpose_O {n : ℕ} (G : GridDiagram n) : G.transpose.O = G.O.transpose

@[simp]

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

The diagonal reflection is an involution on grid diagrams.

@[simp]

theorem TauCeti.GridDiagram.relabelRows_transpose {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) : (relabelRows ρ G).transpose = relabelColumns ρ G.transpose

Reflecting after a row relabeling is the same as column relabeling after reflecting.

@[simp]

theorem TauCeti.GridDiagram.relabelColumns_transpose {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) : (relabelColumns κ G).transpose = relabelRows κ G.transpose

Reflecting after a column relabeling is the same as row relabeling after reflecting.

@[simp]

theorem TauCeti.GridDiagram.swapRows_transpose {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapRows a b G).transpose = swapColumns a b G.transpose

Reflecting after a row swap is the same as the corresponding column swap after reflecting.

@[simp]

theorem TauCeti.GridDiagram.swapColumns_transpose {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapColumns a b G).transpose = swapRows a b G.transpose

Reflecting after a column swap is the same as the corresponding row swap after reflecting.

theorem TauCeti.GridDiagram.transpose_OSet {n : ℕ} (G : GridDiagram n) : G.transpose.OSet = Finset.image Prod.swap G.OSet

The O-marking set of the reflected diagram is the diagonal reflection of the original O-marking set.

theorem TauCeti.GridDiagram.transpose_XSet {n : ℕ} (G : GridDiagram n) : G.transpose.XSet = Finset.image Prod.swap G.XSet

The X-marking set of the reflected diagram is the diagonal reflection of the original X-marking set.

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

The marking swap of a grid diagram, obtained by exchanging the O- and X-marking states.

The defining no-double-marking condition is symmetric in the two marking states, so the swap is again a grid diagram.

@[simp]

theorem TauCeti.GridDiagram.swapMarkings_X {n : ℕ} (G : GridDiagram n) : G.swapMarkings.X = G.O

@[simp]

theorem TauCeti.GridDiagram.swapMarkings_O {n : ℕ} (G : GridDiagram n) : G.swapMarkings.O = G.X

@[simp]

theorem TauCeti.GridDiagram.swapMarkings_OSet {n : ℕ} (G : GridDiagram n) : G.swapMarkings.OSet = G.XSet

The O-marking set of the marking swap is the original X-marking set.

@[simp]

theorem TauCeti.GridDiagram.swapMarkings_XSet {n : ℕ} (G : GridDiagram n) : G.swapMarkings.XSet = G.OSet

The X-marking set of the marking swap is the original O-marking set.

@[simp]

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

The marking swap is an involution.

@[simp]

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

Row relabeling commutes with exchanging the two marking states.

@[simp]

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

Column relabeling commutes with exchanging the two marking states.

@[simp]

theorem TauCeti.GridDiagram.swapRows_swapMarkings {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapRows a b G).swapMarkings = swapRows a b G.swapMarkings

Row swaps commute with exchanging the two marking states.

@[simp]

theorem TauCeti.GridDiagram.swapColumns_swapMarkings {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapColumns a b G).swapMarkings = swapColumns a b G.swapMarkings

Column swaps commute with exchanging the two marking states.

@[simp]

theorem TauCeti.GridDiagram.swapMarkings_transpose {n : ℕ} (G : GridDiagram n) : G.swapMarkings.transpose = G.transpose.swapMarkings

The marking swap commutes with the diagonal reflection of a grid diagram.

def TauCeti.GridDiagram.cast {n m : ℕ} (h : n = m) (G : GridDiagram n) : GridDiagram m

Transport a grid diagram along an equality of grid numbers. Both marking states are reindexed along Fin.cast, as computed by cast_O_apply and cast_X_apply.

@[simp]

theorem TauCeti.GridDiagram.cast_rfl {n : ℕ} (G : GridDiagram n) : cast ⋯ G = G

Transporting a grid diagram along the reflexive equality does nothing.

@[simp]

theorem TauCeti.GridDiagram.cast_O_apply {n : ℕ} (G : GridDiagram n) {m : ℕ} (h : n = m) (c : Fin m) : (cast h G).O.toPerm c = Fin.cast h (G.O.toPerm (Fin.cast ⋯ c))

The O marking of a transported grid diagram in a column is the transported O marking of the transported column.

@[simp]

theorem TauCeti.GridDiagram.cast_X_apply {n : ℕ} (G : GridDiagram n) {m : ℕ} (h : n = m) (c : Fin m) : (cast h G).X.toPerm c = Fin.cast h (G.X.toPerm (Fin.cast ⋯ c))

The X marking of a transported grid diagram in a column is the transported X marking of the transported column.