The circles of a smoothed PD-code

Smoothing every crossing of a PD-code according to a state s leaves a disjoint union of circles, which TauCeti.PDCode.stateLoopCount counts. This file constructs those circles as a finite type, the set of circles a Khovanov chain group is built on.

A circle meeting a crossing is a connected component of the graph on the half-edges whose edges are the arcs of the code (TauCeti.PDCode.edgePair) and the arcs of the chosen local smoothings (TauCeti.PDCode.smoothingTurn). So TauCeti.PDCode.CrossingCircle D s is the quotient of the half-edges by the equivalence relation generated by these two perfect matchings. The crossing-free circles of the code, recorded only by their number, are adjoined as Fin D.crossinglessComponentCount to give TauCeti.PDCode.ResolvedCircle D s.

The traversal TauCeti.PDCode.statePerm, crossing an arc and then following a smoothing, is the product of the two matchings. Its orbits are the circles with a direction of travel, and following the other end of an arc reverses that direction (TauCeti.PDCode.stateCycleReversal). By the general theory of two perfect matchings in TauCeti/Combinatorics/Enumerative/PerfectMatching.lean, the circles are the directed traversal orbits modulo reversal, and no directed orbit is its own reverse, even on a circle made of a single arc and a single smoothing arc. Hence every circle carries exactly two directed orbits, which is the halving in TauCeti.PDCode.stateLoopCount.

Main definitions

• TauCeti.PDCode.CircleStep: the relation joining a half-edge to its partners along an arc and along the chosen smoothing.
• TauCeti.PDCode.CrossingCircle: the circles of a smoothed code that meet a crossing.
• TauCeti.PDCode.ResolvedCircle: all circles of a smoothed code.
• TauCeti.PDCode.stateCycleReversal: reversing the direction of travel on the directed traversal orbits of a smoothed code.
• TauCeti.PDCode.crossingCircleEquiv: the circles meeting a crossing are the directed traversal orbits modulo reversal.

Main results

• TauCeti.PDCode.CrossingCircle.mk_eq_mk_iff: two half-edges lie on one circle exactly when the second lies on the directed traversal orbit of the first or of its partner along the arc.
• TauCeti.PDCode.isPerfectMatching_stateCycleReversal: no directed traversal orbit is its own reverse.
• TauCeti.PDCode.two_mul_card_crossingCircle: the circles meeting a crossing are half as many as the directed traversal orbits.
• TauCeti.PDCode.card_resolvedCircle: there are TauCeti.PDCode.stateLoopCount D s circles.

References

• M. Khovanov, A categorification of the Jones polynomial, Duke Math. J. 101 (2000), 359-426, §2 (the circles of a resolution).
• D. Bar-Natan, On Khovanov's categorification of the Jones polynomial, Algebr. Geom. Topol. 2 (2002), 337-370, §2.

@[reducible, inline]

abbrev TauCeti.PDCode.CircleStep {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (x y : Fin (4 * n)) : Prop

The relation joining a half-edge x to the other end y of its arc, and to the half-edge y that the local smoothing chosen by the state s joins it to. The equivalence relation it generates has the circles of the smoothed diagram that meet a crossing as its classes (TauCeti.PDCode.CrossingCircle).

This is an abbrev, so that the general results about the equivalence relation generated by two involutions, stated for the relation fun a b ↦ b = g a ∨ b = f a, apply to it directly.

theorem TauCeti.PDCode.circleStep_iff {n : ℕ} (D : PDCode n) (s : Fin n → Bool) {x y : Fin (4 * n)} : D.CircleStep s x y ↔ y = ↑D.edgePair x ∨ y = (D.smoothingTurn (D.smoothingChoice s)) x

The defining property of the circle relation.

theorem TauCeti.PDCode.circleStep_comm {n : ℕ} (D : PDCode n) (s : Fin n → Bool) {x y : Fin (4 * n)} : D.CircleStep s x y ↔ D.CircleStep s y x

The circle relation is symmetric, since it is built from two involutions.

@[reducible, inline]

abbrev TauCeti.PDCode.CrossingCircle {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : Type

The circles meeting a crossing of the diagram smoothed according to the state s: the classes of half-edges under the equivalence relation generated by TauCeti.PDCode.CircleStep.

@[reducible, inline]

abbrev TauCeti.PDCode.ResolvedCircle {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : Type

All circles of the diagram smoothed according to the state s: the circles meeting a crossing, together with one label for each crossing-free circle of the code.

theorem TauCeti.PDCode.resolvedCircle_funext {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {φ ψ : D.ResolvedCircle s → D.ResolvedCircle t} (hφ : ∀ (x : Fin (4 * n)), φ (Sum.inl ⟦x⟧) = Sum.inl ⟦x⟧) (hψ : ∀ (x : Fin (4 * n)), ψ (Sum.inl ⟦x⟧) = Sum.inl ⟦x⟧) (hφ' : ∀ (i : Fin D.crossinglessComponentCount), φ (Sum.inr i) = Sum.inr i) (hψ' : ∀ (i : Fin D.crossinglessComponentCount), ψ (Sum.inr i) = Sum.inr i) : φ = ψ

Two correspondences of resolved circles that send the circle of every half-edge to its circle and retain every crossing-free label are equal.

theorem TauCeti.PDCode.eqvGen_circleStep_iff {n : ℕ} (D : PDCode n) (s : Fin n → Bool) {x y : Fin (4 * n)} : Relation.EqvGen (D.CircleStep s) x y ↔ (D.statePerm s).SameCycle x y ∨ (D.statePerm s).SameCycle (↑D.edgePair x) y

Two half-edges lie on one circle of a smoothed diagram exactly when the second lies on the directed traversal orbit of the first, or on that of the other end of the first's arc.

@[instance_reducible]

instance TauCeti.PDCode.instDecidableRelFinHMulNatOfNatEqvGenCircleStep {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : DecidableRel (Relation.EqvGen (D.CircleStep s))

Lying on one circle of a smoothed diagram is decidable, by iterating the traversal.

@[instance_reducible]

instance TauCeti.PDCode.instDecidableEqCrossingCircle {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : DecidableEq (D.CrossingCircle s)

Equality of circles of a smoothed diagram is decidable.

@[instance_reducible]

instance TauCeti.PDCode.instFintypeCrossingCircle {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : Fintype (D.CrossingCircle s)

The circles meeting a crossing of a smoothed diagram form a finite type, computably.

theorem TauCeti.PDCode.CrossingCircle.mk_eq_mk_iff {n : ℕ} {D : PDCode n} {s : Fin n → Bool} {x y : Fin (4 * n)} : ⟦x⟧ = ⟦y⟧ ↔ (D.statePerm s).SameCycle x y ∨ (D.statePerm s).SameCycle (↑D.edgePair x) y

Two half-edges lie on one circle exactly when the second lies on the directed traversal orbit of the first, or on that of the other end of the first's arc.

@[simp]

theorem TauCeti.PDCode.CrossingCircle.mk_edgePair {n : ℕ} {D : PDCode n} {s : Fin n → Bool} (x : Fin (4 * n)) : ⟦↑D.edgePair x⟧ = ⟦x⟧

The two ends of an arc lie on the same circle.

@[simp]

theorem TauCeti.PDCode.CrossingCircle.mk_smoothingTurn {n : ℕ} {D : PDCode n} {s : Fin n → Bool} (x : Fin (4 * n)) : ⟦(D.smoothingTurn (D.smoothingChoice s)) x⟧ = ⟦x⟧

The two ends of an arc of the chosen smoothing lie on the same circle.

theorem TauCeti.PDCode.CrossingCircle.mk_statePerm {n : ℕ} {D : PDCode n} {s : Fin n → Bool} (x : Fin (4 * n)) : ⟦(D.statePerm s) x⟧ = ⟦x⟧

Traversal stays on a circle.

theorem TauCeti.PDCode.CrossingCircle.mk_crossing_slotSmoothing {n : ℕ} {D : PDCode n} {s : Fin n → Bool} (c : Fin n) (k : Fin 4) : ⟦D.crossing c ((slotSmoothing (D.smoothingChoice s c)) k)⟧ = ⟦D.crossing c k⟧

The two half-edges at a crossing c joined by the local smoothing there lie on the same circle.

def TauCeti.PDCode.stateCycleReversal {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : Equiv.Perm (Quotient (Equiv.Perm.SameCycle.setoid (D.statePerm s)))

Reversal of the directed traversal orbits of the diagram smoothed according to the state s: following the other end of an arc carries each directed orbit of TauCeti.PDCode.statePerm onto the same circle traversed in the opposite direction.

@[simp]

theorem TauCeti.PDCode.stateCycleReversal_mk {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (x : Fin (4 * n)) : (D.stateCycleReversal s) ⟦x⟧ = ⟦↑D.edgePair x⟧

Reversal sends the directed orbit of a half-edge to that of the other end of its arc.

theorem TauCeti.PDCode.isPerfectMatching_stateCycleReversal {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : IsPerfectMatching (D.stateCycleReversal s)

No directed traversal orbit of a smoothed diagram is its own reverse, and reversing twice gives back every orbit: reversal is a perfect matching of the directed orbits.

noncomputable def TauCeti.PDCode.crossingCircleEquiv {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : D.CrossingCircle s ≃ Quotient (Equiv.Perm.SameCycle.setoid (D.stateCycleReversal s))

The circles meeting a crossing are the directed traversal orbits modulo reversal: the circle through a half-edge corresponds to the reversal orbit of its directed traversal orbit.

@[simp]

theorem TauCeti.PDCode.crossingCircleEquiv_mk {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (x : Fin (4 * n)) : (D.crossingCircleEquiv s) ⟦x⟧ = ⟦⟦x⟧⟧

The circle through a half-edge corresponds to the reversal orbit of its directed traversal orbit.

theorem TauCeti.PDCode.two_mul_card_crossingCircle {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : 2 * Fintype.card (D.CrossingCircle s) = orbitCount (D.statePerm s)

Each circle meeting a crossing carries exactly two directed traversal orbits, so there are half as many such circles as directed orbits.

theorem TauCeti.PDCode.card_resolvedCircle {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : Fintype.card (D.ResolvedCircle s) = D.stateLoopCount s

The number of circles of a smoothed diagram. The diagram smoothed according to the state s has TauCeti.PDCode.stateLoopCount D s circles, the crossing-free circles included.

theorem TauCeti.PDCode.card_resolvedCircle_eq_crossinglessComponentCount (D : PDCode 0) (s : Fin 0 → Bool) : Fintype.card (D.ResolvedCircle s) = D.crossinglessComponentCount

Every smoothing of a crossing-free diagram has one circle for each of its components.

theorem TauCeti.PDCode.one_le_card_resolvedCircle_of_componentCount_pos {n : ℕ} (D : PDCode n) (h : 0 < D.componentCount) (s : Fin n → Bool) : 1 ≤ Fintype.card (D.ResolvedCircle s)

Every smoothing of a diagram with a component has a circle.

theorem TauCeti.PDCode.one_le_card_resolvedCircle {n : ℕ} (D : PDCode n) (hn : n ≠ 0) (s : Fin n → Bool) : 1 ≤ Fintype.card (D.ResolvedCircle s)

Every smoothing of a diagram with a crossing has a circle.