Fibres of the resolution saddle correspondence

When one target circle passes through a changed crossing, the saddle correspondence collapses all source circles through that crossing and is a bijection elsewhere. This file characterizes its fibres and extends it to all resolved circles, retaining every crossing-free circle label. The only possible collision is between the source circles in slots 0 and 2. When these circles are distinct, the correspondence is exactly a merge of two circles, and the total circle count decreases by one; along any saddle edge it changes by exactly one (TauCeti.PDCode.card_resolvedCircle_of_saddle). These facts identify the factors multiplied by a resolution saddle on indexed circle tensors.

More generally, if only one circle of t passes through each crossing at which s and t differ, the circle of a half-edge in s determines its circle in t (TauCeti.PDCode.coarseningResolvedCircleMap). This compares states two crossings apart around a face of the cube of resolutions.

References

• M. Khovanov, A categorification of the Jones polynomial, Duke Math. J. 101 (2000), §2.

@[simp]

theorem TauCeti.PDCode.saddleCircleMap_mem_circlesAt_iff {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (C : D.CrossingCircle s) : D.saddleCircleMap hst ht C ∈ D.circlesAt t c ↔ C ∈ D.circlesAt s c

A source circle meets the changed crossing exactly when its image does.

theorem TauCeti.PDCode.saddleCircleMap_eq_iff {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (C C' : D.CrossingCircle s) : D.saddleCircleMap hst ht C = D.saddleCircleMap hst ht C' ↔ C = C' ∨ C ∈ D.circlesAt s c ∧ C' ∈ D.circlesAt s c

Two source circles have the same saddle image exactly when they coincide or both meet the changed crossing.

def TauCeti.PDCode.saddleResolvedCircleMap {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) : D.ResolvedCircle s → D.ResolvedCircle t

The saddle correspondence on all resolved circles. It preserves each crossing-free label.

@[simp]

theorem TauCeti.PDCode.saddleResolvedCircleMap_inl {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (C : D.CrossingCircle s) : D.saddleResolvedCircleMap hst ht (Sum.inl C) = Sum.inl (D.saddleCircleMap hst ht C)

On a crossing-bearing circle, the full saddle map is the half-edge quotient map.

@[simp]

theorem TauCeti.PDCode.saddleResolvedCircleMap_inr {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (i : Fin D.crossinglessComponentCount) : D.saddleResolvedCircleMap hst ht (Sum.inr i) = Sum.inr i

Crossing-free circles retain their labels under the saddle.

theorem TauCeti.PDCode.saddleResolvedCircleMap_surjective {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) : Function.Surjective (D.saddleResolvedCircleMap hst ht)

Every target resolved circle is hit by the saddle.

theorem TauCeti.PDCode.saddleResolvedCircleMap_eq_iff {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (C C' : D.ResolvedCircle s) : D.saddleResolvedCircleMap hst ht C = D.saddleResolvedCircleMap hst ht C' ↔ C = C' ∨ (C = Sum.inl ⟦D.crossing c 0⟧ ∨ C = Sum.inl ⟦D.crossing c 2⟧) ∧ (C' = Sum.inl ⟦D.crossing c 0⟧ ∨ C' = Sum.inl ⟦D.crossing c 2⟧)

The only possible distinct circles identified by the full saddle map are the two circles through the changed crossing, represented by slots 0 and 2.

theorem TauCeti.PDCode.saddleResolvedCircleMap_eq_crossing_iff {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (C : D.ResolvedCircle s) : D.saddleResolvedCircleMap hst ht C = Sum.inl ⟦D.crossing c 0⟧ ↔ C = Sum.inl ⟦D.crossing c 0⟧ ∨ C = Sum.inl ⟦D.crossing c 2⟧

The fibre over the target circle through the crossing consists of the source circles through slots 0 and 2.

theorem TauCeti.PDCode.filter_saddleResolvedCircleMap_eq_crossing {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) : {C : D.ResolvedCircle s | D.saddleResolvedCircleMap hst ht C = Sum.inl ⟦D.crossing c 0⟧} = {Sum.inl ⟦D.crossing c 0⟧, Sum.inl ⟦D.crossing c 2⟧}

As a finite set, the fibre through the crossing is the pair of source circles in opposite slots; repeated entries are counted only once.

theorem TauCeti.PDCode.prod_filter_saddleResolvedCircleMap_eq_crossing {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) {M : Type u_1} [CommMonoid M] (hs : (D.circlesAt s c).card = 2) (x : D.ResolvedCircle s → M) : ∏ C' : D.ResolvedCircle s with D.saddleResolvedCircleMap hst ht C' = Sum.inl ⟦D.crossing c 0⟧, x C' = x (Sum.inl ⟦D.crossing c 0⟧) * x (Sum.inl ⟦D.crossing c 2⟧)

The product over the changed fibre is the product of the two merged factors.

theorem TauCeti.PDCode.prod_filter_saddleResolvedCircleMap_eq_of_ne {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) {M : Type u_1} [CommMonoid M] (C : D.ResolvedCircle s) (hC₀ : C ≠ Sum.inl ⟦D.crossing c 0⟧) (hC₂ : C ≠ Sum.inl ⟦D.crossing c 2⟧) (x : D.ResolvedCircle s → M) : ∏ C' : D.ResolvedCircle s with D.saddleResolvedCircleMap hst ht C' = D.saddleResolvedCircleMap hst ht C, x C' = x C

The product over an unchanged fibre is its sole source factor. This includes every crossing-free circle.

@[simp]

theorem TauCeti.PDCode.decide_exists_saddleResolvedCircleMap_eq_crossing {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (l : D.ResolvedCircle s → Bool) : decide (∃ (C' : D.ResolvedCircle s), D.saddleResolvedCircleMap hst ht C' = Sum.inl ⟦D.crossing c 0⟧ ∧ l C' = true) = (l (Sum.inl ⟦D.crossing c 0⟧) || l (Sum.inl ⟦D.crossing c 2⟧))

The target label at the changed circle is the Boolean disjunction of the two source labels. This describes label transport even when the two source circles coincide.

@[simp]

theorem TauCeti.PDCode.decide_exists_saddleResolvedCircleMap_eq_of_notMem {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (l : D.ResolvedCircle s → Bool) (C : D.CrossingCircle s) (hC : C ∉ D.circlesAt s c) : decide (∃ (C' : D.ResolvedCircle s), D.saddleResolvedCircleMap hst ht C' = D.saddleResolvedCircleMap hst ht (Sum.inl C) ∧ l C' = true) = l (Sum.inl C)

A crossing-bearing circle avoiding the changed crossing retains its Boolean label.

theorem TauCeti.PDCode.existsUnique_saddleResolvedCircleMap_eq {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (C : D.ResolvedCircle t) (hC : C ≠ Sum.inl ⟦D.crossing c 0⟧) : ∃! C' : D.ResolvedCircle s, D.saddleResolvedCircleMap hst ht C' = C

Away from the merged target circle every fibre is a singleton.

theorem TauCeti.PDCode.card_resolvedCircle_source_eq_target_add_one {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (hs : (D.circlesAt s c).card = 2) : Fintype.card (D.ResolvedCircle s) = Fintype.card (D.ResolvedCircle t) + 1

A two-to-one saddle reduces the total number of circles by one, including isolated circles.

theorem TauCeti.PDCode.card_resolvedCircle_of_saddle {n : ℕ} (D : 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) (h : (D.circlesAt s c).card = 2 ∨ (D.circlesAt t c).card = 2) : (D.circlesAt s c).card = 2 ∧ Fintype.card (D.ResolvedCircle s) = Fintype.card (D.ResolvedCircle t) + 1 ∨ (D.circlesAt t c).card = 2 ∧ Fintype.card (D.ResolvedCircle t) = Fintype.card (D.ResolvedCircle s) + 1

Along a saddle edge the circle count drops by one if two circles merge, and rises by one if a circle splits.

def TauCeti.PDCode.coarseningResolvedCircleMap {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} (h : ∀ (j : Fin n), s j ≠ t j → (D.circlesAt t j).card = 1) : D.ResolvedCircle s → D.ResolvedCircle t

The circles of a coarser smoothing. If only one circle of t passes through each crossing at which s and t differ, the circle of a half-edge in the smoothing s determines its circle in the smoothing t. Crossing-free circles retain their labels. For one changed crossing this is the saddle correspondence TauCeti.PDCode.saddleResolvedCircleMap.

@[simp]

theorem TauCeti.PDCode.coarseningResolvedCircleMap_inl_mk {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} (h : ∀ (j : Fin n), s j ≠ t j → (D.circlesAt t j).card = 1) (x : Fin (4 * n)) : D.coarseningResolvedCircleMap h (Sum.inl ⟦x⟧) = Sum.inl ⟦x⟧

The coarsening correspondence sends the circle of a half-edge to its circle in the target.

@[simp]

theorem TauCeti.PDCode.coarseningResolvedCircleMap_inr {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} (h : ∀ (j : Fin n), s j ≠ t j → (D.circlesAt t j).card = 1) (i : Fin D.crossinglessComponentCount) : D.coarseningResolvedCircleMap h (Sum.inr i) = Sum.inr i

Crossing-free circles retain their labels under the coarsening correspondence.

theorem TauCeti.PDCode.saddleResolvedCircleMap_eq_coarseningResolvedCircleMap {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (h : ∀ (j : Fin n), s j ≠ t j → (D.circlesAt t j).card = 1) : D.saddleResolvedCircleMap hst ht = D.coarseningResolvedCircleMap h

For states differing at one crossing, the coarsening correspondence is the saddle correspondence.