The signed totalization of a finite commutative cube #
Let ι be a finite linearly ordered type. A commutative cube indexed by ι in a category C is
a functor F : Finset ι ⥤ C on the subsets of ι, ordered by inclusion: it assigns an object
F(S) to every vertex S ⊆ ι and an edge map F(S) ⟶ F(S ∪ {a}) to every a ∉ S, and every
square face of edge maps commutes. When C is preadditive with finite biproducts, the signed
height totalization of F is the cochain complex whose term in degree r is the biproduct of the
F(S) over the vertices of height #S = r, and whose differential is the sum of the edge maps
leaving a vertex, the edge S ⟶ S ∪ {a} carrying the sign (-1) to the number of elements of
S below a. These signs turn the commutativity of each square face into anticommutativity, so
the differential squares to zero.
This is the construction of the Khovanov complex from the cube of resolutions of a link diagram,
where ι is the set of crossings with a chosen order and S is the set of crossings given the
second resolution; the cochain complex is indexed by ℤ so that it can be shifted to the
normalized grading. Its terms vanish outside the degrees 0, …, #ι, and in degree 0 it is the
initial vertex F(∅).
The sign rule is that of the ordered Čech complex CategoryTheory.Functor.orderedCechComplex:
after reversing all arrows, the vertices of positive height form the ordered Čech complex of the
opposite functor, shifted down by one degree. Here the vertex F(∅) is part of the complex, the
degree is the height #S itself, and the terms are finite biproducts.
Main definitions #
CategoryTheory.Functor.cubeComplex F: the signed totalization of the cubeF; its terms are biproducts with summand inclusionsFunctor.cubeComplexιand projectionsFunctor.cubeComplexπ, and its differential is characterised on summands byFunctor.ι_cubeComplex_dand, into a vertex, byFunctor.cubeComplex_d_π.CategoryTheory.NatTrans.cubeComplexMap α: the cochain map induced by a map of cubes.CategoryTheory.cubeComplexFunctor C ι: the totalization as an additive functor of the cube.
Main results #
Functor.isZero_cubeComplex_X_of_neg,Functor.isZero_cubeComplex_X_of_card_lt: the terms vanish outside the degrees0, …, #ι.Functor.cubeComplex_total: each term is the direct sum of its vertices.Functor.cubeComplexXZeroIso: the degree0term is the initial vertexF(∅).
References #
- M. Khovanov, A categorification of the Jones polynomial, Duke Math. J. 101 (2000), §3.
- D. Bar-Natan, On Khovanov's categorification of the Jones polynomial, Algebr. Geom. Topol. 2 (2002), §2.
The signed totalization of the commutative cube F: in degree r it is the biproduct of
the vertices F(S) of height #S = r, with differential the sum of the edge maps
F(S) ⟶ F(S ∪ {a}), signed by (-1) to the number of elements of S below a. It is
characterised by the summand inclusions Functor.cubeComplexι and projections
Functor.cubeComplexπ, and by Functor.ι_cubeComplex_d.
Instances For
The degree r term is the biproduct of the vertices of height r.
The inclusion of the vertex F(S) into the degree r term of the cube complex, for a vertex
of height #S = r.
Instances For
The vertex inclusion agrees with the biproduct inclusion under the term identification.
The vertex inclusion agrees with the biproduct inclusion under the term identification.
The projection of the degree r term of the cube complex onto the vertex F(S), for a vertex
of height #S = r.
Instances For
The biproduct projection agrees with the vertex projection under the term identification.
The biproduct projection agrees with the vertex projection under the term identification.
Transporting a cube term to an equal height preserves each vertex inclusion.
Transporting a cube term to an equal height preserves each vertex inclusion.
The inclusion of a vertex followed by the projection onto a vertex of the same height is the identity when the vertices agree, and zero otherwise.
The inclusion of a vertex followed by the projection onto a vertex of the same height is the identity when the vertices agree, and zero otherwise.
The inclusion of a vertex followed by the projection onto it is the identity.
The inclusion of a vertex followed by the projection onto it is the identity.
The inclusion of a vertex followed by the projection onto another vertex vanishes.
The inclusion of a vertex followed by the projection onto another vertex vanishes.
The inclusion of a vertex is compatible with the identification of equal vertices.
The inclusion of a vertex is compatible with the identification of equal vertices.
The morphism out of the degree r term of the cube complex given on each vertex.
Instances For
The morphism Functor.cubeComplexDesc f restricts to f S on the vertex F(S).
The morphism Functor.cubeComplexDesc f restricts to f S on the vertex F(S).
The morphism into the degree r term of the cube complex given on each vertex.
Instances For
The morphism Functor.cubeComplexLift f projects to f S on the vertex F(S).
The morphism Functor.cubeComplexLift f projects to f S on the vertex F(S).
The projections onto the vertices of height r, followed by their inclusions, sum to the
identity of the degree r term of the cube complex.
Morphisms out of a term of the cube complex agree when they agree on every vertex.
Morphisms into a term of the cube complex agree when their projections to every vertex agree.
A term of the signed totalization vanishes exactly when all vertices of that height vanish.
The cube differential on the vertex F(S) of height r is the sum, over the indices a ∉ S,
of the edge map F(S) ⟶ F(S ∪ {a}) with sign (-1) to the number of elements of S below
a.
The cube differential on the vertex F(S) of height r is the sum, over the indices a ∉ S,
of the edge map F(S) ⟶ F(S ∪ {a}) with sign (-1) to the number of elements of S below
a.
The cube differential into the vertex F(T) of height r + 1 is the sum, over the indices
a ∈ T, of the projection onto the vertex F(T \ {a}) followed by the edge map
F(T \ {a}) ⟶ F(T), with sign (-1) to the number of elements of T \ {a} below a.
The cube differential into the vertex F(T) of height r + 1 is the sum, over the indices
a ∈ T, of the projection onto the vertex F(T \ {a}) followed by the edge map
F(T \ {a}) ⟶ F(T), with sign (-1) to the number of elements of T \ {a} below a.
The cube complex vanishes in negative degrees.
The cube complex vanishes in the degrees above the cardinality of the index type.
The degree 0 term of the cube complex is the initial vertex F(∅), the only vertex of
height 0.
Instances For
The identification of the degree 0 term with F(∅) is the projection onto that vertex.
The identification of F(∅) with the degree 0 term is the inclusion of that vertex.
The cochain map of cube complexes induced by a map of cubes, acting vertex by vertex
(NatTrans.ι_cubeComplexMap_f).
Instances For
The cochain map induced by α restricts to α on the vertex F(S).
The cochain map induced by α restricts to α on the vertex F(S).
The cochain map induced by α followed by the projection onto the vertex G(S) is the
projection onto F(S) followed by α.
The cochain map induced by α followed by the projection onto the vertex G(S) is the
projection onto F(S) followed by α.
The identification of the degree 0 term with the initial vertex is natural in the cube.
The identification of the degree 0 term with the initial vertex is natural in the cube.
The identification of the initial vertex with the degree 0 term is natural in the cube.
The identification of the initial vertex with the degree 0 term is natural in the cube.
The cube complex Functor.cubeComplex as a functor of the cube.
Instances For
The cube complex is additive in the cube.