Other results

Results named in the rest of Tau Ceti's TauCeti.KnotTheory modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremEuler's formula for a PD-code#

The underlying graph has n vertices and 2 * n edges, so its Euler characteristic is the number of faces less the number of crossings.

TauCeti.PDCode.eulerChar_toPermutationTriple {n : ℕ} (D : TauCeti.PDCode n) :
  D.toPermutationTriple.eulerChar = ↑D.faceCount - ↑n
Lean

Formalized in Tau Ceti as TauCeti.PDCode.eulerChar_toPermutationTriple.

Sources
LeanTauCeti.PDCode.eulerChar_toPermutationTriple
Used by 2
Used byEuler–Poincaré for Khovanov homology · Khovanov's theorem

TheoremEuler–Poincaré for Khovanov homology#

over a Noetherian ring with the rank-nullity property, such as ℤ or a field, the homology Euler characteristic of the quantum component j of the normalized Khovanov complex is the coefficient of qʲ in the enhanced state sum, the signed count of enhanced states of quantum degree j.

TauCeti.OrientedPDCode.homologyEulerChar_khovanovComplex.{u} {n : ℕ} (D : TauCeti.OrientedPDCode n)
  (hD : D.IsPlanar) (R : Type u) [CommRing R] [IsNoetherianRing R] [HasRankNullity.{u, u} R]
  (j : ℤ) :
  HomologicalComplex.homologyEulerChar (D.khovanovComplex hD R j) = D.enhancedStateSum.coeff j
Lean

Formalized in Tau Ceti as TauCeti.OrientedPDCode.homologyEulerChar_khovanovComplex.

Other forms

Euler–Poincaré for the unnormalized Khovanov complex. Formalized in Tau Ceti as TauCeti.PDCode.homologyEulerChar_khovanovBracket.

TauCeti.PDCode.homologyEulerChar_khovanovBracket.{u} {n : ℕ} (D : TauCeti.PDCode n)
  (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) [IsNoetherianRing R]
  [HasRankNullity.{u, u} R] :
  HomologicalComplex.homologyEulerChar (D.khovanovBracket hD R j) =
    ∑ S,
      ↑(↑S.card).negOnePow *
        ↑(Module.finrank R
            ↥((TauCeti.Khovanov.circleQuantumGrading R
                    (D.ResolvedCircle (TauCeti.PDCode.cubeState S))).piece
                ℤ (j - ↑S.card)))
Sources
LeanTauCeti.OrientedPDCode.homologyEulerChar_khovanovComplex · TauCeti.PDCode.homologyEulerChar_khovanovBracket
Uses 9 · Used by 1
Statement usesCategoryTheory.Functor.cubeComplex · TauCeti.Khovanov.CircleTensor · TauCeti.PDCode.resolutionMergeMap · TauCeti.PDCode.resolutionSplitMap
Proof usesEuler's formula for a PD-code · Euler–Poincaré for cubes · Hurwitz's transposition bound · TauCeti.Khovanov.fiberwiseSplit · Two states differing exactly at a crossing do not both have two circles through it
Used byKhovanov's theorem

TheoremKhovanov's theorem#

the graded Euler characteristic of the Khovanov homology of a nonempty planar oriented code is (q + q⁻¹) times its Jones polynomial at t ^ (1/2) = -q, over a Noetherian ring with the rank-nullity property, such as ℤ or a field. The hypothesis 0 < componentCount says that the diagram is nonempty; the empty diagram has graded Euler characteristic 1 (TauCeti.OrientedPDCode.khovanovEulerChar_empty).

TauCeti.OrientedPDCode.khovanovEulerChar_eq_mul_eval₂_jonesPolynomial.{u} {n : ℕ}
  (D : TauCeti.OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] [IsNoetherianRing R]
  [HasRankNullity.{u, u} R] (h : 0 < D.componentCount) :
  D.khovanovEulerChar hD R =
    (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) *
      (LaurentPolynomial.eval₂ (Int.castRingHom (LaurentPolynomial ℤ))
          (-LaurentPolynomial.genericUnit ℤ))
        D.jonesPolynomial
Lean

Formalized in Tau Ceti as TauCeti.OrientedPDCode.khovanovEulerChar_eq_mul_eval₂_jonesPolynomial.

Sources
LeanTauCeti.OrientedPDCode.khovanovEulerChar_eq_mul_eval₂_jonesPolynomial
Uses 10
Statement usesCategoryTheory.Functor.cubeComplex · TauCeti.Khovanov.CircleTensor · TauCeti.PDCode.resolutionMergeMap · TauCeti.PDCode.resolutionSplitMap
Proof usesThe enhanced state sum of a nonempty diagram is (q + q⁻¹) times its Jones polynomial at t ^ (1/2) = -q · Euler's formula for a PD-code · Euler–Poincaré for Khovanov homology · Hurwitz's transposition bound · TauCeti.Khovanov.fiberwiseSplit · Two states differing exactly at a crossing do not both have two circles through it

TheoremLevine's theorem gives a boundary that is not S³#

Assuming Levine's theorem, some smooth compact contractible 4-manifold X has as boundary a closed 3-manifold Y not diffeomorphic to S³. A diffeomorphism e : Y ≃ₘ S³ would make the knot K of Levine's theorem homology concordant to the knot e ∘ K in S³ (TauCeti.SmoothEmbedding.homologyConcordant_transDiffeomorph).

TauCeti.LevineHomologyConcordanceTheorem.exists_isEmpty_diffeomorph_sphere
  (h : TauCeti.LevineHomologyConcordanceTheorem) :
  ∃ Y x,
    ∃ (_ : T2Space Y) (_ : CompactSpace Y),
      ∃ x_3,
        ∃ (_ : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))) (↑⊤) Y),
          ∃ X x_5,
            ∃ (_ : T2Space X) (_ : CompactSpace X) (_ : ContractibleSpace X),
              ∃ x_9,
                ∃ (_ :
                  IsManifold
                    ((modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))).prod
                      (modelWithCornersEuclideanHalfSpace 1))
                    (↑⊤) X),
                  ∃ κ,
                    Set.range ⇑κ = ModelWithCorners.boundary X ∧
                      IsEmpty
                        (Diffeomorph (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3)))
                          (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))) Y ↑(Metric.sphere 0 1)
                          ↑⊤)
Lean

Formalized in Tau Ceti as TauCeti.LevineHomologyConcordanceTheorem.exists_isEmpty_diffeomorph_sphere, assuming TauCeti.LevineHomologyConcordanceTheorem, a proposition Tau Ceti defines.

Sources
LeanTauCeti.LevineHomologyConcordanceTheorem.exists_isEmpty_diffeomorph_sphere

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.