Circle tensors and merge maps

A resolution of a link diagram is a finite set ι of circles, and Khovanov's chain group of that resolution is the tensor product ⨂_{i : ι} V of one copy of the rank-two Frobenius algebra V = R[ε] per circle (with X = ε). This file constructs that circle tensor TauCeti.Khovanov.CircleTensor R ι, its basis indexed by the labellings ι → Bool of the circles by 1 (false) and X (true), and its quantum grading, in which a labelling has degree #{1-labels} - #{X-labels}.

For a state s of a PD-code D, the labellings D.ResolvedCircle s → Bool are exactly the enhanced states over s (TauCeti.PDCode.EnhancedState), and the quantum degree of an enhanced state is the quantum shift of its state plus the degree of its labelling (TauCeti.OrientedPDCode.enhancedQuantumDegree_def). So the basis TauCeti.Khovanov.circleBasis identifies the circle tensor of a resolution with the free module on the enhanced states over it, its Finsupp model.

A map f : σ → τ of circle sets acts by PiTensorProduct.fiberwiseMul, which multiplies the labels on each fibre of f and puts 1 on the circles of τ outside the range of f. When f merges two circles and is a bijection on the others, this is the merge map of the Khovanov differential: multiplication m on the two merged factors and the identity on the rest. Empty fibres give the unit η, as for a circle born from nothing. The map depends only on f, so it is independent of any ordering of the circles or parenthesization of the tensor product, and it is functorial in f (PiTensorProduct.fiberwiseMul_comp).

Multiplication by X in the factor of one circle, TauCeti.Khovanov.circleX, has square zero and quantum degree -2, and merging carries it to X on the image circle. This is the action of a marked circle used for reduced Khovanov homology.

Main definitions

• TauCeti.Khovanov.labelBasis: the basis 1, ε of R[ε] indexed by the labels false, true.
• TauCeti.Khovanov.CircleTensor: the tensor product of one copy of R[ε] per circle.
• TauCeti.Khovanov.circleBasis: its basis indexed by labellings.
• TauCeti.Khovanov.circleQuantumGrading: the quantum grading of the circle tensor.
• TauCeti.Khovanov.circlePieceBasis: the basis of its degree-p piece indexed by the labellings of degree p, so that every piece is finite free.
• TauCeti.Khovanov.circlePieceEquivOfUnique: a piece with a single labelling of its degree is identified with R.
• TauCeti.Khovanov.circleX: multiplication by X in the factor of one circle.

Main results

• TauCeti.Khovanov.tprod_mem_circleQuantumGrading_piece: a tensor of homogeneous elements of R[ε] is homogeneous of the total degree.
• TauCeti.Khovanov.circleQuantumGrading_piece_eq_bot_of_card_lt_abs: the circle tensor of k circles vanishes in the quantum degrees p with k < |p|.
• TauCeti.Khovanov.fiberwiseMul_circleBasis: the merge map along f sends a labelling to the labelling marking X on each circle whose fibre carries one X, and to 0 when some fibre carries two Xs.
• TauCeti.Khovanov.isHomogeneous_fiberwiseMul: the merge map along f : σ → τ has quantum degree |τ| - |σ|; in particular merging two circles into one has degree -1.
• TauCeti.Khovanov.circleX_circleX, TauCeti.Khovanov.isHomogeneous_circleX: the X action on a circle squares to zero and has quantum degree -2.
• TauCeti.Khovanov.isHomogeneous_reindex, TauCeti.Khovanov.map_reindex_circleQuantumGrading_piece: relabelling the circle factors preserves quantum degree, and carries each quantum piece onto the piece of the same degree.

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.

noncomputable def TauCeti.Khovanov.labelBasis (R : Type u) [CommSemiring R] : Module.Basis Bool R (DualNumber R)

The basis 1, ε of the dual numbers R[ε] indexed by the labels of a circle: false stands for the generator 1 and true for the generator X = ε. It is TauCeti.dualNumberBasis reindexed along finTwoEquiv.

@[simp]

theorem TauCeti.Khovanov.labelBasis_false (R : Type u) [CommSemiring R] : (labelBasis R) false = 1

The label false is the generator 1.

@[simp]

theorem TauCeti.Khovanov.labelBasis_true (R : Type u) [CommSemiring R] : (labelBasis R) true = DualNumber.eps

The label true is the generator X = ε.

@[simp]

theorem TauCeti.Khovanov.labelBasis_repr_false {R : Type u} [CommSemiring R] (x : DualNumber R) : ((labelBasis R).repr x) false = TrivSqZeroExt.fst x

The coordinate of a dual number along the label false is its scalar part.

@[simp]

theorem TauCeti.Khovanov.labelBasis_repr_true {R : Type u} [CommSemiring R] (x : DualNumber R) : ((labelBasis R).repr x) true = TrivSqZeroExt.snd x

The coordinate of a dual number along the label true is its ε-part.

theorem TauCeti.Khovanov.prod_labelBasis {R : Type u} [CommSemiring R] {ι : Type u_1} (s : Finset ι) (l : ι → Bool) : ∏ i ∈ s, (labelBasis R) (l i) = DualNumber.eps ^ {i ∈ s | l i = true}.card

A product of labels is ε raised to the number of X-labels.

@[reducible, inline]

abbrev TauCeti.Khovanov.CircleTensor (R : Type u) [CommSemiring R] (ι : Type u_1) : Type (max u u_1)

The circle tensor of a finite set ι of circles: the tensor product of one copy of the Khovanov Frobenius algebra R[ε] for each circle. It is a commutative R-algebra.

noncomputable def TauCeti.Khovanov.circleBasis (R : Type u) [CommSemiring R] (ι : Type u_1) [Finite ι] : Module.Basis (ι → Bool) R (CircleTensor R ι)

The basis of the circle tensor indexed by the labellings ι → Bool of the circles by 1 (false) and X (true): the labelling l gives the pure tensor ⨂ₜ i, labelBasis R (l i).

@[simp]

theorem TauCeti.Khovanov.circleBasis_apply {R : Type u} [CommSemiring R] {ι : Type u_1} [Finite ι] (l : ι → Bool) : (circleBasis R ι) l = (PiTensorProduct.tprod R) fun (i : ι) => (labelBasis R) (l i)

The basis vector of a labelling is the pure tensor of the labels.

@[simp]

theorem TauCeti.Khovanov.circleBasis_repr_tprod {R : Type u} [CommSemiring R] {ι : Type u_1} [Fintype ι] (x : ι → DualNumber R) (l : ι → Bool) : ((circleBasis R ι).repr ((PiTensorProduct.tprod R) x)) l = ∏ i : ι, ((labelBasis R).repr (x i)) (l i)

The coordinate of a pure tensor along a labelling is the product of the coordinates of its factors along the labels.

@[simp]

theorem TauCeti.Khovanov.circleBasis_const_false {R : Type u} [CommSemiring R] {ι : Type u_1} [Finite ι] : ((circleBasis R ι) fun (x : ι) => false) = 1

The labelling with 1 on every circle is the unit of the circle tensor. It is a pre-simp lemma since circleBasis_apply would otherwise expand the basis vector first.

@[simp]

theorem TauCeti.Khovanov.circleBasis_update_const_false {R : Type u} [CommSemiring R] {ι : Type u_1} [Finite ι] [DecidableEq ι] (i : ι) : (circleBasis R ι) (Function.update (fun (x : ι) => false) i true) = (PiTensorProduct.singleAlgHom i) DualNumber.eps

The labelling with X on the circle i and 1 elsewhere is X placed in the factor i. It is a pre-simp lemma since circleBasis_apply would otherwise expand the basis vector first.

@[simp]

theorem TauCeti.Khovanov.reindex_circleBasis {R : Type u} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} [Finite σ] [Finite τ] (e : σ ≃ τ) (l : σ → Bool) : (PiTensorProduct.reindex R (fun (x : σ) => DualNumber R) e) ((circleBasis R σ) l) = (circleBasis R τ) (l ∘ ⇑e.symm)

Reindexing circle factors transports their labellings along the inverse bijection.

theorem TauCeti.Khovanov.fiberwiseMul_circleBasis_eq_tprod {R : Type u} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} [Fintype σ] [DecidableEq τ] [Finite τ] (f : σ → τ) (l : σ → Bool) : (PiTensorProduct.fiberwiseMul f) ((circleBasis R σ) l) = (PiTensorProduct.tprod R) fun (j : τ) => DualNumber.eps ^ {i : σ | f i = j ∧ l i = true}.card

The merge map along f sends the basis vector of a labelling l to the pure tensor carrying, on each circle j, the power of ε counting the X-labels of l on the fibre of j.

theorem TauCeti.Khovanov.fiberwiseMul_circleBasis {R : Type u} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} [Fintype σ] [DecidableEq τ] [Fintype τ] (f : σ → τ) (l : σ → Bool) : (PiTensorProduct.fiberwiseMul f) ((circleBasis R σ) l) = if ∀ (j : τ), {i : σ | f i = j ∧ l i = true}.card ≤ 1 then (circleBasis R τ) fun (j : τ) => decide (∃ (i : σ), f i = j ∧ l i = true) else 0

The merge map on the labelling basis. Along f, the basis vector of a labelling l goes to 0 if some fibre of f carries two X-labels. Otherwise it goes to the basis vector of the labelling that marks X exactly on the circles whose fibre carries an X-label.

noncomputable def TauCeti.Khovanov.circleX (R : Type u) [CommSemiring R] {ι : Type u_1} [DecidableEq ι] (i : ι) : CircleTensor R ι →ₗ[R] CircleTensor R ι

The action of X on the circle i: multiplication by X = ε placed in the factor i.

theorem TauCeti.Khovanov.circleX_apply {R : Type u} [CommSemiring R] {ι : Type u_1} [DecidableEq ι] (i : ι) (x : CircleTensor R ι) : (circleX R i) x = (PiTensorProduct.singleAlgHom i) DualNumber.eps * x

The X action on the circle i is multiplication by X in the factor i.

@[simp]

theorem TauCeti.Khovanov.circleX_circleBasis {R : Type u} [CommSemiring R] {ι : Type u_1} [DecidableEq ι] [Finite ι] (i : ι) (l : ι → Bool) : (circleX R i) ((circleBasis R ι) l) = if l i = true then 0 else (circleBasis R ι) (Function.update l i true)

On the labelling basis, X on the circle i relabels i from 1 to X, and kills the labellings already carrying X on i.

@[simp]

theorem TauCeti.Khovanov.circleX_circleX {R : Type u} [CommSemiring R] {ι : Type u_1} [DecidableEq ι] (i : ι) (x : CircleTensor R ι) : (circleX R i) ((circleX R i) x) = 0

The X action on a circle squares to zero, since X² = 0.

theorem TauCeti.Khovanov.fiberwiseMul_circleX {R : Type u} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} [DecidableEq σ] [DecidableEq τ] [Fintype σ] (f : σ → τ) (i : σ) (x : CircleTensor R σ) : (PiTensorProduct.fiberwiseMul f) ((circleX R i) x) = (circleX R (f i)) ((PiTensorProduct.fiberwiseMul f) x)

Merging along f carries X on the circle i to X on the circle f i.

theorem TauCeti.Khovanov.reindex_circleX {R : Type u} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} [DecidableEq σ] [DecidableEq τ] (e : σ ≃ τ) (i : σ) (x : CircleTensor R σ) : (PiTensorProduct.reindex R (fun (x : σ) => DualNumber R) e) ((circleX R i) x) = (circleX R (e i)) ((PiTensorProduct.reindex R (fun (x : σ) => DualNumber R) e) x)

Reindexing along e carries X on the circle i to X on the circle e i.

noncomputable def TauCeti.Khovanov.circleQuantumGrading (R : Type u) [CommRing R] (ι : Type u_1) [Fintype ι] : InternalGrading R (CircleTensor R ι) ℤ

The quantum grading of the circle tensor: the basis vector of a labelling l spans its degree TauCeti.Khovanov.labelingQuantumDegree ι l. It is the grading of the free module on the labellings, transported along TauCeti.Khovanov.circleBasis.

theorem TauCeti.Khovanov.mem_circleQuantumGrading_piece_iff {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {p : ℤ} {x : CircleTensor R ι} : x ∈ (circleQuantumGrading R ι).piece ℤ p ↔ ∀ (l : ι → Bool), ((circleBasis R ι).repr x) l ≠ 0 → labelingQuantumDegree ι l = p

An element of the circle tensor has quantum degree p exactly when its coordinates along the labellings of other degrees vanish.

theorem TauCeti.Khovanov.circleBasis_mem_circleQuantumGrading_piece {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] (l : ι → Bool) : (circleBasis R ι) l ∈ (circleQuantumGrading R ι).piece ℤ (labelingQuantumDegree ι l)

The basis vector of a labelling is homogeneous of the degree of the labelling.

noncomputable def TauCeti.Khovanov.circlePieceBasis (R : Type u) [CommRing R] (ι : Type u_1) [Fintype ι] (p : ℤ) : Module.Basis { l : ι → Bool // labelingQuantumDegree ι l = p } R ↥((circleQuantumGrading R ι).piece ℤ p)

The basis of the degree-p piece of the circle tensor formed by the basis vectors of the labellings of degree p.

@[simp]

theorem TauCeti.Khovanov.coe_circlePieceBasis {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {p : ℤ} (l : { l : ι → Bool // labelingQuantumDegree ι l = p }) : ↑((circlePieceBasis R ι p) l) = (circleBasis R ι) ↑l

The basis vector of a labelling of degree p in the degree-p piece is its basis vector in the circle tensor.

@[simp]

theorem TauCeti.Khovanov.circlePieceBasis_repr_apply {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {p : ℤ} (x : ↥((circleQuantumGrading R ι).piece ℤ p)) (l : { l : ι → Bool // labelingQuantumDegree ι l = p }) : ((circlePieceBasis R ι p).repr x) l = ((circleBasis R ι).repr ↑x) ↑l

The coordinates of a homogeneous element in circlePieceBasis are its coordinates in circleBasis.

theorem TauCeti.Khovanov.circleQuantumGrading_piece_eq_bot {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {p : ℤ} (h : ∀ (l : ι → Bool), labelingQuantumDegree ι l ≠ p) : (circleQuantumGrading R ι).piece ℤ p = ⊥

The degree-p piece of the circle tensor vanishes when no labelling has degree p.

theorem TauCeti.Khovanov.circleQuantumGrading_piece_eq_bot_iff {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] [Nontrivial R] (p : ℤ) : (circleQuantumGrading R ι).piece ℤ p = ⊥ ↔ ∀ (l : ι → Bool), labelingQuantumDegree ι l ≠ p

Over a nontrivial ring, a quantum piece vanishes exactly when no circle labelling has that degree.

theorem TauCeti.Khovanov.circleQuantumGrading_piece_eq_bot_of_card_lt_abs {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {p : ℤ} (hp : ↑(Fintype.card ι) < |p|) : (circleQuantumGrading R ι).piece ℤ p = ⊥

Finite quantum support: the circle tensor of k circles vanishes in the quantum degrees p with k < |p|.

instance TauCeti.Khovanov.instFreeSubtypeCircleTensorMemSubmodulePieceIntCircleQuantumGrading {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] (p : ℤ) : Module.Free R ↥((circleQuantumGrading R ι).piece ℤ p)

Each quantum-degree piece of the circle tensor is a free module.

instance TauCeti.Khovanov.instFiniteSubtypeCircleTensorMemSubmodulePieceIntCircleQuantumGrading {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] (p : ℤ) : Module.Finite R ↥((circleQuantumGrading R ι).piece ℤ p)

Each quantum-degree piece of the circle tensor is a finitely generated module.

noncomputable def TauCeti.Khovanov.circlePieceEquivOfUnique (R : Type u) [CommRing R] {ι : Type u_1} [Fintype ι] {p : ℤ} (l₀ : ι → Bool) (h : ∀ (l : ι → Bool), labelingQuantumDegree ι l = p ↔ l = l₀) : ↥((circleQuantumGrading R ι).piece ℤ p) ≃ₗ[R] R

When l₀ is the only labelling of degree p, the degree-p piece of the circle tensor is free of rank one: the coordinate along l₀ identifies it with R.

@[simp]

theorem TauCeti.Khovanov.circlePieceEquivOfUnique_apply {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {p : ℤ} {l₀ : ι → Bool} (h : ∀ (l : ι → Bool), labelingQuantumDegree ι l = p ↔ l = l₀) (x : ↥((circleQuantumGrading R ι).piece ℤ p)) : (circlePieceEquivOfUnique R l₀ h) x = ((circleBasis R ι).repr ↑x) l₀

The identification of a rank-one piece with R reads off the coordinate along the unique labelling of that degree.

@[simp]

theorem TauCeti.Khovanov.coe_circlePieceEquivOfUnique_symm_apply {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {p : ℤ} {l₀ : ι → Bool} (h : ∀ (l : ι → Bool), labelingQuantumDegree ι l = p ↔ l = l₀) (r : R) : ↑((circlePieceEquivOfUnique R l₀ h).symm r) = r • (circleBasis R ι) l₀

The inverse identification sends a scalar to that multiple of the basis vector of the unique labelling of that degree.

@[simp]

theorem TauCeti.Khovanov.tprod_labelBasis_mem_circleQuantumGrading_piece {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] (l : ι → Bool) : ((PiTensorProduct.tprod R) fun (i : ι) => (labelBasis R) (l i)) ∈ (circleQuantumGrading R ι).piece ℤ (labelingQuantumDegree ι l)

The pure tensor of the labels of a labelling is homogeneous of the degree of the labelling. This is the simp-normal form of TauCeti.Khovanov.circleBasis_mem_circleQuantumGrading_piece.

theorem TauCeti.Khovanov.tprod_mem_circleQuantumGrading_piece {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {d : ι → ℤ} {x : ι → DualNumber R} (hx : ∀ (i : ι), x i ∈ (quantumGrading R).piece ℤ (d i)) : (PiTensorProduct.tprod R) x ∈ (circleQuantumGrading R ι).piece ℤ (∑ i : ι, d i)

A tensor of homogeneous elements is homogeneous: if each factor x i of R[ε] has quantum degree d i, then ⨂ₜ x has quantum degree ∑ i, d i.

theorem TauCeti.Khovanov.isHomogeneous_fiberwiseMul {R : Type u} [CommRing R] {σ : Type u_2} {τ : Type u_3} [Fintype σ] [Fintype τ] [DecidableEq τ] (f : σ → τ) : LinearMap.IsHomogeneous (PiTensorProduct.fiberwiseMul f).toLinearMap ((circleQuantumGrading R σ).piece ℤ) ((circleQuantumGrading R τ).piece ℤ) (↑(Fintype.card τ) - ↑(Fintype.card σ))

The merge map along f : σ → τ has quantum degree |τ| - |σ|. Merging two circles into one has degree -1, and the birth of a circle (a point of τ outside the range of f) has degree +1.

theorem TauCeti.Khovanov.isHomogeneous_circleX {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) : LinearMap.IsHomogeneous (circleX R i) ((circleQuantumGrading R ι).piece ℤ) ((circleQuantumGrading R ι).piece ℤ) (-2)

The X action on a circle has quantum degree -2.

theorem TauCeti.Khovanov.exists_circleX_eq_of_mem_piece_of_circleX_eq_zero {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) {q : ℤ} {x : CircleTensor R ι} (hx : x ∈ (circleQuantumGrading R ι).piece ℤ q) (hX : (circleX R i) x = 0) : ∃ y ∈ (circleQuantumGrading R ι).piece ℤ (q + 2), (circleX R i) y = x

On a quantum piece, every tensor annihilated by X on a selected circle is X times a homogeneous tensor of degree two higher. This holds over every commutative ring, including the zero ring; it is the graded image/kernel identity behind marked-component reduction.

theorem TauCeti.Khovanov.isHomogeneous_reindex {R : Type u} [CommRing R] {σ : Type u_2} {τ : Type u_3} [Fintype σ] [Fintype τ] (e : σ ≃ τ) : LinearMap.IsHomogeneous (↑(PiTensorProduct.reindex R (fun (x : σ) => DualNumber R) e)) ((circleQuantumGrading R σ).piece ℤ) ((circleQuantumGrading R τ).piece ℤ) 0

Reindexing the circle factors preserves their total quantum degree.

theorem TauCeti.Khovanov.map_reindex_circleQuantumGrading_piece {R : Type u} [CommRing R] {σ : Type u_2} {τ : Type u_3} [Fintype σ] [Fintype τ] (e : σ ≃ τ) (p : ℤ) : Submodule.map (↑(PiTensorProduct.reindex R (fun (x : σ) => DualNumber R) e)) ((circleQuantumGrading R σ).piece ℤ p) = (circleQuantumGrading R τ).piece ℤ p

Reindexing the circle factors carries each quantum piece onto the piece of the same degree.