Documentation

TauCeti.KnotTheory.PDCode.Components

Components of PD-codes #

The arcs of a PD-code and the local strands at its crossings determine a permutation of the half-edge labels. Its outgoing restriction has one orbit per component meeting a crossing. Crossing-free components remain an explicit field of PDCode.

The orbits of componentPermOutgoing correspond to the crossing-bearing components; the unrestricted componentPerm preserves orientation and therefore has separate incoming and outgoing orbits for each such component.

The traversal follows M. Mastin, Links and Planar Diagram Codes, Definitions 2–3.

def TauCeti.PDCode.crossingTurn {n : ℕ} (D : PDCode n) :

Equiv.Perm (Fin (4 * n))

The permutation induced by moving to the opposite slot at each crossing.

Equations

D.crossingTurn = (Equiv.permCongr D.halfEdge) ((TauCeti.PDCode.crossingSlotEquiv n).permCongr ((Equiv.refl (Fin n)).prodCongr TauCeti.PDCode.oppositeCrossingSlot))

Instances For

theorem TauCeti.PDCode.crossingTurn_def {n : ℕ} (D : PDCode n) :

D.crossingTurn = (Equiv.permCongr D.halfEdge) ((crossingSlotEquiv n).permCongr ((Equiv.refl (Fin n)).prodCongr oppositeCrossingSlot))

The defining equation for the crossing traversal permutation.

def TauCeti.PDCode.componentPerm {n : ℕ} (D : PDCode n) :

Equiv.Perm (Fin (4 * n))

The component traversal moves across an arc and then through a crossing.

Equations

D.componentPerm = D.crossingTurn * ↑D.edgePair

Instances For

theorem TauCeti.PDCode.componentPerm_def {n : ℕ} (D : PDCode n) :

D.componentPerm = D.crossingTurn * ↑D.edgePair

The defining equation of component traversal.

@[simp]

theorem TauCeti.PDCode.componentPerm_apply {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) :

D.componentPerm h = D.crossingTurn (↑D.edgePair h)

Traversal pairs the arc first, then takes the opposite crossing slot.

@[simp]

theorem TauCeti.PDCode.crossingTurn_crossing {n : ℕ} (D : PDCode n) (i : Fin n) (slot : Fin 4) :

D.crossingTurn (D.halfEdge ((crossingSlotEquiv n) (i, slot))) = D.crossing i (oppositeCrossingSlot slot)

Crossing turns take a crossing slot to its opposite slot.

@[simp]

theorem TauCeti.PDCode.crossingTurn_apply_apply {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) :

D.crossingTurn (D.crossingTurn h) = h

The crossing turn is an involution.

@[simp]

theorem TauCeti.PDCode.crossingTurn_mirror {n : ℕ} (D : PDCode n) :

D.mirror.crossingTurn = D.crossingTurn

Mirroring preserves the opposite-slot permutation.

@[simp]

theorem TauCeti.PDCode.componentPerm_mirror {n : ℕ} (D : PDCode n) :

D.mirror.componentPerm = D.componentPerm

Mirroring preserves component traversal.

@[simp]

theorem TauCeti.PDCode.crossingTurn_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) :

(D.relabel half cross).crossingTurn = half.permCongr D.crossingTurn

Relabelling conjugates the opposite-slot permutation by the half-edge relabelling.

theorem TauCeti.PDCode.crossingTurn_eq_permCongr_sumCongr {n : ℕ} {D : PDCode n} {D' : PDCode (n + 1)} (hD : D'.halfEdge = (halfEdgeSuccEquiv n).permCongr (D.halfEdge.sumCongr 1)) :

D'.crossingTurn = (halfEdgeSuccEquiv n).permCongr (D.crossingTurn.sumCongr oppositeCrossingSlot)

On a code D' with one crossing more than D, whose first n crossings keep the half-edges of D and whose last crossing takes the four new half-edge positions, the crossing turn is that of D together with the opposite-slot permutation of the new crossing.

@[simp]

theorem TauCeti.PDCode.componentPerm_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) :

(D.relabel half cross).componentPerm = half.permCongr D.componentPerm

Relabelling conjugates component traversal by the half-edge relabelling.

noncomputable def TauCeti.PDCode.crossingComponentCount {n : ℕ} (D : PDCode n) :

The number of crossing-bearing components, each represented by two directed traversal orbits. The outgoing restriction records the directed traversal on the positively oriented half-edges.

Equations

D.crossingComponentCount = TauCeti.orbitCount D.componentPerm / 2

Instances For

theorem TauCeti.PDCode.isPerfectMatching_crossingTurn {n : ℕ} (D : PDCode n) :

IsPerfectMatching D.crossingTurn

Crossing traversal is a perfect matching of the half-edge labels.

theorem TauCeti.PDCode.even_orbitCount_componentPerm {n : ℕ} (D : PDCode n) :

Even (orbitCount D.componentPerm)

The directed crossing traversal orbits come in pairs.

theorem TauCeti.PDCode.crossingComponentCount_def {n : ℕ} (D : PDCode n) :

D.crossingComponentCount = orbitCount D.componentPerm / 2

The number of crossing-bearing components is half the number of directed traversal orbits.

theorem TauCeti.PDCode.crossingComponentCount_pos {n : ℕ} (D : PDCode n) (hn : n ≠ 0) :

0 < D.crossingComponentCount

A code with a crossing has at least one crossing-bearing component.

@[simp]

theorem TauCeti.PDCode.crossingComponentCount_eq_zero (D : PDCode 0) :

D.crossingComponentCount = 0

A code with no crossing visits has no crossing-bearing components.

@[simp]

theorem TauCeti.PDCode.crossingComponentCount_mirror {n : ℕ} (D : PDCode n) :

D.mirror.crossingComponentCount = D.crossingComponentCount

Mirroring preserves the number of crossing-bearing components.

@[simp]

theorem TauCeti.PDCode.crossingComponentCount_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) :

(D.relabel half cross).crossingComponentCount = D.crossingComponentCount

Relabelling preserves the number of crossing-bearing components.

@[reducible, inline]

noncomputable abbrev TauCeti.PDCode.componentCount {n : ℕ} (D : PDCode n) :

The total number of components, including crossing-free circles.

Equations

D.componentCount = D.crossingComponentCount + D.crossinglessComponentCount

Instances For

theorem TauCeti.PDCode.componentCount_eq {n : ℕ} (D : PDCode n) :

D.componentCount = D.crossingComponentCount + D.crossinglessComponentCount

The total component count is the sum of crossing-bearing and crossing-free components.

theorem TauCeti.PDCode.componentCount_pos {n : ℕ} (D : PDCode n) (hn : n ≠ 0) :

0 < D.componentCount

A code with a nonzero crossing count has at least one component.

@[simp]

theorem TauCeti.PDCode.componentCount_mirror {n : ℕ} (D : PDCode n) :

D.mirror.componentCount = D.componentCount

Mirroring preserves the total number of components.

@[simp]

theorem TauCeti.PDCode.componentCount_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) :

(D.relabel half cross).componentCount = D.componentCount

Relabelling preserves the total number of components.

@[simp]

theorem TauCeti.PDCode.kink_crossingTurn (i : Fin 1) (t : Fin 4) :

kink.crossingTurn ((crossingSlotEquiv 1) (i, t)) = (crossingSlotEquiv 1) (i, oppositeCrossingSlot t)

Following a strand of the kink through its crossing passes to the opposite slot.

theorem TauCeti.PDCode.crossingComponentCount_kink :

kink.crossingComponentCount = 1

The kink is a diagram of a knot: it has a single component.

@[simp]

theorem TauCeti.OrientedPDCode.orientation_crossingTurn {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) :

D.orientation (D.crossingTurn h) = !D.orientation h

The crossing turn reverses the orientation of a half-edge.

theorem TauCeti.OrientedPDCode.orientation_componentPerm {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) :

D.orientation (D.componentPerm h) = D.orientation h

The component traversal preserves the orientation of a half-edge.

noncomputable def TauCeti.OrientedPDCode.componentPermOutgoing {n : ℕ} (D : OrientedPDCode n) :

Equiv.Perm { h : Fin (4 * n) // D.orientation h = true }

The component traversal permutation restricted to half-edges pointing away from crossings.

Equations

D.componentPermOutgoing = D.componentPerm.subtypePerm ⋯

Instances For

def TauCeti.OrientedPDCode.mirrorOutgoingEquiv {n : ℕ} (D : OrientedPDCode n) :

{ h : Fin (4 * n) // D.orientation h = true } ≃ { h : Fin (4 * n) // D.mirror.orientation h = true }

The identity on half-edge labels identifies outgoing half-edges before and after mirroring.

Equations

D.mirrorOutgoingEquiv = (Equiv.refl (Fin (4 * n))).subtypeEquiv ⋯

Instances For

@[simp]

theorem TauCeti.OrientedPDCode.mirrorOutgoingEquiv_apply {n : ℕ} (D : OrientedPDCode n) (h : { h : Fin (4 * n) // D.orientation h = true }) :

↑(D.mirrorOutgoingEquiv h) = ↑h

The outgoing mirror equivalence preserves the underlying half-edge label.

@[simp]

theorem TauCeti.OrientedPDCode.mirrorOutgoingEquiv_symm_apply {n : ℕ} (D : OrientedPDCode n) (h : { h : Fin (4 * n) // D.mirror.orientation h = true }) :

↑(D.mirrorOutgoingEquiv.symm h) = ↑h

The inverse outgoing mirror equivalence preserves the underlying half-edge label.

@[simp]

theorem TauCeti.OrientedPDCode.componentPermOutgoing_mirror {n : ℕ} (D : OrientedPDCode n) :

D.mirror.componentPermOutgoing = D.mirrorOutgoingEquiv.permCongr D.componentPermOutgoing

Mirroring transports the outgoing traversal along the outgoing half-edge equivalence.

def TauCeti.OrientedPDCode.reverseOutgoingEquiv {n : ℕ} (D : OrientedPDCode n) :

{ h : Fin (4 * n) // D.orientation h = true } ≃ { h : Fin (4 * n) // D.reverse.orientation h = true }

Arc pairing identifies outgoing half-edges with outgoing half-edges after reversal.

Equations

D.reverseOutgoingEquiv = Equiv.subtypeEquiv ↑D.edgePair ⋯

Instances For

@[simp]

theorem TauCeti.OrientedPDCode.reverseOutgoingEquiv_apply {n : ℕ} (D : OrientedPDCode n) (h : { h : Fin (4 * n) // D.orientation h = true }) :

↑(D.reverseOutgoingEquiv h) = ↑D.edgePair ↑h

The outgoing reversal equivalence acts by arc pairing on half-edge labels.

@[simp]

theorem TauCeti.OrientedPDCode.reverseOutgoingEquiv_symm_apply {n : ℕ} (D : OrientedPDCode n) (h : { h : Fin (4 * n) // D.reverse.orientation h = true }) :

↑(D.reverseOutgoingEquiv.symm h) = ↑D.edgePair ↑h

The inverse outgoing reversal equivalence acts by arc pairing.

@[simp]

theorem TauCeti.OrientedPDCode.componentPermOutgoing_symm_apply_val {n : ℕ} (D : OrientedPDCode n) (h : { h : Fin (4 * n) // D.orientation h = true }) :

↑((Equiv.symm D.componentPermOutgoing) h) = (Equiv.symm D.componentPerm) ↑h

Inverse outgoing traversal has the same half-edge value as inverse unrestricted traversal.

@[simp]

theorem TauCeti.OrientedPDCode.componentPermOutgoing_reverse {n : ℕ} (D : OrientedPDCode n) :

D.reverse.componentPermOutgoing = D.reverseOutgoingEquiv.permCongr D.componentPermOutgoing⁻¹

Reversal transports inverse outgoing traversal along the arc-pairing equivalence.

@[simp]

theorem TauCeti.OrientedPDCode.componentPermOutgoing_apply {n : ℕ} (D : OrientedPDCode n) (h : { h : Fin (4 * n) // D.orientation h = true }) :

D.componentPermOutgoing h = ⟨D.componentPerm ↑h, ⋯⟩

Outgoing traversal has the same half-edge value as unrestricted traversal.

@[simp]

theorem TauCeti.OrientedPDCode.orbitCount_componentPermOutgoing {n : ℕ} (D : OrientedPDCode n) :

orbitCount D.componentPermOutgoing = D.crossingComponentCount

Counting outgoing traversal orbits gives the crossing-bearing component count.

def TauCeti.OrientedPDCode.relabelOutgoingEquiv {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) :

{ h : Fin (4 * n) // D.orientation h = true } ≃ { h : Fin (4 * m) // (D.relabel half cross).orientation h = true }

Relabelling restricts to an equivalence of outgoing half-edges.

Equations

D.relabelOutgoingEquiv half cross = half.subtypeEquiv ⋯

Instances For

@[simp]

theorem TauCeti.OrientedPDCode.relabelOutgoingEquiv_apply {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (h : { h : Fin (4 * n) // D.orientation h = true }) :

↑((D.relabelOutgoingEquiv half cross) h) = half ↑h

The outgoing relabelling equivalence acts by the original half-edge permutation.

@[simp]

theorem TauCeti.OrientedPDCode.relabelOutgoingEquiv_symm_apply {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (h : { h : Fin (4 * m) // (D.relabel half cross).orientation h = true }) :

↑((D.relabelOutgoingEquiv half cross).symm h) = half.symm ↑h

The inverse outgoing relabelling equivalence acts by the inverse permutation.

@[simp]

theorem TauCeti.OrientedPDCode.componentPermOutgoing_relabel {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) :

(D.relabel half cross).componentPermOutgoing = (D.relabelOutgoingEquiv half cross).permCongr D.componentPermOutgoing

Relabelling transports outgoing traversal along the outgoing half-edge equivalence.