The bigrading of fully blocked grid homology

For a grid diagram with an odd number of components, the fully blocked differential lowers the (O-Maslov, Alexander) bidegree of every state by (1, 0). So taking the homogeneous part of bidegree g of a chain sends cycles to cycles and boundaries to boundaries, and descends to a projection of the fully blocked grid homology GH~ (written $\widetilde{GH}$ in the literature) onto its bidegree-g piece. These pieces form an internal direct sum, so GH~ is a bigraded vector space over ZMod 2. Its Poincaré series, the dimension of each piece recorded as a TauCeti.Bigraded.Series, refines the dimension of GH~: its total dimension is the dimension of GH~.

By Ozsváth--Stipsicz--Szabó, the fully blocked homology of a grid of size n presenting an ℓ-component link is the simply blocked homology of the link tensored with n - ℓ copies of the two-dimensional bigraded space W. So the Poincaré series is the object on which the ⊗ W-stabilization quotient TauCeti.Bigraded.StableSeries acts.

Main definitions

• TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyProjection: the projection of GH~ onto bidegree g.
• TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPiece: the bidegree-g piece of GH~.
• TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyGrading: the bundled internal grading of GH~.
• TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPoincareSeries: the Poincaré series of GH~.

Main results

• TauCeti.OddComponentGridDiagram.mem_bigradedFullyBlockedHomologyPiece_iff_exists: a class is homogeneous of bidegree g exactly when it is the class of a cycle of bidegree g.
• TauCeti.OddComponentGridDiagram.isInternal_bigradedFullyBlockedHomologyPiece: GH~ is the internal direct sum of its homogeneous pieces.
• TauCeti.OddComponentGridDiagram.totalDim_bigradedFullyBlockedHomologyPoincareSeries: the total dimension of the Poincaré series is the dimension of GH~.
• TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPoincareSeries_eq_of_linearEquiv: a linear equivalence of fully blocked homologies commuting with the homogeneous projections identifies the Poincaré series.

References

Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Sections 4.3--4.4, for the bigrading of the fully blocked complex, and Chapter 5 for the factor W in bidegrees (0, 0) and (-1, -1).

Homogeneous parts of cycles and boundaries

theorem TauCeti.OddComponentGridDiagram.bigradedChainInclusion_bigradedChainProjection_mem_fullyBlockedCycles {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) {z : GridChain (ZMod 2) n} (hz : z ∈ (↑G).fullyBlockedCycles) : (G.bigradedChainInclusion (ZMod 2) g) ((G.bigradedChainProjection (ZMod 2) g) z) ∈ (↑G).fullyBlockedCycles

The homogeneous part of a fully blocked cycle is a cycle.

theorem TauCeti.OddComponentGridDiagram.bigradedChainInclusion_bigradedChainProjection_mem_fullyBlockedBoundaries {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) {b : GridChain (ZMod 2) n} (hb : b ∈ (↑G).fullyBlockedBoundaries) : (G.bigradedChainInclusion (ZMod 2) g) ((G.bigradedChainProjection (ZMod 2) g) b) ∈ (↑G).fullyBlockedBoundaries

The homogeneous part of a fully blocked boundary is a boundary.

The homogeneous projections of fully blocked homology

noncomputable def TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyProjection {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) : (↑G).fullyBlockedHomology →ₗ[ZMod 2] (↑G).fullyBlockedHomology

The projection of fully blocked grid homology onto bidegree g: the class of a cycle goes to the class of its homogeneous part of bidegree g.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyProjection_mk {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) (z : ↥(↑G).fullyBlockedCycles) : (G.bigradedFullyBlockedHomologyProjection g) (Submodule.Quotient.mk z) = Submodule.Quotient.mk ⟨(G.bigradedChainInclusion (ZMod 2) g) ((G.bigradedChainProjection (ZMod 2) g) ↑z), ⋯⟩

The projection onto bidegree g sends the class of a cycle to the class of its homogeneous part of bidegree g.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyProjection_apply_self {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) (y : (↑G).fullyBlockedHomology) : (G.bigradedFullyBlockedHomologyProjection g) ((G.bigradedFullyBlockedHomologyProjection g) y) = (G.bigradedFullyBlockedHomologyProjection g) y

The projection onto bidegree g is idempotent.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyProjection_apply_of_ne {n : ℕ} (G : OddComponentGridDiagram n) {g h : ℤ × ℤ} (hgh : g ≠ h) (y : (↑G).fullyBlockedHomology) : (G.bigradedFullyBlockedHomologyProjection g) ((G.bigradedFullyBlockedHomologyProjection h) y) = 0

Projections onto two different bidegrees are orthogonal.

theorem TauCeti.OddComponentGridDiagram.sum_bigradedFullyBlockedHomologyProjection {n : ℕ} (G : OddComponentGridDiagram n) (y : (↑G).fullyBlockedHomology) : ∑ g ∈ G.bidegreeSupport, (G.bigradedFullyBlockedHomologyProjection g) y = y

A homology class is the sum of its homogeneous projections over the occupied bidegrees.

The homogeneous pieces

noncomputable def TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPiece {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) : Submodule (ZMod 2) (↑G).fullyBlockedHomology

The bidegree-g piece of fully blocked grid homology: the image of the projection onto bidegree g. Its elements are the classes of cycles of bidegree g (mem_bigradedFullyBlockedHomologyPiece_iff_exists).

theorem TauCeti.OddComponentGridDiagram.mem_bigradedFullyBlockedHomologyPiece_iff {n : ℕ} (G : OddComponentGridDiagram n) {g : ℤ × ℤ} {y : (↑G).fullyBlockedHomology} : y ∈ G.bigradedFullyBlockedHomologyPiece g ↔ (G.bigradedFullyBlockedHomologyProjection g) y = y

A class lies in the bidegree-g piece exactly when the projection onto bidegree g fixes it.

theorem TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyProjection_mem {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) (y : (↑G).fullyBlockedHomology) : (G.bigradedFullyBlockedHomologyProjection g) y ∈ G.bigradedFullyBlockedHomologyPiece g

The projection onto bidegree g lands in the bidegree-g piece.

theorem TauCeti.OddComponentGridDiagram.mem_bigradedFullyBlockedHomologyPiece_iff_exists {n : ℕ} (G : OddComponentGridDiagram n) {g : ℤ × ℤ} {y : (↑G).fullyBlockedHomology} : y ∈ G.bigradedFullyBlockedHomologyPiece g ↔ ∃ (z : ↥(↑G).fullyBlockedCycles), ↑z ∈ (G.bigradedChainInclusion (ZMod 2) g).range ∧ Submodule.Quotient.mk z = y

A class is homogeneous of bidegree g exactly when it is the class of a cycle of bidegree g.

theorem TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyProjection_eq_zero_of_mem {n : ℕ} (G : OddComponentGridDiagram n) {g h : ℤ × ℤ} (hgh : g ≠ h) {y : (↑G).fullyBlockedHomology} (hy : y ∈ G.bigradedFullyBlockedHomologyPiece h) : (G.bigradedFullyBlockedHomologyProjection g) y = 0

The projection onto bidegree g kills the pieces of every other bidegree.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPiece_eq_bot {n : ℕ} (G : OddComponentGridDiagram n) {g : ℤ × ℤ} (hg : g ∉ G.bidegreeSupport) : G.bigradedFullyBlockedHomologyPiece g = ⊥

Only the bidegrees occupied by grid states carry homology.

theorem TauCeti.OddComponentGridDiagram.isInternal_bigradedFullyBlockedHomologyPiece {n : ℕ} (G : OddComponentGridDiagram n) : DirectSum.IsInternal G.bigradedFullyBlockedHomologyPiece

Fully blocked grid homology is bigraded: it is the internal direct sum of its homogeneous pieces.

noncomputable def TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyGrading {n : ℕ} (G : OddComponentGridDiagram n) : InternalGrading (ZMod 2) (↑G).fullyBlockedHomology (ℤ × ℤ)

The internal (O-Maslov, Alexander) grading of fully blocked grid homology.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyGrading_piece {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) : G.bigradedFullyBlockedHomologyGrading.piece g = G.bigradedFullyBlockedHomologyPiece g

The pieces of the bundled grading are the homogeneous pieces.

@[simp]

theorem TauCeti.OddComponentGridDiagram.coe_decompose_bigradedFullyBlockedHomologyGrading {n : ℕ} (G : OddComponentGridDiagram n) (y : (↑G).fullyBlockedHomology) (g : ℤ × ℤ) : ↑(((DirectSum.decompose G.bigradedFullyBlockedHomologyGrading.piece) y) g) = (G.bigradedFullyBlockedHomologyProjection g) y

The homogeneous components of a class under the bundled grading are its homogeneous projections.

The Poincaré series

noncomputable def TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPoincareSeries {n : ℕ} (G : OddComponentGridDiagram n) : Bigraded.Series

The bigraded Poincaré series of fully blocked grid homology: its coefficient in bidegree g is the dimension of the bidegree-g piece.

@[simp]

theorem TauCeti.OddComponentGridDiagram.coeff_bigradedFullyBlockedHomologyPoincareSeries {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) : G.bigradedFullyBlockedHomologyPoincareSeries.coeff g = Module.finrank (ZMod 2) ↥(G.bigradedFullyBlockedHomologyPiece g)

The coefficient of the Poincaré series in bidegree g is the dimension of the bidegree-g piece of fully blocked homology.

theorem TauCeti.OddComponentGridDiagram.sum_finrank_bigradedFullyBlockedHomologyPiece {n : ℕ} (G : OddComponentGridDiagram n) : ∑ g ∈ G.bidegreeSupport, Module.finrank (ZMod 2) ↥(G.bigradedFullyBlockedHomologyPiece g) = Module.finrank (ZMod 2) (↑G).fullyBlockedHomology

The dimension of fully blocked homology is the sum of the dimensions of its pieces.

@[simp]

theorem TauCeti.OddComponentGridDiagram.totalDim_bigradedFullyBlockedHomologyPoincareSeries {n : ℕ} (G : OddComponentGridDiagram n) : Bigraded.totalDim G.bigradedFullyBlockedHomologyPoincareSeries = Module.finrank (ZMod 2) (↑G).fullyBlockedHomology

The total dimension of the Poincaré series is the dimension of fully blocked homology.

theorem TauCeti.OddComponentGridDiagram.map_bigradedFullyBlockedHomologyPiece {n : ℕ} (G : OddComponentGridDiagram n) {m : ℕ} {G' : OddComponentGridDiagram m} (e : (↑G).fullyBlockedHomology ≃ₗ[ZMod 2] (↑G').fullyBlockedHomology) (he : ∀ (g : ℤ × ℤ) (y : (↑G).fullyBlockedHomology), e ((G.bigradedFullyBlockedHomologyProjection g) y) = (G'.bigradedFullyBlockedHomologyProjection g) (e y)) (g : ℤ × ℤ) : Submodule.map (↑e) (G.bigradedFullyBlockedHomologyPiece g) = G'.bigradedFullyBlockedHomologyPiece g

A linear equivalence of fully blocked homologies that commutes with the homogeneous projections carries each homogeneous piece onto the piece of the same bidegree.

theorem TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPoincareSeries_eq_of_linearEquiv {n : ℕ} (G : OddComponentGridDiagram n) {m : ℕ} {G' : OddComponentGridDiagram m} (e : (↑G).fullyBlockedHomology ≃ₗ[ZMod 2] (↑G').fullyBlockedHomology) (he : ∀ (g : ℤ × ℤ) (y : (↑G).fullyBlockedHomology), e ((G.bigradedFullyBlockedHomologyProjection g) y) = (G'.bigradedFullyBlockedHomologyProjection g) (e y)) : G.bigradedFullyBlockedHomologyPoincareSeries = G'.bigradedFullyBlockedHomologyPoincareSeries

A linear equivalence of fully blocked homologies that commutes with the homogeneous projections identifies their Poincaré series.