The quantum grading of the Khovanov Frobenius algebra

Khovanov homology is bigraded: besides the cochain degree it carries a quantum degree, which on the rank-two Frobenius algebra V = R[ε] of TauCeti.KnotTheory.Khovanov.Frobenius (with X = ε) puts 1 in degree 1 and X in degree -1. This file constructs that grading and records the degrees of the four Frobenius structure maps:

m : V ⊗ V → V   and   Δ : V → V ⊗ V   have degree -1,
η : R → V       and   ε : V → R       have degree +1,

where V ⊗ V carries the total-degree grading and R the grading concentrated in degree 0. These degrees are what make the differential of the Khovanov complex preserve the quantum grading once each resolution is shifted by its number of 1-smoothings.

With the shift convention (M⟨k⟩)ⱼ = Mⱼ₋ₖ, the regraded algebra W = V⟨-1⟩, which is (TauCeti.Khovanov.quantumGrading R).shift 1, has its unit and multiplication in degree 0 and X in degree -2: it is a graded algebra.

The homogeneous pieces of V form a Mathlib graded object of R-modules, TauCeti.Khovanov.quantumGradedObject R, whose categorical total is identified with the underlying algebra R[ε] by TauCeti.InternalGrading.totalIso.

Main definitions

• TauCeti.Khovanov.quantumDegree: the quantum degrees 1, -1 of the basis vectors 1, ε.
• TauCeti.Khovanov.quantumGrading: the quantum grading of R[ε], an internal grading.
• TauCeti.Khovanov.quantumGradedObject: its homogeneous pieces as a graded object of ModuleCat R.
• TauCeti.Khovanov.instGradedAlgebraShiftOne: the graded algebra W = V⟨-1⟩.

Main results

• TauCeti.Khovanov.mem_quantumGrading_piece_iff: x has degree p exactly when its scalar coordinate vanishes unless p = 1 and its ε-coordinate vanishes unless p = -1.
• TauCeti.Khovanov.quantumGrading_piece_eq_bot: every degree other than ±1 vanishes.
• TauCeti.Khovanov.mul_mem_quantumGrading_piece: multiplication lowers the total degree by one.
• TauCeti.Khovanov.isHomogeneous_mul', TauCeti.Khovanov.isHomogeneous_comul, TauCeti.Khovanov.isHomogeneous_algebraLinearMap, TauCeti.Khovanov.isHomogeneous_counit: the degrees of the four structure maps.

References

• M. Khovanov, A categorification of the Jones polynomial, Duke Math. J. 101 (2000), §2.
• D. Bar-Natan, On Khovanov's categorification of the Jones polynomial, Algebr. Geom. Topol. 2 (2002), §1.

def TauCeti.Khovanov.quantumDegree : Fin 2 → ℤ

The quantum degrees of the basis 1, ε of R[ε] (TauCeti.dualNumberBasis): 1 has degree 1 and X = ε has degree -1.

@[simp]

theorem TauCeti.Khovanov.quantumDegree_zero : quantumDegree 0 = 1

The basis vector 1 has quantum degree 1.

@[simp]

theorem TauCeti.Khovanov.quantumDegree_one : quantumDegree 1 = -1

The basis vector ε has quantum degree -1.

noncomputable def TauCeti.Khovanov.quantumGrading (R : Type u) [CommRing R] : InternalGrading R (DualNumber R) ℤ

The quantum grading of the Khovanov Frobenius algebra R[ε]: the basis vector 1 spans degree 1, the basis vector ε spans degree -1, and every other degree is zero. It is the grading of the free module on the basis 1, ε by TauCeti.Khovanov.quantumDegree, transported to R[ε].

@[reducible, inline]

noncomputable abbrev TauCeti.Khovanov.quantumGradedObject (R : Type u) [CommRing R] : CategoryTheory.GradedObject ℤ (ModuleCat R)

The homogeneous pieces of the quantum grading as a graded object of R-modules: the quantum-graded object V of Khovanov homology. Its categorical total is identified with R[ε] by (TauCeti.Khovanov.quantumGrading R).totalIso.

theorem TauCeti.Khovanov.mem_quantumGrading_piece_iff {R : Type u} [CommRing R] {p : ℤ} {x : DualNumber R} : x ∈ (quantumGrading R).piece ℤ p ↔ (TrivSqZeroExt.fst x ≠ 0 → p = 1) ∧ (TrivSqZeroExt.snd x ≠ 0 → p = -1)

A dual number has quantum degree p exactly when its scalar coordinate vanishes unless p = 1, and its ε-coordinate vanishes unless p = -1.

theorem TauCeti.Khovanov.dualNumberBasis_mem_quantumGrading_piece {R : Type u} [CommRing R] (i : Fin 2) : (dualNumberBasis R) i ∈ (quantumGrading R).piece ℤ (quantumDegree i)

Each basis vector of R[ε] is homogeneous of its quantum degree.

@[simp]

theorem TauCeti.Khovanov.mem_quantumGrading_piece_one_iff {R : Type u} [CommRing R] {x : DualNumber R} : x ∈ (quantumGrading R).piece ℤ 1 ↔ TrivSqZeroExt.snd x = 0

The degree-1 piece consists of the scalars.

@[simp]

theorem TauCeti.Khovanov.mem_quantumGrading_piece_neg_one_iff {R : Type u} [CommRing R] {x : DualNumber R} : x ∈ (quantumGrading R).piece ℤ (-1) ↔ TrivSqZeroExt.fst x = 0

The degree--1 piece consists of the multiples of ε.

theorem TauCeti.Khovanov.quantumGrading_piece_eq_bot {R : Type u} [CommRing R] {p : ℤ} (h1 : p ≠ 1) (h2 : p ≠ -1) : (quantumGrading R).piece ℤ p = ⊥

Every quantum degree other than 1 and -1 is zero.

theorem TauCeti.Khovanov.isZero_quantumGradedObject {R : Type u} [CommRing R] {p : ℤ} (h1 : p ≠ 1) (h2 : p ≠ -1) : CategoryTheory.Limits.IsZero (quantumGradedObject R p)

The quantum-graded object vanishes outside the degrees 1 and -1.

theorem TauCeti.Khovanov.one_mem_quantumGrading_piece_one {R : Type u} [CommRing R] : 1 ∈ (quantumGrading R).piece ℤ 1

The unit 1 has quantum degree 1.

theorem TauCeti.Khovanov.eps_mem_quantumGrading_piece_neg_one {R : Type u} [CommRing R] : DualNumber.eps ∈ (quantumGrading R).piece ℤ (-1)

The generator X = ε has quantum degree -1.

theorem TauCeti.Khovanov.mul_mem_quantumGrading_piece {R : Type u} [CommRing R] {p q : ℤ} {x y : DualNumber R} (hx : x ∈ (quantumGrading R).piece ℤ p) (hy : y ∈ (quantumGrading R).piece ℤ q) : x * y ∈ (quantumGrading R).piece ℤ (p + q - 1)

Multiplication has quantum degree -1: the product of elements of degrees p and q has degree p + q - 1.

theorem TauCeti.Khovanov.isHomogeneous_mul' {R : Type u} [CommRing R] : LinearMap.IsHomogeneous (LinearMap.mul' R (DualNumber R)) (((quantumGrading R).tensorProduct (quantumGrading R)).piece ℤ) ((quantumGrading R).piece ℤ) (-1)

The merge map m : V ⊗ V → V has quantum degree -1, for the total-degree grading of V ⊗ V.

theorem TauCeti.Khovanov.isHomogeneous_comul {R : Type u} [CommRing R] : LinearMap.IsHomogeneous CoalgebraStruct.comul ((quantumGrading R).piece ℤ) (((quantumGrading R).tensorProduct (quantumGrading R)).piece ℤ) (-1)

The split map Δ : V → V ⊗ V has quantum degree -1, for the total-degree grading of V ⊗ V.

theorem TauCeti.Khovanov.isHomogeneous_algebraLinearMap {R : Type u} [CommRing R] : LinearMap.IsHomogeneous (Algebra.linearMap R (DualNumber R)) (trivialGrading R R) ((quantumGrading R).piece ℤ) 1

The unit η : R → V has quantum degree 1, for the grading of R concentrated in degree 0.

theorem TauCeti.Khovanov.isHomogeneous_counit {R : Type u} [CommRing R] : LinearMap.IsHomogeneous CoalgebraStruct.counit ((quantumGrading R).piece ℤ) (trivialGrading R R) 1

The counit ε : V → R has quantum degree 1, for the grading of R concentrated in degree 0.

The regraded algebra W = V⟨-1⟩

instance TauCeti.Khovanov.instGradedMonoidShiftOne (R : Type u) [CommRing R] : SetLike.GradedMonoid (((quantumGrading R).shift 1).piece ℤ)

In the regrading W = V⟨-1⟩ of the quantum grading, in which 1 has degree 0, the unit and multiplication have degree 0.

@[instance_reducible]

noncomputable instance TauCeti.Khovanov.instGradedAlgebraShiftOne (R : Type u) [CommRing R] : GradedAlgebra (((quantumGrading R).shift 1).piece ℤ)

The regrading W = V⟨-1⟩ of the quantum grading makes R[ε] a graded algebra, with 1 in degree 0 and X = ε in degree -2. Its decomposition is the one carried by the internal grading.

theorem TauCeti.Khovanov.eps_mem_quantumGrading_shift_one_piece_neg_two {R : Type u} [CommRing R] : DualNumber.eps ∈ ((quantumGrading R).shift 1).piece ℤ (-2)

In the regrading W = V⟨-1⟩, the generator X = ε has degree -2.