The simply blocked grid map

The unblocked grid complex GC⁻ has one polynomial variable V_c for each O-marking. Blocking the O-marking in a chosen column i means setting V_i = 0. The resulting simply blocked construction keeps the variables indexed by the other columns and counts exactly the empty rectangles which cover neither an X-marking nor the blocked O-marking. This specialization is defined for every grid diagram and every commutative coefficient semiring. For a knot grid over a coefficient semiring of characteristic two, it is the simply blocked differential. Outside characteristic two it is only the unsigned candidate linear map: exactly as for the unblocked differential it specializes, the unsigned rectangle count squares to zero only after a sign assignment, and signs use additive inverses, so the sign-corrected construction needs a commutative coefficient ring. For a multi-component link, the corresponding simply blocked theory instead requires blocking one O-marking on each component.

The coefficients form the polynomial semiring R[V_c | c ≠ i], rather than one carrying a redundant variable known to act by zero. Mathlib's MvPolynomial.killCompl makes the relation to GC⁻ explicit, while simplyBlockedCoefficient_eq_sum identifies the terms that remain after specialization.

Main definitions

• TauCeti.GridChainHat: the free module underlying the one-variable specialization.
• TauCeti.simplyBlockedRingHom: setting V_i to zero, as a ring homomorphism.
• TauCeti.simplyBlockedSpecialization: coefficientwise specialization of GC⁻ at V_i = 0.
• TauCeti.simplyBlockedRenameEquiv: rename surviving variables and transport the blocked column.
• TauCeti.simplyBlockedRenameRingHomInvPair, TauCeti.simplyBlockedRenameRingHomInvPairSymm: the renaming and its inverse form a RingHomInvPair.
• TauCeti.simplyBlockedMap: the endomorphism of GC^ induced by an endomorphism of GC⁻.
• TauCeti.GridDiagram.simplyBlockedRectangles: the empty, X-avoiding rectangles which also avoid the chosen O-marking.
• TauCeti.GridDiagram.simplyBlockedCoefficient: the matrix coefficient of the specialized map.
• TauCeti.GridDiagram.simplyBlockedDifferential: the map obtained from GC⁻ by specializing V_i to zero.

Main results

• TauCeti.simplyBlockedRingHom_rename: blocking commutes with column renaming when the blocked column is transported.
• TauCeti.simplyBlockedSpecialization_apply_linearMap: specialization intertwines an endomorphism of GC⁻ with its specialization TauCeti.simplyBlockedMap.
• TauCeti.simplyBlockedSpecialization_surjective and TauCeti.exact_X_smul_simplyBlockedSpecialization: specialization presents the specialized chain module as the quotient of GC⁻ by the multiples of V_i, which TauCeti.X_smul_gridChainMinus_injective says form a copy of GC⁻.
• TauCeti.GridDiagram.simplyBlockedCoefficient_eq_sum: a matrix coefficient is the sum, over the rectangles which avoid the blocked O-marking, of the product of the variables of the other O-markings the rectangle covers.
• TauCeti.GridDiagram.simplyBlockedSpecialization_unblockedDifferential: coefficientwise specialization intertwines the unblocked differential with the simply blocked map, so the latter really is the V_i = 0 reduction of the former.

References

The specialization and rectangle formula follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

@[reducible, inline]

abbrev TauCeti.GridChainHat (R : Type u_1) [CommSemiring R] (n : ℕ) (i : Fin n) : Type u_1

The chain module underlying the one-variable specialization, freely generated by grid states over the polynomial semiring in the columns other than the blocked column i. Its homology, for a knot grid in characteristic two, is the simply blocked grid homology, which is not defined here.

@[reducible, inline]

noncomputable abbrev TauCeti.simplyBlockedRingHom {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) : MvPolynomial (Fin n) R →+* MvPolynomial { c : Fin n // c ≠ i } R

Setting the blocked variable V_i to zero, as a ring homomorphism R[V₀, …, V_{n-1}] → R[V_c | c ≠ i]. It is the homomorphism over which TauCeti.simplyBlockedSpecialization is semilinear.

@[simp]

theorem TauCeti.simplyBlockedRingHom_apply {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) (p : MvPolynomial (Fin n) R) : (simplyBlockedRingHom R i) p = (MvPolynomial.killCompl ⋯) p

The coefficient specialization is MvPolynomial.killCompl.

theorem TauCeti.simplyBlockedRingHom_X_eq_zero {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) : (simplyBlockedRingHom R i) (MvPolynomial.X i) = 0

The blocked variable specializes to zero.

Not a simp lemma: TauCeti.simplyBlockedRingHom_apply and MvPolynomial.killCompl_X_of_notMem_range already rewrite the left-hand side to 0.

noncomputable def TauCeti.simplyBlockedSpecialization {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) : GridChainMinus R n →ₛₗ[simplyBlockedRingHom R i] GridChainHat R n i

Coefficientwise specialization of an unblocked grid chain at V_i = 0.

This is semilinear over MvPolynomial.killCompl: specializing a polynomial multiple of a chain specializes both the scalar and every coefficient.

@[simp]

theorem TauCeti.simplyBlockedSpecialization_apply {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) (c : GridChainMinus R n) (x : GridState n) : ((simplyBlockedSpecialization R i) c) x = (MvPolynomial.killCompl ⋯) (c x)

Specializing a grid chain applies MvPolynomial.killCompl to each coefficient.

@[simp]

theorem TauCeti.simplyBlockedSpecialization_single {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) (x : GridState n) (a : MvPolynomial (Fin n) R) : (simplyBlockedSpecialization R i) (Finsupp.single x a) = Finsupp.single x ((MvPolynomial.killCompl ⋯) a)

Specialization sends a single supported coefficient to the single supported specialized coefficient.

noncomputable def TauCeti.simplyBlockedRenameEquiv {n m : ℕ} (R : Type u_1) [CommSemiring R] (e : Fin n ≃ Fin m) (i : Fin n) : MvPolynomial { c : Fin n // c ≠ i } R ≃ₐ[R] MvPolynomial { c : Fin m // c ≠ e i } R

Renaming the unblocked columns also renames the surviving variables, carrying the blocked column i to e i.

instance TauCeti.simplyBlockedRenameRingHomInvPair {n m : ℕ} (R : Type u_1) [CommSemiring R] (e : Fin n ≃ Fin m) (i : Fin n) : RingHomInvPair ↑(simplyBlockedRenameEquiv R e i).toRingEquiv ↑(simplyBlockedRenameEquiv R e i).toRingEquiv.symm

Renaming the surviving variables and its inverse form a RingHomInvPair, so that maps semilinear along the renaming can be inverted.

instance TauCeti.simplyBlockedRenameRingHomInvPairSymm {n m : ℕ} (R : Type u_1) [CommSemiring R] (e : Fin n ≃ Fin m) (i : Fin n) : RingHomInvPair ↑(simplyBlockedRenameEquiv R e i).toRingEquiv.symm ↑(simplyBlockedRenameEquiv R e i).toRingEquiv

The inverse renaming of the surviving variables and the forward renaming form a RingHomInvPair.

@[simp]

theorem TauCeti.simplyBlockedRenameEquiv_X {n m : ℕ} (R : Type u_1) [CommSemiring R] (e : Fin n ≃ Fin m) (i : Fin n) (c : { c : Fin n // c ≠ i }) : (simplyBlockedRenameEquiv R e i) (MvPolynomial.X c) = MvPolynomial.X ⟨e ↑c, ⋯⟩

A surviving variable is renamed by the underlying column equivalence.

theorem TauCeti.simplyBlockedRingHom_rename {n m : ℕ} (R : Type u_1) [CommSemiring R] (e : Fin n ≃ Fin m) (i : Fin n) (p : MvPolynomial (Fin n) R) : (simplyBlockedRingHom R (e i)) ((MvPolynomial.rename ⇑e) p) = (simplyBlockedRenameEquiv R e i) ((simplyBlockedRingHom R i) p)

Blocking a column and then renaming the surviving variables agrees with renaming all columns first and blocking the image column.

Specializing linear maps

theorem TauCeti.simplyBlockedSpecialization_apply_eq_of_single {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) {f : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n} {g : GridChainHat R n i →ₗ[MvPolynomial { c : Fin n // c ≠ i } R] GridChainHat R n i} (h : ∀ (x : GridState n), (simplyBlockedSpecialization R i) (f (Finsupp.single x 1)) = g (Finsupp.single x 1)) (c : GridChainMinus R n) : (simplyBlockedSpecialization R i) (f c) = g ((simplyBlockedSpecialization R i) c)

Specialization at V_i = 0 intertwines a linear map of GC⁻ with a linear map of GC^ as soon as it does so on the generators.

noncomputable def TauCeti.simplyBlockedMap {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) (f : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n) : GridChainHat R n i →ₗ[MvPolynomial { c : Fin n // c ≠ i } R] GridChainHat R n i

The endomorphism of GC^ obtained from an endomorphism f of GC⁻ by setting V_i = 0: it sends each generator to the specialization of its image under f.

theorem TauCeti.simplyBlockedMap_single {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) (f : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n) (x : GridState n) : (simplyBlockedMap R i f) (Finsupp.single x 1) = (simplyBlockedSpecialization R i) (f (Finsupp.single x 1))

On a generator, the specialized map is the specialization of the original map.

@[simp]

theorem TauCeti.simplyBlockedMap_single_apply {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) (f : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n) (x y : GridState n) : ((simplyBlockedMap R i f) (Finsupp.single x 1)) y = (MvPolynomial.killCompl ⋯) ((f (Finsupp.single x 1)) y)

The matrix entries of the specialized map are the specialized matrix entries.

@[simp]

theorem TauCeti.simplyBlockedMap_apply_apply {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) (f : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n) (c : GridChainHat R n i) (y : GridState n) : ((simplyBlockedMap R i f) c) y = Finsupp.sum c fun (x : GridState n) (p : MvPolynomial { c : Fin n // c ≠ i } R) => p * (MvPolynomial.killCompl ⋯) ((f (Finsupp.single x 1)) y)

The specialized map multiplies a chain by the specialized matrix.

theorem TauCeti.simplyBlockedSpecialization_apply_linearMap {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) (f : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n) (c : GridChainMinus R n) : (simplyBlockedSpecialization R i) (f c) = (simplyBlockedMap R i f) ((simplyBlockedSpecialization R i) c)

Specialization at V_i = 0 intertwines a map of GC⁻ with its specialization.

Not a simp lemma: its left-hand side matches every specialized linear-map application, which would bypass the intertwining lemmas of named specialized maps.

theorem TauCeti.killCompl_monomial_sum_single_one {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) (s : Finset (Fin n)) : (MvPolynomial.killCompl ⋯) ((MvPolynomial.monomial (∑ c ∈ s, Finsupp.single c 1)) 1) = if i ∈ s then 0 else ∏ c ∈ Finset.subtype (fun (x : Fin n) => x ≠ i) s, MvPolynomial.X c

Setting V_i = 0 in a squarefree monomial discards it if it contains V_i; otherwise it leaves the product of the same variables.

Specialization as a quotient map

theorem TauCeti.simplyBlockedRingHom_surjective {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) : Function.Surjective ⇑(simplyBlockedRingHom R i)

The coefficient specialization is surjective.

theorem TauCeti.simplyBlockedSpecialization_surjective {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) : Function.Surjective ⇑(simplyBlockedSpecialization R i)

Specialization at V_i = 0 is surjective: renaming the surviving variables back is a section of it.

theorem TauCeti.X_smul_gridChainMinus_injective {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) : Function.Injective fun (c : GridChainMinus R n) => MvPolynomial.X i • c

Multiplication by the blocked variable V_i is injective on the unblocked grid chain module.

theorem TauCeti.exact_X_mul_simplyBlockedRingHom {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) : Function.Exact (fun (p : MvPolynomial (Fin n) R) => MvPolynomial.X i * p) ⇑(simplyBlockedRingHom R i)

Multiplication by V_i and coefficient specialization form an exact pair.

theorem TauCeti.exact_X_smul_simplyBlockedSpecialization {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) : Function.Exact (fun (c : GridChainMinus R n) => MvPolynomial.X i • c) ⇑(simplyBlockedSpecialization R i)

The chains killed by specialization at V_i = 0 are exactly the multiples of V_i: together with TauCeti.X_smul_gridChainMinus_injective and TauCeti.simplyBlockedSpecialization_surjective this presents the specialized chain module as the quotient of GC⁻ by a copy of itself.

@[simp]

theorem TauCeti.simplyBlockedSpecialization_X_smul {n : ℕ} (R : Type u_1) [CommSemiring R] (i : Fin n) (c : GridChainMinus R n) : (simplyBlockedSpecialization R i) (MvPolynomial.X i • c) = 0

Specialization at V_i = 0 kills multiples of V_i.

@[simp]

theorem TauCeti.GridDiagram.killCompl_OMonomial_eq_zero_of_mem {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {i : Fin n} {r : GridRectangle n} (hi : i ∈ G.OColumns r) : (MvPolynomial.killCompl ⋯) (G.OMonomial R r) = 0

A rectangle covering the blocked O-marking has weight zero after specialization.

@[simp]

theorem TauCeti.GridDiagram.killCompl_OMonomial_eq_prod_of_notMem {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {i : Fin n} {r : GridRectangle n} (hi : i ∉ G.OColumns r) : (MvPolynomial.killCompl ⋯) (G.OMonomial R r) = ∏ c ∈ Finset.subtype (fun (x : Fin n) => x ≠ i) (G.OColumns r), MvPolynomial.X c

A rectangle avoiding the blocked O-marking keeps as its weight the product of the variables of the other O-markings it covers.

noncomputable def TauCeti.GridDiagram.simplyBlockedRectangles {n : ℕ} (G : GridDiagram n) (i : Fin n) (x y : GridState n) : Finset (GridRectangleBetween x y)

The rectangles counted after blocking column i: unblocked rectangles which do not cover the O-marking in column i.

@[simp]

theorem TauCeti.GridDiagram.mem_simplyBlockedRectangles {n : ℕ} (G : GridDiagram n) (i : Fin n) {x y : GridState n} (r : GridRectangleBetween x y) : r ∈ G.simplyBlockedRectangles i x y ↔ r.IsEmpty ∧ Disjoint r.toGridRectangle.coveredSquares G.XSet ∧ (i, G.O.toPerm i) ∉ r.toGridRectangle.coveredSquares

Membership in the simply blocked rectangle set is emptiness, X-avoidance, and avoidance of the O-marking in the selected column.

theorem TauCeti.GridDiagram.simplyBlockedRectangles_subset_unblockedRectangles {n : ℕ} (G : GridDiagram n) (i : Fin n) (x y : GridState n) : G.simplyBlockedRectangles i x y ⊆ G.unblockedRectangles x y

Simply blocked rectangles are among those counted by the unblocked differential.

@[simp]

theorem TauCeti.GridDiagram.simplyBlockedRectangles_self {n : ℕ} (G : GridDiagram n) (i : Fin n) (x : GridState n) : G.simplyBlockedRectangles i x x = ∅

There are no simply blocked rectangles from a grid state to itself.

noncomputable def TauCeti.GridDiagram.simplyBlockedCoefficient {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) (x y : GridState n) : MvPolynomial { c : Fin n // c ≠ i } R

The matrix coefficient of the simply blocked map, obtained by specializing the corresponding coefficient of GC⁻.

theorem TauCeti.GridDiagram.simplyBlockedCoefficient_eq_sum {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) (x y : GridState n) : G.simplyBlockedCoefficient R i x y = ∑ r ∈ G.simplyBlockedRectangles i x y, ∏ c ∈ Finset.subtype (fun (x : Fin n) => x ≠ i) (G.OColumns r.toGridRectangle), MvPolynomial.X c

The simply blocked coefficient is the finite sum over the contributing rectangles. Terms covering the blocked marking disappear; each of the other terms is the product of the variables of the remaining O-markings the rectangle covers.

@[simp]

theorem TauCeti.GridDiagram.simplyBlockedCoefficient_self {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) (x : GridState n) : G.simplyBlockedCoefficient R i x x = 0

The simply blocked map has no diagonal matrix coefficient.

noncomputable def TauCeti.GridDiagram.simplyBlockedDifferentialOnGenerator {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) (x : GridState n) : GridChainHat R n i

The value of the simply blocked map on one grid-state generator.

@[simp]

theorem TauCeti.GridDiagram.simplyBlockedDifferentialOnGenerator_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) (x y : GridState n) : (G.simplyBlockedDifferentialOnGenerator R i x) y = G.simplyBlockedCoefficient R i x y

The y-coefficient of the simply blocked map on the generator x.

theorem TauCeti.GridDiagram.simplyBlockedDifferentialOnGenerator_support_subset {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) (x : GridState n) : (G.simplyBlockedDifferentialOnGenerator R i x).support ⊆ x.columnSwapNeighbors

The simply blocked map of a generator is supported on its column transpositions.

@[simp]

theorem TauCeti.GridDiagram.simplyBlockedSpecialization_unblockedDifferentialOnGenerator {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) (x : GridState n) : (simplyBlockedSpecialization R i) (G.unblockedDifferentialOnGenerator R x) = G.simplyBlockedDifferentialOnGenerator R i x

Specializing the unblocked differential of a generator gives its simply blocked row.

noncomputable def TauCeti.GridDiagram.simplyBlockedDifferential {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) : GridChainHat R n i →ₗ[MvPolynomial { c : Fin n // c ≠ i } R] GridChainHat R n i

The linear map obtained from the GC⁻ differential by setting V_i = 0. For a knot grid over a coefficient semiring of characteristic two it is the simply blocked differential; outside characteristic two it is only the unsigned candidate map, since sign correction uses additive inverses and so needs a commutative coefficient ring. A link with multiple components requires one blocked marking on each component instead.

@[simp]

theorem TauCeti.GridDiagram.simplyBlockedDifferential_single {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) (x : GridState n) : (G.simplyBlockedDifferential R i) (Finsupp.single x 1) = G.simplyBlockedDifferentialOnGenerator R i x

The simply blocked map sends a single generator to its rectangle-weight row.

theorem TauCeti.GridDiagram.simplyBlockedDifferential_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) (c : GridChainHat R n i) : (G.simplyBlockedDifferential R i) c = Finsupp.sum c fun (x : GridState n) (a : MvPolynomial { c : Fin n // c ≠ i } R) => a • G.simplyBlockedDifferentialOnGenerator R i x

The simply blocked map is the finite sum of its generator rows over the support of a chain.

@[simp]

theorem TauCeti.GridDiagram.simplyBlockedDifferential_apply_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) (c : GridChainHat R n i) (y : GridState n) : ((G.simplyBlockedDifferential R i) c) y = Finsupp.sum c fun (x : GridState n) (a : MvPolynomial { c : Fin n // c ≠ i } R) => a * G.simplyBlockedCoefficient R i x y

The coefficient formula for the simply blocked map on an arbitrary chain.

@[simp]

theorem TauCeti.GridDiagram.simplyBlockedSpecialization_unblockedDifferential {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (i : Fin n) (c : GridChainMinus R n) : (simplyBlockedSpecialization R i) ((G.unblockedDifferential R) c) = (G.simplyBlockedDifferential R i) ((simplyBlockedSpecialization R i) c)

Coefficientwise specialization intertwines the unblocked and simply blocked maps.