The bigrading of unblocked grid homology

The homogeneous cycles and their classes give an internal direct sum decomposition of GH⁻ by (O-Maslov, Alexander) degree. The differential has degree (-1, 0), and each variable has degree (-2, -1). Homogeneous projection preserves both cycles and boundaries, so a class has a homogeneous representative precisely when it belongs to the corresponding piece.

The cycle pieces are defined over commutative semirings, and their internal direct sum decomposition is available over commutative rings, using the chain decomposition isInternal_bigradedChainMinusPiece, whose internality criterion requires a ring. The homology grading and its consequences require a commutative ring of characteristic two ([CommRing R] [CharP R 2]).

These pieces are modules over the ground ring, not over the polynomial coefficient ring. As for the chain bigrading, an odd number of link components ensures integral Alexander degrees. The decomposition allows degree-preserving homology comparisons to be restricted to each bidegree without choosing cycle representatives.

References

Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Sections 4.3 and 4.6.

noncomputable def TauCeti.OddComponentGridDiagram.bigradedUnblockedCyclesPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (g : ℤ × ℤ) : Submodule R ↥((↑G).unblockedDifferential R).ker

The cycles of GC⁻ homogeneous of bidegree g.

@[simp]

theorem TauCeti.OddComponentGridDiagram.mem_bigradedUnblockedCyclesPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] {g : ℤ × ℤ} {z : ↥((↑G).unblockedDifferential R).ker} : z ∈ G.bigradedUnblockedCyclesPiece R g ↔ ↑z ∈ G.bigradedChainMinusPiece R g

Homogeneity of a cycle is homogeneity of its underlying chain.

theorem TauCeti.OddComponentGridDiagram.isInternal_bigradedUnblockedCyclesPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] : DirectSum.IsInternal (G.bigradedUnblockedCyclesPiece R)

The homogeneous cycle modules form an internal direct sum.

noncomputable def TauCeti.OddComponentGridDiagram.bigradedUnblockedHomologyGrading {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : InternalGrading R (↑((↑G).unblockedHomology R)) (ℤ × ℤ)

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

noncomputable def TauCeti.OddComponentGridDiagram.bigradedUnblockedHomologyPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (g : ℤ × ℤ) : Submodule R ↑((↑G).unblockedHomology R)

The bidegree-g piece of GH⁻: classes of cycles homogeneous of bidegree g.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedUnblockedHomologyGrading_piece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (g : ℤ × ℤ) : (G.bigradedUnblockedHomologyGrading R).piece g = G.bigradedUnblockedHomologyPiece R g

The pieces of the bundled homology grading are the homogeneous homology pieces.

theorem TauCeti.OddComponentGridDiagram.mem_bigradedUnblockedHomologyPiece_iff {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] {g : ℤ × ℤ} {y : ↑((↑G).unblockedHomology R)} : y ∈ G.bigradedUnblockedHomologyPiece R g ↔ ∃ (z : ↥((↑G).unblockedDifferential R).ker), ↑z ∈ G.bigradedChainMinusPiece R g ∧ ((↑G).unblockedHomologyClass R) z = y

A class has bidegree g exactly when it has a cycle representative of that bidegree.

theorem TauCeti.OddComponentGridDiagram.unblockedHomologyClass_mem_bigradedUnblockedHomologyPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] {g : ℤ × ℤ} {z : ↥((↑G).unblockedDifferential R).ker} (hz : ↑z ∈ G.bigradedChainMinusPiece R g) : ((↑G).unblockedHomologyClass R) z ∈ G.bigradedUnblockedHomologyPiece R g

The class of a homogeneous cycle lies in the homology piece of the same bidegree.

theorem TauCeti.OddComponentGridDiagram.iSup_bigradedUnblockedHomologyPiece_eq_top {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : ⨆ (g : ℤ × ℤ), G.bigradedUnblockedHomologyPiece R g = ⊤

The bigraded homology pieces span GH⁻.

theorem TauCeti.OddComponentGridDiagram.iSupIndep_bigradedUnblockedHomologyPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : iSupIndep (G.bigradedUnblockedHomologyPiece R)

The bigraded homology pieces are independent: a homogeneous boundary can be detected in its own bidegree.

theorem TauCeti.OddComponentGridDiagram.isInternal_bigradedUnblockedHomologyPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : DirectSum.IsInternal (G.bigradedUnblockedHomologyPiece R)

GH⁻ is the internal direct sum of its (O-Maslov, Alexander) pieces.

theorem TauCeti.OddComponentGridDiagram.monomial_smul_mem_bigradedUnblockedHomologyPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (d : Fin n →₀ ℕ) (a : R) {g : ℤ × ℤ} {y : ↑((↑G).unblockedHomology R)} (hy : y ∈ G.bigradedUnblockedHomologyPiece R g) : (MvPolynomial.monomial d) a • y ∈ G.bigradedUnblockedHomologyPiece R (g - (2 * ↑(Finsupp.degree d), ↑(Finsupp.degree d)))

Multiplication by a monomial of total degree d.degree lowers homology bidegree by (2 * d.degree, d.degree).

theorem TauCeti.OddComponentGridDiagram.X_smul_mem_bigradedUnblockedHomologyPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Fin n) {g : ℤ × ℤ} {y : ↑((↑G).unblockedHomology R)} (hy : y ∈ G.bigradedUnblockedHomologyPiece R g) : MvPolynomial.X i • y ∈ G.bigradedUnblockedHomologyPiece R (g - (2, 1))

Multiplication by a grid variable lowers homology bidegree by (2, 1).

theorem TauCeti.OddComponentGridDiagram.unblockedHomologyEquiv_mem_bigradedPiece_iff {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (G' : OddComponentGridDiagram n) {σ σ' : MvPolynomial (Fin n) R →+* MvPolynomial (Fin n) R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : GridChainMinus R n ≃ₛₗ[σ] GridChainMinus R n) (he : ∀ (c : GridChainMinus R n), ((↑G').unblockedDifferential R) (e c) = e (((↑G).unblockedDifferential R) c)) (f : ↑((↑G).unblockedHomology R) ≃ₛₗ[σ] ↑((↑G').unblockedHomology R)) (hf : ∀ (z : ↥((↑G).unblockedDifferential R).ker), f (((↑G).unblockedHomologyClass R) z) = ((↑G').unblockedHomologyClass R) ⟨e ↑z, ⋯⟩) (hg : ∀ (g : ℤ × ℤ) (c : GridChainMinus R n), e c ∈ G'.bigradedChainMinusPiece R g ↔ c ∈ G.bigradedChainMinusPiece R g) {g : ℤ × ℤ} {y : ↑((↑G).unblockedHomology R)} : f y ∈ G'.bigradedUnblockedHomologyPiece R g ↔ y ∈ G.bigradedUnblockedHomologyPiece R g

An equivalence intertwining the unblocked differentials identifies each homology bidegree if it identifies each chain bidegree. The converse membership implication includes the inverse homology equivalence, so the image is the entire homogeneous piece.