Khovanov homology of classical links
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
TheoremThe enhanced state sum of a nonempty diagram is (q + q⁻¹) times its Jones polynomial at t ^ (1/2) = -q#
The hypothesis 0 < componentCount says that the diagram is nonempty; it
excludes the empty diagram, whose enhanced state sum is 1.
TauCeti.OrientedPDCode.enhancedStateSum_eq_mul_eval₂_jonesPolynomial {n : ℕ}
(D : TauCeti.OrientedPDCode n) (h : 0 < D.componentCount) :
D.enhancedStateSum =
(LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) *
(LaurentPolynomial.eval₂ (Int.castRingHom (LaurentPolynomial ℤ))
(-LaurentPolynomial.genericUnit ℤ))
D.jonesPolynomial
Lean
Formalized in Tau Ceti as TauCeti.OrientedPDCode.enhancedStateSum_eq_mul_eval₂_jonesPolynomial.
Sources
Used by 1
TheoremTwo states differing exactly at a crossing do not both have two circles through it#
So along an edge of the cube of resolutions two circles merge into one, one circle splits into two, or one circle through the crossing is replaced by one circle.
TauCeti.PDCode.card_circlesAt_add_card_circlesAt_le_three {n : ℕ} (D : TauCeti.PDCode n)
{s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (hc : s c ≠ t c) :
(D.circlesAt s c).card + (D.circlesAt t c).card ≤ 3
Lean
Formalized in Tau Ceti as TauCeti.PDCode.card_circlesAt_add_card_circlesAt_le_three.
Sources
TheoremThe boundary-count criterion for noninterleaving#
A chord diagram on a nonempty boundary
circle, with matching an involution σ and m = n - orbitCount σ bands, has exactly m + 1
boundary cycles if and only if no two of its bands interleave.
Function.Involutive.orbitCount_finRotate_mul_add_orbitCount_eq_iff {n : ℕ} [NeZero n]
{σ : Equiv.Perm (Fin n)} (hinv : Function.Involutive ⇑σ) :
TauCeti.orbitCount (finRotate n * σ) + TauCeti.orbitCount σ = n + 1 ↔ σ.IsNoncrossingMatching
Lean
Formalized in Tau Ceti as Function.Involutive.orbitCount_finRotate_mul_add_orbitCount_eq_iff.
Sources
TheoremTauCeti.Khovanov.isFrobenius#
The dual numbers with the Khovanov comultiplication satisfy the Frobenius equation.
TauCeti.Khovanov.isFrobenius.{u_1} (R : Type u_1) [CommSemiring R] :
Coalgebra.IsFrobenius R (DualNumber R)
DefinitionCategoryTheory.Functor.cubeComplex#
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.
CategoryTheory.Functor.cubeComplex.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {ι : Type w}
[Fintype ι] [LinearOrder ι] (F : CategoryTheory.Functor (Finset ι) C) : CochainComplex C ℤ
Used by 3
AbbreviationTauCeti.Khovanov.CircleTensor#
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.
TauCeti.Khovanov.CircleTensor.{u, u_1} (R : Type u) [CommSemiring R] (ι : Type u_1) :
Type (max u u_1)
DefinitionTauCeti.Khovanov.quantumGrading#
The quantum grading of the Khovanov Frobenius algebra R[ε]: the basis vector 1 spans
degree 1, the basis vector ε spans degree -1, and every other degree is zero. It is the
grading of the free module on the basis 1, ε by TauCeti.Khovanov.quantumDegree, transported
to R[ε].
TauCeti.Khovanov.quantumGrading.{u} (R : Type u) [CommRing R] :
TauCeti.InternalGrading R (DualNumber R) ℤ
DefinitionTauCeti.Khovanov.fiberwiseSplit#
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.
TauCeti.Khovanov.fiberwiseSplit.{u_1, u_3, u_4} {R : Type u_1} [CommSemiring R] {σ : Type u_3}
{τ : Type u_4} [Fintype σ] [Fintype τ] [DecidableEq τ] (f : σ → τ) :
TauCeti.Khovanov.CircleTensor R τ →ₗ[R] TauCeti.Khovanov.CircleTensor R σ
Uses 1 · Used by 3
DefinitionTauCeti.PDCode.resolutionMergeMap#
Multiplication on the two circles merged at c, and identity on every other factor of the
actual resolved-circle tensor. The one-circle target condition follows from the source count.
TauCeti.PDCode.resolutionMergeMap.{u} {n : ℕ} (D : TauCeti.PDCode n) {s t : Fin n → Bool}
{c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (hc : s c ≠ t c)
(hs : (D.circlesAt s c).card = 2) (R : Type u) [CommSemiring R] :
TauCeti.Khovanov.CircleTensor R (D.ResolvedCircle s) →ₐ[R]
TauCeti.Khovanov.CircleTensor R (D.ResolvedCircle t)
Uses 2 · Used by 2
DefinitionTauCeti.PDCode.resolutionSplitMap#
Comultiplication on the circle through c, splitting it into the two circles of the target
through c, and identity on every other factor of the actual resolved-circle tensor. The
one-circle source condition follows from the target count.
TauCeti.PDCode.resolutionSplitMap.{u} {n : ℕ} (D : TauCeti.PDCode n) {s t : Fin n → Bool}
{c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (hc : s c ≠ t c)
(ht : (D.circlesAt t c).card = 2) (R : Type u) [CommSemiring R] :
TauCeti.Khovanov.CircleTensor R (D.ResolvedCircle s) →ₗ[R]
TauCeti.Khovanov.CircleTensor R (D.ResolvedCircle t)
Uses 3 · Used by 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.