The Khovanov Frobenius algebra

Ordinary Khovanov homology assigns to each resolved circle a copy of the rank-two Frobenius algebra R[X]/(X²). Here it is the dual numbers R[ε], with X = ε, together with the comultiplication and counit

Δ 1 = 1 ⊗ ε + ε ⊗ 1,     Δ ε = ε ⊗ ε,
counit 1 = 0,            counit ε = 1.

Merging two circles acts by multiplication and splitting one circle acts by Δ.

This coalgebra structure is a choice, not a canonical structure on every algebra of dual numbers, so it is installed only as scoped instances in TauCeti.Khovanov; open TauCeti.Khovanov (or open scoped TauCeti.Khovanov) to use it.

Main definitions and results

• TauCeti.Khovanov.coalgebra: the Khovanov coalgebra structure on R[ε].
• TauCeti.Khovanov.comul_one, TauCeti.Khovanov.comul_eps, DualNumber.khovanov_counit_apply: the values of the comultiplication and counit.
• TauCeti.Khovanov.isCocomm: the comultiplication is cocommutative.
• TauCeti.Khovanov.isFrobenius: R[ε] satisfies the Frobenius equation. Through Mathlib's Coalgebra.IsFrobenius.left_eq_comul_comp_mul' and Coalgebra.IsFrobenius.right_eq_comul_comp_mul' this identifies Δ ∘ m with both mixed composites (m ⊗ id) ∘ (id ⊗ Δ) and (id ⊗ m) ∘ (Δ ⊗ id).
• TauCeti.Khovanov.mul_compr₂_counit: the Frobenius form (a, b) ↦ counit (a * b) is the perfect pairing TauCeti.dualNumberTracePairing.
• TauCeti.Khovanov.counit_basis_mul_basis_rev: the basis ε, 1 is dual to the basis 1, ε for that pairing; DualNumber.khovanov_counit_eps_mul_smul_one_add_counit_smul_eps is the resulting expansion a = counit (ε * a) • 1 + counit a • ε.
• TauCeti.Khovanov.baseChangeCoalgEquiv: for a commutative R-algebra S, the algebra isomorphism S ⊗[R] R[ε] ≃ S[ε] is an isomorphism of S-coalgebras, so the Khovanov Frobenius algebra over S is the base change of the one over R.

References

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

@[instance_reducible]

noncomputable def TauCeti.Khovanov.coalgebra (R : Type u_1) [CommSemiring R] : Coalgebra R (DualNumber R)

The Khovanov coalgebra structure on the dual numbers R[ε]: the comultiplication is Δ (a + b ε) = a • (1 ⊗ ε + ε ⊗ 1) + b • (ε ⊗ ε) and the counit is a + b ε ↦ b.

theorem DualNumber.khovanov_comul_apply {R : Type u_1} [CommSemiring R] (x : DualNumber R) : CoalgebraStruct.comul x = TrivSqZeroExt.fst x • (1 ⊗ₜ[R] eps + eps ⊗ₜ[R] 1) + TrivSqZeroExt.snd x • eps ⊗ₜ[R] eps

The Khovanov comultiplication of a general dual number.

@[simp]

theorem DualNumber.khovanov_counit_apply {R : Type u_1} [CommSemiring R] (x : DualNumber R) : CoalgebraStruct.counit x = TrivSqZeroExt.snd x

The Khovanov counit reads off the coefficient of ε.

@[simp]

theorem TauCeti.Khovanov.comul_one (R : Type u_1) [CommSemiring R] : CoalgebraStruct.comul 1 = 1 ⊗ₜ[R] DualNumber.eps + DualNumber.eps ⊗ₜ[R] 1

Splitting a circle labelled 1 gives 1 ⊗ ε + ε ⊗ 1.

@[simp]

theorem TauCeti.Khovanov.comul_eps (R : Type u_1) [CommSemiring R] : CoalgebraStruct.comul DualNumber.eps = DualNumber.eps ⊗ₜ[R] DualNumber.eps

Splitting a circle labelled ε gives ε ⊗ ε.

theorem TauCeti.Khovanov.isCocomm (R : Type u_1) [CommSemiring R] : Coalgebra.IsCocomm R (DualNumber R)

The Khovanov comultiplication is cocommutative.

theorem TauCeti.Khovanov.isFrobenius (R : Type u_1) [CommSemiring R] : Coalgebra.IsFrobenius R (DualNumber R)

The dual numbers with the Khovanov comultiplication satisfy the Frobenius equation.

theorem TauCeti.Khovanov.mul_compr₂_counit (R : Type u_1) [CommSemiring R] : (LinearMap.mul R (DualNumber R)).compr₂ CoalgebraStruct.counit = dualNumberTracePairing R

The Frobenius form (a, b) ↦ counit (a * b) of the Khovanov coalgebra is the perfect trace pairing of the dual numbers.

theorem TauCeti.Khovanov.counit_basis_mul_basis_rev (R : Type u_1) [CommSemiring R] (i j : Fin 2) : CoalgebraStruct.counit ((dualNumberBasis R) i * (dualNumberBasis R) j.rev) = if i = j then 1 else 0

The basis ε, 1 is dual to the basis 1, ε of R[ε] for the Frobenius form.

theorem DualNumber.khovanov_counit_eps_mul_smul_one_add_counit_smul_eps {R : Type u_1} [CommSemiring R] (a : DualNumber R) : CoalgebraStruct.counit (eps * a) • 1 + CoalgebraStruct.counit a • eps = a

Expansion of a dual number in the basis 1, ε with coefficients computed by the Frobenius form against the dual basis ε, 1.

noncomputable def TauCeti.Khovanov.baseChangeCoalgEquiv (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] : TensorProduct R S (DualNumber R) ≃ₗc[S] DualNumber S

Base change of the Khovanov coalgebra: S ⊗[R] R[ε] ≃ S[ε] as S-coalgebras, where S ⊗[R] R[ε] carries the base change of the Khovanov coalgebra over R. Its underlying map is the algebra isomorphism TauCeti.dualNumberAlgebraTensorAlgEquiv.

@[simp]

theorem TauCeti.Khovanov.coe_baseChangeCoalgEquiv (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] : ⇑(baseChangeCoalgEquiv R S) = ⇑(dualNumberAlgebraTensorAlgEquiv R S)

The underlying map of baseChangeCoalgEquiv is the algebra isomorphism TauCeti.dualNumberAlgebraTensorAlgEquiv.