The Alexander grading on knot grid homology over R[U]

For a knot grid the Alexander grading of the concrete cycle quotient transports to the categorical unblocked homology GH⁻. The knot module structure identifies the action of U with that of every grid variable. Since each grid variable lowers Alexander degree by one, so does U. This is the grading property used to define the grid concordance invariant from the top non-torsion degree.

Two knot grids, possibly of different sizes, have isomorphic GH⁻ as Alexander-graded R[U]-modules when some R[U]-linear equivalence between their homologies preserves the Alexander grading (GridDiagram.IsKnot.UnblockedHomologyIsomorphic). This relation is reflexive, symmetric and transitive. The maps that grid moves induce on GH⁻ are initially packaged as semilinear maps over the polynomial rings in the grid variables, along a ring homomorphism such as a renaming of the variables. When that homomorphism commutes with the evaluation V_j ↦ U, the underlying function is R[U]-linear, so such a map that is bijective and preserves the Alexander grading witnesses the relation (GridDiagram.IsKnot.UnblockedHomologyIsomorphic.of_semilinearMap). This is the form in which the grid-move invariance theorems for GH⁻ are stated.

The Alexander grading and the convention that U has degree -1 follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 4 and 6.

noncomputable def TauCeti.GridDiagram.IsKnot.alexanderUnblockedHomologyGrading {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (R : Type u_1) [CommRing R] [CharP R 2] : InternalGrading R ↑(G.unblockedHomology R) ℤ

The Alexander grading of the R[U]-module GH⁻ of a knot grid.

@[simp]

theorem TauCeti.GridDiagram.IsKnot.mem_alexanderUnblockedHomologyGrading_piece_iff {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (R : Type u_1) [CommRing R] [CharP R 2] (a : ℤ) (y : ↑(G.unblockedHomology R)) : y ∈ (hG.alexanderUnblockedHomologyGrading R).piece ℤ a ↔ (CategoryTheory.ConcreteCategory.hom (G.unblockedHomologyIso R).hom) y ∈ (hG.toOddComponentGridDiagram.alexanderHomologyGrading R).piece ℤ a

Membership in a knot grid's Alexander piece is membership in the corresponding piece of the concrete cycle quotient.

theorem TauCeti.GridDiagram.IsKnot.X_smul_mem_alexanderUnblockedHomologyGrading_piece {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (R : Type u_1) [CommRing R] [CharP R 2] {a : ℤ} {y : ↑(G.unblockedHomology R)} (hy : y ∈ (hG.alexanderUnblockedHomologyGrading R).piece ℤ a) : Polynomial.X • y ∈ (hG.alexanderUnblockedHomologyGrading R).piece ℤ (a - 1)

Multiplication by U lowers the Alexander grading of knot grid homology by one.

Isomorphism of graded homologies

def TauCeti.GridDiagram.IsKnot.UnblockedHomologyIsomorphic {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} (hG : G.IsKnot) (hG' : G'.IsKnot) (R : Type u_1) [CommRing R] [CharP R 2] : Prop

The unblocked grid homologies of two knot grids are isomorphic as Alexander-graded R[U]-modules: some R[U]-linear equivalence GH⁻(G) ≃ GH⁻(G') maps each Alexander piece into the piece of the same degree. The two grids may have different sizes.

theorem TauCeti.GridDiagram.IsKnot.UnblockedHomologyIsomorphic.refl {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (R : Type u_1) [CommRing R] [CharP R 2] : hG.UnblockedHomologyIsomorphic hG R

Every knot grid has GH⁻ isomorphic to itself.

theorem TauCeti.GridDiagram.IsKnot.unblockedHomologyIsomorphic_def {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} {hG : G.IsKnot} {hG' : G'.IsKnot} {R : Type u_1} [CommRing R] [CharP R 2] : hG.UnblockedHomologyIsomorphic hG' R ↔ ∃ (e : ↑(G.unblockedHomology R) ≃ₗ[Polynomial R] ↑(G'.unblockedHomology R)), LinearMap.IsHomogeneous (↑e) ((hG.alexanderUnblockedHomologyGrading R).piece ℤ) ((hG'.alexanderUnblockedHomologyGrading R).piece ℤ) 0

Unfold UnblockedHomologyIsomorphic to the existence of a graded equivalence.

theorem TauCeti.GridDiagram.IsKnot.unblockedHomologyIsomorphic_of_eq {n : ℕ} {G : GridDiagram n} {hG : G.IsKnot} {R : Type u_1} [CommRing R] [CharP R 2] {G₁ : GridDiagram n} {hG₁ : G₁.IsKnot} (h : G = G₁) : hG.UnblockedHomologyIsomorphic hG₁ R

Equal knot grids have isomorphic GH⁻. This transports the relation along a propositional equation of diagrams, such as one between two descriptions of a moved diagram.

theorem TauCeti.GridDiagram.IsKnot.UnblockedHomologyIsomorphic.symm {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} {hG : G.IsKnot} {hG' : G'.IsKnot} {R : Type u_1} [CommRing R] [CharP R 2] (h : hG.UnblockedHomologyIsomorphic hG' R) : hG'.UnblockedHomologyIsomorphic hG R

Isomorphism of graded homologies is symmetric: the inverse of a graded equivalence is graded.

theorem TauCeti.GridDiagram.IsKnot.UnblockedHomologyIsomorphic.trans {n m l : ℕ} {G : GridDiagram n} {G' : GridDiagram m} {G'' : GridDiagram l} {hG : G.IsKnot} {hG' : G'.IsKnot} {hG'' : G''.IsKnot} {R : Type u_1} [CommRing R] [CharP R 2] (h : hG.UnblockedHomologyIsomorphic hG' R) (h' : hG'.UnblockedHomologyIsomorphic hG'' R) : hG.UnblockedHomologyIsomorphic hG'' R

Isomorphism of graded homologies is transitive: graded equivalences compose.

theorem TauCeti.GridDiagram.IsKnot.unblockedHomologyIsomorphic_comm {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} {hG : G.IsKnot} {hG' : G'.IsKnot} {R : Type u_1} [CommRing R] [CharP R 2] : hG.UnblockedHomologyIsomorphic hG' R ↔ hG'.UnblockedHomologyIsomorphic hG R

Isomorphism of graded homologies holds in one direction exactly when it holds in the other.

theorem TauCeti.GridDiagram.IsKnot.UnblockedHomologyIsomorphic.of_semilinearMap {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} {hG : G.IsKnot} {hG' : G'.IsKnot} {R : Type u_1} [CommRing R] [CharP R 2] {σ : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R} (hσ : ∀ (p : MvPolynomial (Fin n) R), (MvPolynomial.aeval fun (x : Fin m) => Polynomial.X) (σ p) = (MvPolynomial.aeval fun (x : Fin n) => Polynomial.X) p) (f : ↑(G.unblockedHomology R) →ₛₗ[σ] ↑(G'.unblockedHomology R)) (hf : Function.Bijective ⇑f) (hA : ∀ (a : ℤ), ∀ y ∈ (hG.alexanderUnblockedHomologyGrading R).piece ℤ a, f y ∈ (hG'.alexanderUnblockedHomologyGrading R).piece ℤ a) : hG.UnblockedHomologyIsomorphic hG' R

A bijection between the unblocked homologies of two knot grids makes them isomorphic as Alexander-graded R[U]-modules if it preserves the Alexander grading and is semilinear along a ring homomorphism σ of the polynomial rings that commutes with the evaluation V_j ↦ U, such as a renaming of the variables.