Split maps on circle tensors

The Frobenius pairing on a circle pairs 1 with X and X with 1. On a finite set of circles it therefore pairs a labelling with its pointwise complement. We construct this perfect pairing using Module.Basis.equiv and Module.Basis.dualBasis, and define the split map along a map of circle sets as the adjoint of PiTensorProduct.fiberwiseMul. The pairing is symmetric, and since complementary labellings have opposite quantum degrees it restricts to a perfect pairing between the quantum pieces of degrees p and -p (TauCeti.Khovanov.circlePieceDuality).

This construction retains all unaffected circles and makes no choice of circle order. Its coefficient formula is the transpose of the merge formula with both labellings complemented. Composition is contravariant: successive splittings correspond to composition of the maps collapsing the output circles. Empty fibres give deaths, dual to the births of the merge map.

The pairing is the Frobenius form of the algebra ⨂ R[ε]: it reads the X ⊗ ⋯ ⊗ X coordinate of the product. Consequently the split map along f satisfies the projection formula Δ_f (m_f x * z) = x * Δ_f z, the Frobenius identity Δ(a b) = (a ⊗ 1) Δ(b) for fibres. This reduces composites of merges and splits to multiplication by merged splits of the unit; in particular, merging and splitting around a commuting square of circle correspondences agree when those splits of the unit agree. It also shows that splitting carries X on a circle to X on any one of its output circles.

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), §2.

noncomputable def TauCeti.Khovanov.circleDuality (R : Type u_1) [CommSemiring R] (ι : Type u_2) [Fintype ι] : CircleTensor R ι ≃ₗ[R] Module.Dual R (CircleTensor R ι)

The perfect Frobenius pairing of a finite circle tensor: complementary labellings are paired with coefficient one and all other pairs with coefficient zero.

@[simp]

theorem TauCeti.Khovanov.circleDuality_apply_circleBasis {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] (x : CircleTensor R ι) (l : ι → Bool) : ((circleDuality R ι) x) ((circleBasis R ι) l) = ((circleBasis R ι).repr x) fun (i : ι) => !l i

Pairing a tensor with a basis labelling reads its complementary coordinate.

theorem TauCeti.Khovanov.circleDuality_circleBasis {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] (l k : ι → Bool) : ((circleDuality R ι) ((circleBasis R ι) l)) ((circleBasis R ι) k) = ∏ i : ι, CoalgebraStruct.counit ((labelBasis R) (l i) * (labelBasis R) (k i))

On the labelling basis, the circle pairing is the tensor product of the original Frobenius forms (a, b) ↦ counit (a * b).

theorem TauCeti.Khovanov.circleDuality_apply_eq_repr_mul {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] (x y : CircleTensor R ι) : ((circleDuality R ι) x) y = ((circleBasis R ι).repr (x * y)) fun (x : ι) => true

The circle pairing is the Frobenius form of the algebra ⨂ R[ε]: it pairs x and y by reading the coordinate of x * y along the labelling with X on every circle. This is the tensor product of the original counits.

theorem TauCeti.Khovanov.circleDuality_comm {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] (x y : CircleTensor R ι) : ((circleDuality R ι) x) y = ((circleDuality R ι) y) x

The circle pairing is symmetric, since it is the Frobenius form of a commutative algebra.

noncomputable def TauCeti.Khovanov.fiberwiseSplit {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} [Fintype σ] [Fintype τ] [DecidableEq τ] (f : σ → τ) : CircleTensor R τ →ₗ[R] CircleTensor R σ

The split map along f, adjoint to multiplication along its fibres. It maps the tensor on τ to the tensor on σ; a two-element fibre splits that circle.

@[simp]

theorem TauCeti.Khovanov.circleDuality_fiberwiseSplit {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} [Fintype σ] [Fintype τ] [DecidableEq τ] (f : σ → τ) (x : CircleTensor R τ) (y : CircleTensor R σ) : ((circleDuality R σ) ((fiberwiseSplit f) x)) y = ((circleDuality R τ) x) ((PiTensorProduct.fiberwiseMul f) y)

The split map is characterized by adjunction for the Frobenius pairing.

theorem TauCeti.Khovanov.circleBasis_repr_fiberwiseSplit_eq_circleDuality {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} [Fintype σ] [Fintype τ] [DecidableEq τ] (f : σ → τ) (x : CircleTensor R τ) (l : σ → Bool) : ((circleBasis R σ).repr ((fiberwiseSplit f) x)) l = ((circleDuality R τ) x) ((PiTensorProduct.fiberwiseMul f) ((circleBasis R σ) fun (i : σ) => !l i))

The l-coordinate of the split of x is the pairing of x with the merge of the basis tensor labelled by the pointwise complement of l.

theorem TauCeti.Khovanov.circleBasis_repr_fiberwiseSplit {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} [Fintype σ] [Fintype τ] [DecidableEq τ] (f : σ → τ) (x : CircleTensor R τ) (l : σ → Bool) : ((circleBasis R σ).repr ((fiberwiseSplit f) x)) l = if ∀ (j : τ), {i : σ | f i = j ∧ (!l i) = true}.card ≤ 1 then ((circleBasis R τ).repr x) fun (j : τ) => !decide (∃ (i : σ), f i = j ∧ (!l i) = true) else 0

The coefficient formula for arbitrary splittings and deaths. At most one output in each fibre may carry 1; a fibre carrying only X requires an input X, and a fibre carrying one 1 requires an input 1. An empty fibre also requires an input X.

@[simp]

theorem TauCeti.Khovanov.fiberwiseSplit_id {R : Type u_1} [CommSemiring R] {σ : Type u_3} [Fintype σ] [DecidableEq σ] : fiberwiseSplit id = LinearMap.id

The identity correspondence gives the identity split map.

theorem TauCeti.Khovanov.fiberwiseSplit_comp {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} {υ : Type u_5} [Fintype σ] [Fintype τ] [DecidableEq τ] [Fintype υ] [DecidableEq υ] (g : τ → υ) (f : σ → τ) : fiberwiseSplit f ∘ₗ fiberwiseSplit g = fiberwiseSplit (g ∘ f)

Splitting successively is splitting along the composite circle correspondence.

theorem TauCeti.Khovanov.fiberwiseSplit_equiv {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} [Fintype σ] [Fintype τ] [DecidableEq τ] (e : σ ≃ τ) : fiberwiseSplit ⇑e = ↑(PiTensorProduct.reindex R (fun (x : τ) => DualNumber R) e.symm)

Along a bijection the split map is inverse reindexing, so relabelling circles introduces neither a scalar nor a sign.

theorem TauCeti.Khovanov.reindex_fiberwiseSplit {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} [Fintype σ] [Fintype τ] [DecidableEq τ] {σ' : Type u_6} {τ' : Type u_7} [Fintype σ'] [Fintype τ'] [DecidableEq τ'] (eσ : σ ≃ σ') (eτ : τ ≃ τ') {f : σ → τ} {f' : σ' → τ'} (h : ⇑eτ ∘ f = f' ∘ ⇑eσ) (x : CircleTensor R τ) : (PiTensorProduct.reindex R (fun (x : σ) => DualNumber R) eσ) ((fiberwiseSplit f) x) = (fiberwiseSplit f') ((PiTensorProduct.reindex R (fun (x : τ) => DualNumber R) eτ) x)

The split map is natural in the index map: reindexing along bijections of the source and target carries the split along f to the split along f' when the square eτ ∘ f = f' ∘ eσ commutes.

theorem TauCeti.Khovanov.fiberwiseSplit_fiberwiseMul_mul {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} [Fintype σ] [Fintype τ] [DecidableEq τ] (f : σ → τ) (x : CircleTensor R σ) (z : CircleTensor R τ) : (fiberwiseSplit f) ((PiTensorProduct.fiberwiseMul f) x * z) = x * (fiberwiseSplit f) z

The projection formula. The split map along f : σ → τ is linear over the algebra of the circles σ, which acts on the tensor over τ through multiplication along f. For a single splitting this is the Frobenius identity Δ(a b) = (a ⊗ 1) Δ(b).

theorem TauCeti.Khovanov.fiberwiseSplit_circleX {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} [Fintype σ] [Fintype τ] [DecidableEq τ] [DecidableEq σ] (f : σ → τ) (i : σ) (z : CircleTensor R τ) : (fiberwiseSplit f) ((circleX R (f i)) z) = (circleX R i) ((fiberwiseSplit f) z)

Splitting along f carries X on the circle f i to X on the circle i. By the projection formula, X on a split circle may be applied on either output circle.

theorem TauCeti.Khovanov.fiberwiseSplit_eq_fiberwiseMul_surjInv_mul {R : Type u_1} [CommSemiring R] {σ : Type u_3} [Fintype σ] {ρ : Type u_6} [Fintype ρ] [DecidableEq σ] [DecidableEq ρ] {f : ρ → σ} (hf : Function.Surjective f) (x : CircleTensor R σ) : (fiberwiseSplit f) x = (PiTensorProduct.fiberwiseMul (Function.surjInv hf)) x * (fiberwiseSplit f) 1

Splitting along a surjection is multiplication by the split of 1. By the projection formula, splitting x along a surjection f multiplies the split of 1 by x, transported to the split circles by merging along a section of f.

theorem TauCeti.Khovanov.fiberwiseMul_fiberwiseSplit {R : Type u_1} [CommSemiring R] {σ : Type u_3} {υ : Type u_5} [Fintype σ] {ρ : Type u_6} [Fintype ρ] [DecidableEq σ] [DecidableEq υ] {f : ρ → σ} (hf : Function.Surjective f) {g : ρ → υ} {h : σ → υ} (hgh : h ∘ f = g) (x : CircleTensor R σ) : (PiTensorProduct.fiberwiseMul g) ((fiberwiseSplit f) x) = (PiTensorProduct.fiberwiseMul h) x * (PiTensorProduct.fiberwiseMul g) ((fiberwiseSplit f) 1)

Splitting and then merging along a factorization. Split along a surjection f and then merge along g = h ∘ f, which merges every circle split off by f back together. The result is multiplication by the merge of the split of 1, after merging along h.

theorem TauCeti.Khovanov.fiberwiseSplit_fiberwiseMul_of_comp_eq {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} {υ : Type u_5} [Fintype σ] [Fintype τ] [DecidableEq τ] {ρ : Type u_6} [Fintype ρ] [DecidableEq σ] [Fintype υ] [DecidableEq υ] {f' : ρ → σ} (hf' : Function.Surjective f') {g' : ρ → υ} {f : σ → τ} {g : υ → τ} (hcomm : f ∘ f' = g ∘ g') (hone : (PiTensorProduct.fiberwiseMul g') ((fiberwiseSplit f') 1) = (fiberwiseSplit g) 1) (x : CircleTensor R σ) : (fiberwiseSplit g) ((PiTensorProduct.fiberwiseMul f) x) = (PiTensorProduct.fiberwiseMul g') ((fiberwiseSplit f') x)

The Frobenius relation for a commuting square of circle correspondences. Let f ∘ f' = g ∘ g', with f' surjective, and suppose that splitting 1 along f' and merging along g' gives the split of 1 along g. Then merging along f and splitting along g is splitting along f' and merging along g'.

theorem TauCeti.Khovanov.fiberwiseSplit_comp_fiberwiseMul_equiv_comp {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} {υ : Type u_5} [Fintype σ] [Fintype τ] [DecidableEq τ] [Fintype υ] {τ' : Type u_6} [Fintype τ'] [DecidableEq τ'] (e : τ ≃ τ') (f : σ → τ) (g : υ → τ) : fiberwiseSplit (⇑e ∘ g) ∘ₗ (PiTensorProduct.fiberwiseMul (⇑e ∘ f)).toLinearMap = fiberwiseSplit g ∘ₗ (PiTensorProduct.fiberwiseMul f).toLinearMap

Merging and then splitting through a set of circles depends on that set only up to a bijection compatible with both correspondences.

theorem TauCeti.Khovanov.fiberwiseSplit_const_circleBasis {R : Type u_1} [CommSemiring R] (b : Bool) : (fiberwiseSplit fun (x : Bool) => ()) ((circleBasis R Unit) fun (x : Unit) => b) = if b = true then (circleBasis R Bool) fun (x : Bool) => true else (circleBasis R Bool) id + (circleBasis R Bool) not

Splitting 1 into two circles gives 1 ⊗ X + X ⊗ 1; splitting X gives X ⊗ X. The two output circles are indexed by Bool, and the input by Unit.

theorem TauCeti.Khovanov.fiberwiseSplit_circleBasis_of_eq_iff {R : Type u_1} [CommSemiring R] {σ : Type u_3} {τ : Type u_4} [Fintype σ] [Fintype τ] [DecidableEq τ] [DecidableEq σ] {f : σ → τ} (hf : Function.Surjective f) {p q : σ} (hpq : p ≠ q) (hfeq : ∀ (a b : σ), f a = f b ↔ a = b ∨ (a = p ∨ a = q) ∧ (b = p ∨ b = q)) (l : τ → Bool) : (fiberwiseSplit f) ((circleBasis R τ) l) = if l (f p) = true then (circleBasis R σ) fun (i : σ) => l (f i) else (circleBasis R σ) (Function.update (fun (i : σ) => l (f i)) p true) + (circleBasis R σ) (Function.update (fun (i : σ) => l (f i)) q true)

Splitting along a surjection whose only non-singleton fibre is {p, q} obeys Δ X = X ⊗ X and Δ 1 = X ⊗ 1 + 1 ⊗ X on the circles p and q; every other circle retains the label of its image.

theorem TauCeti.Khovanov.isHomogeneous_fiberwiseSplit (R : Type u_1) [CommRing R] {σ : Type u_2} {τ : Type u_3} [Fintype σ] [Fintype τ] [DecidableEq τ] (f : σ → τ) : LinearMap.IsHomogeneous (fiberwiseSplit f) ((circleQuantumGrading R τ).piece ℤ) ((circleQuantumGrading R σ).piece ℤ) (↑(Fintype.card τ) - ↑(Fintype.card σ))

Splitting along f : σ → τ has quantum degree |τ| - |σ|. Thus an elementary split has degree -1, and deleting a circle by the counit has degree +1.

noncomputable def TauCeti.Khovanov.circlePieceDuality (R : Type u_1) [CommRing R] (ι : Type u_4) [Fintype ι] (p : ℤ) : ↥((circleQuantumGrading R ι).piece ℤ p) ≃ₗ[R] Module.Dual R ↥((circleQuantumGrading R ι).piece ℤ (-p))

The Frobenius pairing restricts to a perfect pairing between the quantum pieces of degrees p and -p of a circle tensor: complementary labellings have opposite degrees, so the basis of the degree-p piece is carried to the dual basis of the degree--p piece (TauCeti.Khovanov.circlePieceDuality_apply).

@[simp]

theorem TauCeti.Khovanov.circlePieceDuality_apply (R : Type u_1) [CommRing R] {ι : Type u_4} [Fintype ι] {p : ℤ} (x : ↥((circleQuantumGrading R ι).piece ℤ p)) (y : ↥((circleQuantumGrading R ι).piece ℤ (-p))) : ((circlePieceDuality R ι p) x) y = ((circleDuality R ι) ↑x) ↑y

The pairing of the quantum pieces of degrees p and -p is the Frobenius pairing of the whole circle tensor.