The Euler characteristic of a cube of modules

The signed totalization of a finite commutative cube in any preadditive category with finite biproducts is strictly supported in the degrees 0, …, #ι; this file records that support as instances of CochainComplex.IsStrictlyGE and CochainComplex.IsStrictlyLE, which is how the Euler-characteristic API bounds its sums.

Let F : Finset ι ⥤ ModuleCat R be a finite commutative cube of modules. The term of degree r of its signed totalization F.cubeComplex is the product of the vertices F(S) of height #S = r (CategoryTheory.Functor.cubeComplexXLinearEquiv). When the vertices are finite free, so are the terms, and the Euler characteristic of the cube complex is the signed sum of the ranks of the vertices, each vertex F(S) counted with the sign (-1) ^ #S. Over a Noetherian ring with the rank-nullity property, such as ℤ or a field, Euler–Poincaré identifies this signed sum with the Euler characteristic of the cohomology of the cube complex.

This computes the quantum components of the graded Euler characteristic of Khovanov homology from the cube of resolutions: there the vertices are the homogeneous pieces of the circle tensors, which are finite free.

Main definitions

• CategoryTheory.Functor.cubeComplexXLinearEquiv: the term of degree r of the cube complex is the product of the vertices of height r.

Main results

• CategoryTheory.Functor.finrank_cubeComplex_X: for finite free vertices, the rank of the term of degree r is the sum of the ranks of the vertices of height r.
• CategoryTheory.Functor.eulerChar_cubeComplex: the Euler characteristic of the cube complex is ∑ S, (-1) ^ #S rank F(S).
• CategoryTheory.Functor.homologyEulerChar_cubeComplex: Euler–Poincaré for cubes, the Euler characteristic of the cohomology of the cube complex is ∑ S, (-1) ^ #S rank F(S).

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.

instance CategoryTheory.Functor.instIsStrictlyGECubeComplexOfNatInt {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasFiniteBiproducts C] {ι : Type w} [Fintype ι] [LinearOrder ι] (F : Functor (Finset ι) C) : F.cubeComplex.IsStrictlyGE 0

The cube complex is strictly supported in nonnegative degrees.

instance CategoryTheory.Functor.instIsStrictlyLECubeComplexCastIntCard {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasFiniteBiproducts C] {ι : Type w} [Fintype ι] [LinearOrder ι] (F : Functor (Finset ι) C) : F.cubeComplex.IsStrictlyLE ↑(Fintype.card ι)

The cube complex is strictly supported in the degrees at most the cardinality of the index type.

noncomputable def CategoryTheory.Functor.cubeComplexXLinearEquiv {ι : Type w} [Fintype ι] [LinearOrder ι] {R : Type u} [Ring R] (F : Functor (Finset ι) (ModuleCat R)) (r : ℤ) : ↑(F.cubeComplex.X r) ≃ₗ[R] (S : { S : Finset ι // ↑S.card = r }) → ↑(F.obj ↑S)

The term of degree r of the cube complex of a cube of modules is the product of the vertices of height r: an element is determined by its projections to these vertices, and a family of elements of the vertices is the sum of their inclusions.

@[simp]

theorem CategoryTheory.Functor.cubeComplexXLinearEquiv_apply {ι : Type w} [Fintype ι] [LinearOrder ι] {R : Type u} [Ring R] (F : Functor (Finset ι) (ModuleCat R)) {r : ℤ} (x : ↑(F.cubeComplex.X r)) (S : { S : Finset ι // ↑S.card = r }) : (F.cubeComplexXLinearEquiv r) x S = (ModuleCat.Hom.hom (F.cubeComplexπ S)) x

The coordinate of an element of a term of the cube complex at a vertex is its projection to that vertex.

@[simp]

theorem CategoryTheory.Functor.cubeComplexXLinearEquiv_symm_apply {ι : Type w} [Fintype ι] [LinearOrder ι] {R : Type u} [Ring R] (F : Functor (Finset ι) (ModuleCat R)) {r : ℤ} (f : (S : { S : Finset ι // ↑S.card = r }) → ↑(F.obj ↑S)) : (F.cubeComplexXLinearEquiv r).symm f = ∑ S : { S : Finset ι // ↑S.card = r }, (ModuleCat.Hom.hom (F.cubeComplexι S)) (f S)

A family of elements of the vertices of height r corresponds to the sum of their inclusions into the term of degree r of the cube complex.

instance CategoryTheory.Functor.instFiniteCarrierXIntModuleCatCubeComplexOfObjFinset {ι : Type w} [Fintype ι] [LinearOrder ι] {R : Type u} [Ring R] (F : Functor (Finset ι) (ModuleCat R)) [∀ (S : Finset ι), Module.Finite R ↑(F.obj S)] (r : ℤ) : Module.Finite R ↑(F.cubeComplex.X r)

The terms of the cube complex of a cube of finitely generated modules are finitely generated.

instance CategoryTheory.Functor.instFreeCarrierXIntModuleCatCubeComplexOfObjFinset {ι : Type w} [Fintype ι] [LinearOrder ι] {R : Type u} [Ring R] (F : Functor (Finset ι) (ModuleCat R)) [∀ (S : Finset ι), Module.Free R ↑(F.obj S)] (r : ℤ) : Module.Free R ↑(F.cubeComplex.X r)

The terms of the cube complex of a cube of free modules are free.

theorem CategoryTheory.Functor.finrank_cubeComplex_X {ι : Type w} [Fintype ι] [LinearOrder ι] {R : Type u} [Ring R] (F : Functor (Finset ι) (ModuleCat R)) [∀ (S : Finset ι), Module.Free R ↑(F.obj S)] [∀ (S : Finset ι), Module.Finite R ↑(F.obj S)] [StrongRankCondition R] (r : ℤ) : Module.finrank R ↑(F.cubeComplex.X r) = ∑ S : Finset ι with ↑S.card = r, Module.finrank R ↑(F.obj S)

For a cube of finite free modules, the rank of the term of degree r of the cube complex is the sum of the ranks of the vertices of height r.

theorem CategoryTheory.Functor.eulerChar_cubeComplex {ι : Type w} [Fintype ι] [LinearOrder ι] {R : Type u} [Ring R] (F : Functor (Finset ι) (ModuleCat R)) [∀ (S : Finset ι), Module.Free R ↑(F.obj S)] [∀ (S : Finset ι), Module.Finite R ↑(F.obj S)] [StrongRankCondition R] : HomologicalComplex.eulerChar F.cubeComplex = ∑ S : Finset ι, ↑(↑S.card).negOnePow * ↑(Module.finrank R ↑(F.obj S))

The Euler characteristic of a cube complex. For a cube of finite free modules, the Euler characteristic of the cube complex is the sum of the ranks of the vertices F(S), each with the sign (-1) ^ #S.

theorem CategoryTheory.Functor.homologyEulerChar_cubeComplex {ι : Type w} [Fintype ι] [LinearOrder ι] {R : Type u} [Ring R] (F : Functor (Finset ι) (ModuleCat R)) [∀ (S : Finset ι), Module.Free R ↑(F.obj S)] [∀ (S : Finset ι), Module.Finite R ↑(F.obj S)] [IsNoetherianRing R] [HasRankNullity.{v, u} R] : HomologicalComplex.homologyEulerChar F.cubeComplex = ∑ S : Finset ι, ↑(↑S.card).negOnePow * ↑(Module.finrank R ↑(F.obj S))

Euler–Poincaré for cubes. Over a Noetherian ring with the rank-nullity property, such as ℤ or a field, the Euler characteristic of the cohomology of the cube complex of a cube of finite free modules is the sum of the ranks of the vertices F(S), each with the sign (-1) ^ #S. Over ℤ the rank of a cohomology group is the rank of its free part, so torsion does not contribute.