Combinatorial Heegaard Floer and grid homology

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe commutation map is a chain map#

Over a commutative semiring of characteristic two, counting empty pentagons turning on either side of the replaced grid line intertwines the unblocked differentials of a grid diagram and of the diagram with the two columns of the turn exchanged. This holds at every column turn: the two marking segments need not be non-interleaving.

TauCeti.GridDiagram.commutationMap_comp_unblockedDifferential.{u_1} {n : ℕ}
  (G : TauCeti.GridDiagram n) (C : TauCeti.GridDiagram.ColumnTurn n) (R : Type u_1) [CommSemiring R]
  [CharP R 2] :
  G.commutationMap R C ∘ₛₗ G.unblockedDifferential R =
    (TauCeti.GridDiagram.swapColumns C.column ((finRotate n) C.column) G).unblockedDifferential
        R ∘ₛₗ
      G.commutationMap R C
Lean

Formalized in Tau Ceti as TauCeti.GridDiagram.commutationMap_comp_unblockedDifferential.

Sources
LeanTauCeti.GridDiagram.commutationMap_comp_unblockedDifferential
Used by 1
Used byThe commutation map on GH⁻ preserves the class of the X-marking state

TheoremTauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq#

The homotopy equation ∂ ∘ H + H ∘ ∂ = 1 + Ψ ∘ Φ of a column commutation, over any commutative semiring of characteristic two: the hexagon-counting map H is a chain homotopy between the identity of GC⁻(G) and the round trip through the commuted diagram.

TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq.{u_1} {n : ℕ}
  (G : TauCeti.GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R]
  [CharP R 2] (c : TauCeti.GridChainMinus R n) :
  (G.unblockedDifferential R) ((G.commutationHomotopy R C) c) +
      (G.commutationHomotopy R C) ((G.unblockedDifferential R) c) =
    c +
      ((TauCeti.GridDiagram.swapColumns C.column ((finRotate n) C.column) G).commutationMap R
          C.reverse.toColumnTurn)
        ((G.commutationMap R C.toColumnTurn) c)
Lean

Formalized in Tau Ceti as TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq.

Sources
LeanTauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq

TheoremStabilization invariance of GH⁻#

The map GH⁻(G') → GH⁻(G) induced by the stabilization chain map is bijective.

TauCeti.GridDiagram.stabilizeXHomologyMap_bijective.{u_1} {n : ℕ} (G : TauCeti.GridDiagram n)
  (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :
  Function.Bijective ⇑(G.stabilizeXHomologyMap s R)
Lean

Formalized in Tau Ceti as TauCeti.GridDiagram.stabilizeXHomologyMap_bijective.

Sources
LeanTauCeti.GridDiagram.stabilizeXHomologyMap_bijective
Uses 1
Proof usesGraded Nakayama lemma for free complexes over a polynomial ring

TheoremStabilization multiplies the Poincaré series by W#

The Poincaré series of the fully blocked homology of the stabilization splitting an X-marking is that of the original diagram times the series W of the stabilization factor.

TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPoincareSeries_stabilizeX {n : ℕ}
  (G : TauCeti.OddComponentGridDiagram n) (s : Fin n) :
  (G.stabilizeX s).bigradedFullyBlockedHomologyPoincareSeries =
    G.bigradedFullyBlockedHomologyPoincareSeries * TauCeti.Bigraded.W
Lean

Formalized in Tau Ceti as TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPoincareSeries_stabilizeX.

Sources
LeanTauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPoincareSeries_stabilizeX

Theoremτ of a torus knot grid#

on the standard grid of the (p + 1, q + 1) torus knot, 2 τ = -p q.

TauCeti.GridDiagram.two_mul_tau_torusLink.{u_1} {p q : ℕ} (h : (p + 1).Coprime (q + 1))
  (K : Type u_1) [Field K] [CharP K 2] : 2 * ⋯.tau K = -(↑p * ↑q)
Lean

Formalized in Tau Ceti as TauCeti.GridDiagram.two_mul_tau_torusLink.

Sources
LeanTauCeti.GridDiagram.two_mul_tau_torusLink
Uses 1
Statement usesThe invariant τ of a knot grid diagram

TheoremThe structure theorem for finitely generated graded k[X]-modules#

Let X lower degree by d ≠ 0 in a finitely generated graded k[X]-module M over a field. Then M is the internal direct sum of cyclic submodules k[X] ∙ t i generated by homogeneous elements t i, indexed by the disjoint union of two finite types: for i in the first, t i has zero annihilator, so k[X] ∙ t i is a free X-tower; for j in the second, t j has annihilator (X ^ m j) with m j ≠ 0, so k[X] ∙ t j ≅ k[X] ⧸ (X ^ m j).

TauCeti.InternalGrading.exists_isInternal_span_singleton.{u, u_1} {k : Type u_1} {M : Type u}
  [Field k] [AddCommGroup M] [_root_.Module k M] [_root_.Module (Polynomial k) M]
  [IsScalarTower k (Polynomial k) M] {G : TauCeti.InternalGrading k M ℤ} {d : ℕ}
  [Module.Finite (Polynomial k) M] (hd : d ≠ 0)
  (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece ℤ p → Polynomial.X • x ∈ G.piece ℤ (p - ↑d)) :
  ∃ ι κ,
    ∃ (_ : Finite ι) (_ : Finite κ),
      ∃ t deg m,
        (∀ (i : ι ⊕ κ), t i ∈ G.piece ℤ (deg i)) ∧
          (∀ (i : ι), Ideal.torsionOf (Polynomial k) M (t (Sum.inl i)) = ⊥) ∧
            (∀ (j : κ), m j ≠ 0) ∧
              (∀ (j : κ),
                  Ideal.torsionOf (Polynomial k) M (t (Sum.inr j)) =
                    Ideal.span {Polynomial.X ^ m j}) ∧
                DirectSum.IsInternal fun i => Polynomial k ∙ t i
Lean

Formalized in Tau Ceti as TauCeti.InternalGrading.exists_isInternal_span_singleton.

Sources
LeanTauCeti.InternalGrading.exists_isInternal_span_singleton
Uses 2
Proof usesThe free part of the structure theorem · The torsion part of the structure theorem

TheoremThe graded Euler characteristic of fully blocked grid homology is the normalized grid determinant# 

TauCeti.OddComponentGridDiagram.gradedHomologyEulerChar_eq_smul_T_mul_det_weightMatrix {n : ℕ}
  (G : TauCeti.OddComponentGridDiagram n) :
  G.gradedHomologyEulerChar =
    (Equiv.Perm.sign (↑G).O.toPerm * (↑n + 1).negOnePow) •
      (LaurentPolynomial.T (↑G).alexanderTwoShift * (↑G).weightMatrix.det)
Lean

Formalized in Tau Ceti as TauCeti.OddComponentGridDiagram.gradedHomologyEulerChar_eq_smul_T_mul_det_weightMatrix.

Sources
LeanTauCeti.OddComponentGridDiagram.gradedHomologyEulerChar_eq_smul_T_mul_det_weightMatrix
Uses 1
Proof usesEuler--Poincaré in one Alexander degree

The unknotting number of a grid link: the least number of crossing changes turning it into the unknot, or ⊤ if no sequence of crossing changes does.

TauCeti.GridLink.unknottingNumber (L : TauCeti.GridLink) : ℕ∞
Lean

Formalized in Tau Ceti as TauCeti.GridLink.unknottingNumber.

Sources
LeanTauCeti.GridLink.unknottingNumber

TheoremA chain map of bidegree (-2, -1) across a crossing change#

If the segments of the two columns of the column turn C interleave and the O-marking of the first column does not lie on the arc of the second, then the commutation map turning in the row of the X-marking of the first column has bidegree (-2, -1), the bidegree of multiplication by U.

TauCeti.GridDiagram.commutationBidegree_eq_of_notMem_columnArc {n : ℕ} {G : TauCeti.GridDiagram n}
  (C : TauCeti.GridDiagram.ColumnTurn n)
  (h : G.ColumnsInterleaving C.column ((finRotate n) C.column))
  (hO : G.O.toPerm C.column ∉ G.columnArc ((finRotate n) C.column))
  (hs : C.turnRow = G.X.toPerm C.column) : G.commutationBidegree C = (-2, -1)
Lean

Formalized in Tau Ceti as TauCeti.GridDiagram.commutationBidegree_eq_of_notMem_columnArc.

Sources
LeanTauCeti.GridDiagram.commutationBidegree_eq_of_notMem_columnArc

DefinitionThe invariant τ of a knot grid diagram#

minus the largest Alexander degree of a homogeneous element of the unblocked grid homology GH⁻(G) that is not K[U]-torsion.

Over a Noetherian K, the supremum is attained as soon as GH⁻(G) is not a torsion module (isGreatest_nonTorsionDegrees_neg_tau); if GH⁻(G) is torsion the value is 0, the supremum of the empty set. It is an invariant of the presented knot: knot grids connected by grid moves have the same τ (tau_eq_of_movesTo, in Homology/Invariance.lean). This is the grid definition of the concordance invariant τ of Ozsváth--Stipsicz--Szabó.

TauCeti.GridDiagram.IsKnot.tau.{u_1} {n : ℕ} {G : TauCeti.GridDiagram n} (hG : G.IsKnot)
  (K : Type u_1) [CommRing K] [CharP K 2] : ℤ
Lean

Formalized in Tau Ceti as TauCeti.GridDiagram.IsKnot.tau.

Sources
LeanTauCeti.GridDiagram.IsKnot.tau
Used by 1
Used byτ of a torus knot grid

TheoremThe commutation map on GH⁻ preserves the class of the X-marking state#

Under the condition of commutationMap_single_X, the induced map on unblocked grid homology sends the class of the X-marking state of G to that of the commuted diagram.

TauCeti.GridDiagram.unblockedHomologyCommutationMap_XMarkingClass.{u_1} {n : ℕ}
  (G : TauCeti.GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (C : G.ColumnCommutationData)
  (hs : C.turnRow ≠ G.X.toPerm ((finRotate n) C.column)) :
  (G.unblockedHomologyCommutationMap R C.toColumnTurn) (G.XMarkingClass R) =
    (TauCeti.GridDiagram.swapColumns C.column ((finRotate n) C.column) G).XMarkingClass R
Lean

Formalized in Tau Ceti as TauCeti.GridDiagram.unblockedHomologyCommutationMap_XMarkingClass.

Sources
LeanTauCeti.GridDiagram.unblockedHomologyCommutationMap_XMarkingClass
Uses 1
Proof usesThe commutation map is a chain map

DefinitionTauCeti.HeegaardRegionSystem.hatDifferential#

The hat differential of a Heegaard diagram with region Euler characteristics χ: the ZMod 2-linear endomorphism of the free module on generators whose coefficient from x to y is the number, modulo two, of nonnegative domains of Maslov index one from x to y avoiding the basepoints (TauCeti.HeegaardRegionSystem.hatCoefficient).

TauCeti.HeegaardRegionSystem.hatDifferential.{u, v, w} {n : ℕ} {Point : Type u} {Region : Type v}
  {Basepoint : Type w} (H : TauCeti.HeegaardRegionSystem n Point Region Basepoint) [Fintype Point]
  [DecidableEq Region] [Fintype Region] (χ : Region → ℤ) :
  (H.Generator →₀ ZMod 2) →ₗ[ZMod 2] H.Generator →₀ ZMod 2
Lean

Formalized in Tau Ceti as TauCeti.HeegaardRegionSystem.hatDifferential.

Sources
LeanTauCeti.HeegaardRegionSystem.hatDifferential

DefinitionTauCeti.HeegaardRegionSystem.IsNice#

A pointed Heegaard diagram, with region Euler characteristics χ, is nice when every region containing no basepoint is a bigon or a square: a disk, of Euler characteristic one, with two or four corners.

TauCeti.HeegaardRegionSystem.IsNice.{u, v, w} {n : ℕ} {Point : Type u} {Region : Type v}
  {Basepoint : Type w} (H : TauCeti.HeegaardRegionSystem n Point Region Basepoint) [Fintype Point]
  [DecidableEq Region] (χ : Region → ℤ) : Prop
Lean

Formalized in Tau Ceti as TauCeti.HeegaardRegionSystem.IsNice.

Sources
LeanTauCeti.HeegaardRegionSystem.IsNice

TheoremEuler--Poincaré in one Alexander degree#

The alternating dimension of fully blocked grid homology equals the alternating count of grid states.

TauCeti.OddComponentGridDiagram.alexanderHomologyEulerChar_eq_alexanderEulerChar {n : ℕ}
  (G : TauCeti.OddComponentGridDiagram n) (a : ℤ) :
  G.alexanderHomologyEulerChar a = G.alexanderEulerChar (ZMod 2) a
Lean

Formalized in Tau Ceti as TauCeti.OddComponentGridDiagram.alexanderHomologyEulerChar_eq_alexanderEulerChar.

Sources
LeanTauCeti.OddComponentGridDiagram.alexanderHomologyEulerChar_eq_alexanderEulerChar
Uses 1 · Used by 1
Proof usesEuler–Poincaré for cubes
Used byThe graded Euler characteristic of fully blocked grid homology is the normalized grid determinant

TheoremThe torsion part of the structure theorem#

Let X lower degree by d ≠ 0 in a finitely generated graded k[X]-module over a field. Then every homogeneous k[X]-submodule L contained in the torsion submodule is the independent sum of finitely many cyclic submodules k[X] ∙ t i, where each t i is homogeneous with annihilator (X ^ m i) for some m i ≠ 0. Thus each summand is isomorphic to k[X] ⧸ (X ^ m i) (Ideal.quotTorsionOfEquivSpanSingleton).

TauCeti.InternalGrading.exists_iSupIndep_iSup_span_singleton_eq_of_le_torsion.{u, u_1}
  {k : Type u_1} {M : Type u} [Field k] [AddCommGroup M] [_root_.Module k M]
  [_root_.Module (Polynomial k) M] [IsScalarTower k (Polynomial k) M]
  {G : TauCeti.InternalGrading k M ℤ} {d : ℕ} [Module.Finite (Polynomial k) M] (hd : d ≠ 0)
  (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece ℤ p → Polynomial.X • x ∈ G.piece ℤ (p - ↑d))
  (L : Submodule (Polynomial k) M) (hL : DirectSum.SetLike.IsHomogeneous (G.piece ℤ) L)
  (hLT : L ≤ Submodule.torsion (Polynomial k) M) :
  ∃ ι,
    ∃ (_ : Finite ι),
      ∃ t deg m,
        (∀ (i : ι), t i ∈ G.piece ℤ (deg i)) ∧
          (∀ (i : ι), m i ≠ 0) ∧
            (∀ (i : ι), Ideal.torsionOf (Polynomial k) M (t i) = Ideal.span {Polynomial.X ^ m i}) ∧
              (iSupIndep fun i => Polynomial k ∙ t i) ∧ ⨆ i, Polynomial k ∙ t i = L
Lean

Formalized in Tau Ceti as TauCeti.InternalGrading.exists_iSupIndep_iSup_span_singleton_eq_of_le_torsion.

Sources
LeanTauCeti.InternalGrading.exists_iSupIndep_iSup_span_singleton_eq_of_le_torsion
Used by 1
Used byThe structure theorem for finitely generated graded k[X]-modules

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.