Disjoint unions of PD-codes

Placing two diagrams in disjoint discs concatenates their crossings and arcs. Crossing-free circles are retained separately. This operation allows a local diagram replacement on an isolated component to be used in the presence of an arbitrary surrounding diagram.

The number of link components and the number of circles in each smoothing are additive. For nonempty diagrams the normalized convention ⟨unknot⟩ = 1 gives ⟨D ⊔ E⟩ = δ ⟨D⟩ ⟨E⟩, where δ = -(a² + a⁻²). The nonemptiness conditions matter: the empty diagram has bracket 1, and adjoining it contributes no factor of δ.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 3 (the state sum and its circle normalization).
• L. H. Kauffman, State models and the Jones polynomial, Topology 26 (1987), 395–407.

def TauCeti.PDCode.disjointUnionHalfEdgeEquiv (n m : ℕ) : Fin (4 * n) ⊕ Fin (4 * m) ≃ Fin (4 * (n + m))

Number the half-edges of two disjoint diagrams consecutively.

Equations

• TauCeti.PDCode.disjointUnionHalfEdgeEquiv n m = finSumFinEquiv.trans (finCongr ⋯)

@[simp]

theorem TauCeti.PDCode.disjointUnionHalfEdgeEquiv_inl_crossingSlot {n m : ℕ} (i : Fin n) (slot : Fin 4) : (disjointUnionHalfEdgeEquiv n m) (Sum.inl ((crossingSlotEquiv n) (i, slot))) = (crossingSlotEquiv (n + m)) (Fin.castAdd m i, slot)

The first diagram's crossing slots occupy the first block of crossings.

@[simp]

theorem TauCeti.PDCode.disjointUnionHalfEdgeEquiv_inr_crossingSlot {n m : ℕ} (i : Fin m) (slot : Fin 4) : (disjointUnionHalfEdgeEquiv n m) (Sum.inr ((crossingSlotEquiv m) (i, slot))) = (crossingSlotEquiv (n + m)) (Fin.natAdd n i, slot)

The second diagram's crossing slots occupy the second block of crossings.

@[simp]

theorem TauCeti.PDCode.disjointUnionHalfEdgeEquiv_symm_crossingSlot_castAdd {n m : ℕ} (i : Fin n) (slot : Fin 4) : (disjointUnionHalfEdgeEquiv n m).symm ((crossingSlotEquiv (n + m)) (Fin.castAdd m i, slot)) = Sum.inl ((crossingSlotEquiv n) (i, slot))

Splitting a slot in the first crossing block recovers its original label.

@[simp]

theorem TauCeti.PDCode.disjointUnionHalfEdgeEquiv_symm_crossingSlot_natAdd {n m : ℕ} (i : Fin m) (slot : Fin 4) : (disjointUnionHalfEdgeEquiv n m).symm ((crossingSlotEquiv (n + m)) (Fin.natAdd n i, slot)) = Sum.inr ((crossingSlotEquiv m) (i, slot))

Splitting a slot in the second crossing block recovers its original label.

def TauCeti.PDCode.disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) : PDCode (n + m)

The disjoint union of two PD-codes. Both the crossing labels and the half-edge labels are concatenated, and the arc matching never joins the two blocks.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PDCode.disjointUnion_halfEdge {n m : ℕ} (D : PDCode n) (E : PDCode m) : (D.disjointUnion E).halfEdge = (disjointUnionHalfEdgeEquiv n m).permCongr (D.halfEdge.sumCongr E.halfEdge)

The half-edge labelling acts separately on the two blocks.

@[simp]

theorem TauCeti.PDCode.disjointUnion_edgePair_val {n m : ℕ} (D : PDCode n) (E : PDCode m) : ↑(D.disjointUnion E).edgePair = (disjointUnionHalfEdgeEquiv n m).permCongr ((↑D.edgePair).sumCongr ↑E.edgePair)

The arc matching acts separately on the two blocks.

@[simp]

theorem TauCeti.PDCode.disjointUnion_crossinglessComponentCount {n m : ℕ} (D : PDCode n) (E : PDCode m) : (D.disjointUnion E).crossinglessComponentCount = D.crossinglessComponentCount + E.crossinglessComponentCount

Disjoint union adds the crossing-free circles.

@[simp]

theorem TauCeti.PDCode.disjointUnion_overPair_castAdd {n m : ℕ} (D : PDCode n) (E : PDCode m) (i : Fin n) : (D.disjointUnion E).overPair (Fin.castAdd m i) = D.overPair i

The over-strand at a crossing of the first summand is unchanged.

@[simp]

theorem TauCeti.PDCode.disjointUnion_overPair_natAdd {n m : ℕ} (D : PDCode n) (E : PDCode m) (i : Fin m) : (D.disjointUnion E).overPair (Fin.natAdd n i) = E.overPair i

The over-strand at a crossing of the second summand is unchanged.

theorem TauCeti.PDCode.crossing_disjointUnion_castAdd {n m : ℕ} (D : PDCode n) (E : PDCode m) (i : Fin n) (slot : Fin 4) : (D.disjointUnion E).crossing (Fin.castAdd m i) slot = (disjointUnionHalfEdgeEquiv n m) (Sum.inl (D.crossing i slot))

A crossing of the first diagram retains its four incident half-edges.

theorem TauCeti.PDCode.crossing_disjointUnion_natAdd {n m : ℕ} (D : PDCode n) (E : PDCode m) (i : Fin m) (slot : Fin 4) : (D.disjointUnion E).crossing (Fin.natAdd n i) slot = (disjointUnionHalfEdgeEquiv n m) (Sum.inr (E.crossing i slot))

A crossing of the second diagram retains its four incident half-edges.

@[simp]

theorem TauCeti.PDCode.crossingTurn_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) : (D.disjointUnion E).crossingTurn = (disjointUnionHalfEdgeEquiv n m).permCongr (D.crossingTurn.sumCongr E.crossingTurn)

The strand traversal acts separately on the two diagrams.

@[simp]

theorem TauCeti.PDCode.componentPerm_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) : (D.disjointUnion E).componentPerm = (disjointUnionHalfEdgeEquiv n m).permCongr (D.componentPerm.sumCongr E.componentPerm)

The component permutation is the disjoint sum of the two component permutations.

@[simp]

theorem TauCeti.PDCode.crossingComponentCount_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) : (D.disjointUnion E).crossingComponentCount = D.crossingComponentCount + E.crossingComponentCount

The number of components meeting crossings is additive under disjoint union.

@[simp]

theorem TauCeti.PDCode.componentCount_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) : (D.disjointUnion E).componentCount = D.componentCount + E.componentCount

The number of link components is additive under disjoint union, including crossing-free components.

@[simp]

theorem TauCeti.PDCode.mirror_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) : (D.disjointUnion E).mirror = D.mirror.disjointUnion E.mirror

Reflection commutes with disjoint union.

@[simp]

theorem TauCeti.PDCode.smoothingTurn_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) (b : Fin (n + m) → Bool) : (D.disjointUnion E).smoothingTurn b = (disjointUnionHalfEdgeEquiv n m).permCongr ((D.smoothingTurn (b ∘ Fin.castAdd m)).sumCongr (E.smoothingTurn (b ∘ Fin.natAdd n)))

Smoothing a disjoint union smooths each diagram independently.

@[simp]

theorem TauCeti.PDCode.statePerm_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) (s : Fin (n + m) → Bool) : (D.disjointUnion E).statePerm s = (disjointUnionHalfEdgeEquiv n m).permCongr ((D.statePerm (s ∘ Fin.castAdd m)).sumCongr (E.statePerm (s ∘ Fin.natAdd n)))

The state traversal is the disjoint sum of the traversals of the restricted states.

@[simp]

theorem TauCeti.PDCode.stateLoopCount_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) (s : Fin (n + m) → Bool) : (D.disjointUnion E).stateLoopCount s = D.stateLoopCount (s ∘ Fin.castAdd m) + E.stateLoopCount (s ∘ Fin.natAdd n)

The smoothing circles of a disjoint union are the circles from the two summands.

The state sum

@[simp]

theorem TauCeti.PDCode.kauffmanBracket_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) {R : Type u_1} [CommRing R] (a : Rˣ) (hD : 0 < D.componentCount) (hE : 0 < E.componentCount) : (D.disjointUnion E).kauffmanBracket a = TemperleyLieb.jonesDelta a * D.kauffmanBracket a * E.kauffmanBracket a

The bracket of the disjoint union of two nonempty diagrams is the product of their brackets times the circle value. Nonemptiness is measured by the component count, so crossing-free diagrams are included.

@[simp]

theorem TauCeti.PDCode.kauffmanBracket_disjointUnion_of_componentCount_eq_zero_left {n m : ℕ} (D : PDCode n) (E : PDCode m) {R : Type u_1} [CommRing R] (a : Rˣ) (hD : D.componentCount = 0) : (D.disjointUnion E).kauffmanBracket a = E.kauffmanBracket a

An empty first summand contributes no factor of the circle value.

@[simp]

theorem TauCeti.PDCode.kauffmanBracket_disjointUnion_of_componentCount_eq_zero_right {n m : ℕ} (D : PDCode n) (E : PDCode m) {R : Type u_1} [CommRing R] (a : Rˣ) (hE : E.componentCount = 0) : (D.disjointUnion E).kauffmanBracket a = D.kauffmanBracket a

An empty second summand contributes no factor of the circle value.