The fully blocked grid chain module

This file packages the first algebraic object in the grid-combinatorial lane: the free ZMod 2-module on grid states, together with the linear map whose matrix coefficient from x to y is the parity of fully blocked empty rectangles from x to y.

The square-zero theorem is deliberately not asserted here. This module only supplies the concrete finite free module and differential map to which the later rectangle-pairing proof will apply.

Main definitions

• TauCeti.GridChain: the free module generated by grid states.
• TauCeti.GridChain.transposeEquiv: the linear automorphism of grid chains relabeling each generator by the diagonal reflection of grid states.
• TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator: the row of the fully blocked differential on one generator.
• TauCeti.GridDiagram.fullyBlockedDifferential: the corresponding ZMod 2-linear map.
• TauCeti.GridDiagram.exists_swapColumns_of_fullyBlockedDifferentialOnGenerator_ne_zero: the fully blocked differential of a generator is supported on its column transpositions.

References

The coefficient formula follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

@[reducible, inline]

abbrev TauCeti.GridChain (R : Type u_1) [Zero R] (n : ℕ) : Type u_1

Finitely supported coefficient functions on grid states of size n.

When R has the needed algebraic structure, this is the free module generated by those grid states with coefficients in R.

noncomputable def TauCeti.GridChain.transposeEquiv (R : Type u_1) [Semiring R] (n : ℕ) : GridChain R n ≃ₗ[R] GridChain R n

The linear automorphism of grid chains induced by the diagonal reflection of grid states.

Because GridState.transpose is an involution, relabeling each generator x by x.transpose gives a linear automorphism of the chain module GridChain R n.

@[simp]

theorem TauCeti.GridChain.transposeEquiv_single {R : Type u_1} [Semiring R] {n : ℕ} (x : GridState n) (a : R) : (transposeEquiv R n) (Finsupp.single x a) = Finsupp.single x.transpose a

The transpose relabeling sends the generator x to the generator x.transpose.

@[simp]

theorem TauCeti.GridChain.transposeEquiv_apply {R : Type u_1} [Semiring R] {n : ℕ} (f : GridChain R n) (y : GridState n) : ((transposeEquiv R n) f) y = f y.transpose

The y-coefficient of a relabeled chain is the y.transpose-coefficient of the original chain.

@[simp]

theorem TauCeti.GridChain.transposeEquiv_symm {R : Type u_1} [Semiring R] {n : ℕ} : (transposeEquiv R n).symm = transposeEquiv R n

The transpose relabeling is its own inverse: since GridState.transpose is an involution, the inverse automorphism is again transposeEquiv. This lets the forward lemmas transposeEquiv_single and transposeEquiv_apply also drive the inverse map.

noncomputable def TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator {n : ℕ} (G : GridDiagram n) (x : GridState n) : GridChain (ZMod 2) n

The value of the fully blocked differential on a single grid-state generator.

Its y-coefficient is the parity of fully blocked empty rectangles from x to y.

theorem TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator_def {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.fullyBlockedDifferentialOnGenerator x = ∑ y : GridState n, Finsupp.single y (G.fullyBlockedRectangleCount x y)

The generator row of the fully blocked differential is the finite sum of rectangle-count coefficients.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator_apply {n : ℕ} (G : GridDiagram n) (x y : GridState n) : (G.fullyBlockedDifferentialOnGenerator x) y = G.fullyBlockedRectangleCount x y

The y-coefficient of the fully blocked differential on the generator x.

theorem TauCeti.GridDiagram.exists_swapColumns_of_fullyBlockedDifferentialOnGenerator_ne_zero {n : ℕ} (G : GridDiagram n) {x y : GridState n} (h : (G.fullyBlockedDifferentialOnGenerator x) y ≠ 0) : ∃ (a : Fin n) (b : Fin n), a ≠ b ∧ y = GridState.swapColumns a b x

The fully blocked differential of a generator is supported on the column transpositions of that generator: if the y-coefficient is nonzero, then y is a column transposition of x.

noncomputable def TauCeti.GridDiagram.fullyBlockedDifferential {n : ℕ} (G : GridDiagram n) : GridChain (ZMod 2) n →ₗ[ZMod 2] GridChain (ZMod 2) n

The fully blocked grid differential as a ZMod 2-linear map on chains.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedDifferential_single {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.fullyBlockedDifferential (Finsupp.single x 1) = G.fullyBlockedDifferentialOnGenerator x

The fully blocked differential sends a single generator to the corresponding rectangle-count row.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_single_apply {n : ℕ} (G : GridDiagram n) (x y : GridState n) : (G.fullyBlockedDifferential (Finsupp.single x 1)) y = G.fullyBlockedRectangleCount x y

The matrix coefficient of the fully blocked differential on a single generator is the fully blocked rectangle count.

theorem TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator_apply_self {n : ℕ} (G : GridDiagram n) (x : GridState n) : (G.fullyBlockedDifferentialOnGenerator x) x = 0

There is no self-term in the fully blocked differential of a generator.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_single_apply_self {n : ℕ} (G : GridDiagram n) (x : GridState n) : (G.fullyBlockedDifferential (Finsupp.single x 1)) x = 0

The self-coefficient of the fully blocked differential on a single generator is zero.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_apply {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) : G.fullyBlockedDifferential c = Finsupp.sum c fun (x : GridState n) (a : ZMod 2) => a • G.fullyBlockedDifferentialOnGenerator x

The fully blocked differential is the finite sum of its generator rows over the support of a chain.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedDifferential_apply_apply {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) (y : GridState n) : (G.fullyBlockedDifferential c) y = Finsupp.sum c fun (x : GridState n) (a : ZMod 2) => a * G.fullyBlockedRectangleCount x y

The coefficient formula for the fully blocked differential on an arbitrary chain.